2005 International Conference on Dependable Systems and Networks (DSN'05) (2005)
June 28, 2005 to July 1, 2005
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/DSN.2005.64
Lucia Cloth , University of Twente
Joost-Pieter Katoen , RWTH Aachen and University of Twente
Maneesh Khattri , University of Twente
Reza Pulungan , Saarland University
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.
J. Katoen, L. Cloth, M. Khattri and R. Pulungan, "Model Checking Markov Reward Models with Impulse Rewards," 2005 International Conference on Dependable Systems and Networks (DSN'05)(DSN), Yokohama, Japan, 2005, pp. 722-731.