Model Checking Markov Reward Models with Impulse Rewards

Lucia Cloth; Joost-Pieter Katoen; Maneesh Khattri; Reza Pulungan

doi:10.1109/DSN.2005.64

Model Checking Markov Reward Models with Impulse Rewards

Lucia Cloth
, Joost-Pieter Katoen
, Maneesh Khattri
, Reza Pulungan

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

31 Citations (Scopus)

23 Downloads (Pure)

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.

Original language	English
Title of host publication	2005 International Conference on Dependable Systems and Networks (DSN'05)
Editors	Andrea Bondavalli, Boudewijn Haverkort, Dong Tang
Place of Publication	Los Alamitos, NJ
Publisher	IEEE
Pages	722-731
Number of pages	10
ISBN (Print)	0-7695-2282-3
DOIs	https://doi.org/10.1109/DSN.2005.64
Publication status	Published - Jul 2005
Event	International Conference on Dependable Systems and Networks, DSN 2005 - Yokohama, Japan Duration: 28 Jun 2005 → 1 Jul 2005

Conference

Conference	International Conference on Dependable Systems and Networks, DSN 2005
Abbreviated title	DSN
Country/Territory	Japan
City	Yokohama
Period	28/06/05 → 1/07/05

Keywords

EWI-1542
IR-53159
METIS-225539

Access to Document

10.1109/DSN.2005.64

http://doi.ieeecomputersociety.org/10.1109/DSN.2005.64

Cite this

@inproceedings{55890effdca8495ca0f241094411e3d8,

title = "Model Checking Markov Reward Models with Impulse Rewards",

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.",

keywords = "EWI-1542, IR-53159, METIS-225539",

author = "Lucia Cloth and Joost-Pieter Katoen and Maneesh Khattri and Reza Pulungan",

year = "2005",

month = jul,

doi = "10.1109/DSN.2005.64",

language = "English",

isbn = "0-7695-2282-3",

pages = "722--731",

editor = "Andrea Bondavalli and Boudewijn Haverkort and Dong Tang",

booktitle = "2005 International Conference on Dependable Systems and Networks (DSN'05)",

publisher = "IEEE",

address = "United States",

note = "International Conference on Dependable Systems and Networks, DSN 2005, DSN ; Conference date: 28-06-2005 Through 01-07-2005",

}

Cloth, L, Katoen, J-P, Khattri, M & Pulungan, R 2005, Model Checking Markov Reward Models with Impulse Rewards. in A Bondavalli, B Haverkort & D Tang (eds), 2005 International Conference on Dependable Systems and Networks (DSN'05). IEEE, Los Alamitos, NJ, pp. 722-731, International Conference on Dependable Systems and Networks, DSN 2005, Yokohama, Japan, 28/06/05. https://doi.org/10.1109/DSN.2005.64

Model Checking Markov Reward Models with Impulse Rewards. / Cloth, Lucia; Katoen, Joost-Pieter; Khattri, Maneesh et al.
2005 International Conference on Dependable Systems and Networks (DSN'05). ed. / Andrea Bondavalli; Boudewijn Haverkort; Dong Tang. Los Alamitos, NJ: IEEE, 2005. p. 722-731.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Model Checking Markov Reward Models with Impulse Rewards

AU - Cloth, Lucia

AU - Katoen, Joost-Pieter

AU - Khattri, Maneesh

AU - Pulungan, Reza

PY - 2005/7

Y1 - 2005/7

N2 - 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.

AB - 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.

KW - EWI-1542

KW - IR-53159

KW - METIS-225539

U2 - 10.1109/DSN.2005.64

DO - 10.1109/DSN.2005.64

M3 - Conference contribution

SN - 0-7695-2282-3

SP - 722

EP - 731

BT - 2005 International Conference on Dependable Systems and Networks (DSN'05)

A2 - Bondavalli, Andrea

A2 - Haverkort, Boudewijn

A2 - Tang, Dong

PB - IEEE

CY - Los Alamitos, NJ

T2 - International Conference on Dependable Systems and Networks, DSN 2005

Y2 - 28 June 2005 through 1 July 2005

ER -

Model Checking Markov Reward Models with Impulse Rewards

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this