Model Checking Markov Reward Models with Impulse Rewards


Cloth, L. and Katoen, J.P. and Maneesh Khattri, M. and Pulungan, R. (2005) Model Checking Markov Reward Models with Impulse Rewards. In: International Conference on Dependable Systems and Networks, 2005. DSN 2005 (pp. pp. 722-731).

open access
Abstract: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.
Item Type:Conference or Workshop Item
Copyright:©2005 IEEE
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Official URL:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 225539