2005 International Conference on Dependable Systems and Networks (DSN'05)
Model Checking Markov Reward Models with Impulse Rewards
Yokohama, Japan
June 28-July 01
ISBN: 0-7695-2282-3
DOI Bookmark:
http://doi.ieeecomputersociety.org/10.1109/DSN.2005.64
This paper considers model checking of Markov reward models (MRMs), continuous-time Markov chains with state rewards as well as impulse rewards. The reward extension of the logic CSL (Continuous Stochastic Logic) is interpreted over such MRMs, and two numerical algorithms are provided to check the reachability of a set of goal states under a time and an accumulated reward constraint. This extends existing model-checking techniques for MRMs with just state rewards, and improves the applicability to thousands of states. Our approach is illustrated by using rewards for energy consumption in the setting of dynamic power management.
Citation:
Lucia Cloth, Joost-Pieter Katoen, Maneesh Khattri, Reza Pulungan, "Model Checking Markov Reward Models with Impulse Rewards," dsn, pp.722-731, 2005 International Conference on Dependable Systems and Networks (DSN'05), 2005
Usage of this product signifies your acceptance of the
Terms of Use.
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||