Model Checking Markov Reward Models with Impulse Rewards


Share/Save/Bookmark

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
[img]
Preview
PDF
355kB
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
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/53159
Official URL:http://dx.doi.org/10.1109/DSN.2005.64
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 225539