Model Checking Markov Reward Models with Impulse Rewards

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

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

24 Citations (Scopus)
6 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 languageEnglish
Title of host publication2005 International Conference on Dependable Systems and Networks (DSN'05)
EditorsAndrea Bondavalli, Boudewijn Haverkort, Dong Tang
Place of PublicationLos Alamitos, NJ
PublisherIEEE Computer Society
Pages722-731
Number of pages10
ISBN (Print)0-7695-2282-3
DOIs
Publication statusPublished - Jul 2005
EventInternational Conference on Dependable Systems and Networks, DSN 2005 - Yokohama, Japan
Duration: 28 Jun 20051 Jul 2005

Conference

ConferenceInternational Conference on Dependable Systems and Networks, DSN 2005
Abbreviated titleDSN
CountryJapan
CityYokohama
Period28/06/051/07/05

Fingerprint

Model checking
Markov processes
Energy utilization

Keywords

  • EWI-1542
  • IR-53159
  • METIS-225539

Cite this

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) (pp. 722-731). Los Alamitos, NJ: IEEE Computer Society. https://doi.org/10.1109/DSN.2005.64
Cloth, Lucia ; Katoen, Joost-Pieter ; Khattri, Maneesh ; Pulungan, Reza. / Model Checking Markov Reward Models with Impulse Rewards. 2005 International Conference on Dependable Systems and Networks (DSN'05). editor / Andrea Bondavalli ; Boudewijn Haverkort ; Dong Tang. Los Alamitos, NJ : IEEE Computer Society, 2005. pp. 722-731
@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 = "7",
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 Computer Society",
address = "United States",

}

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 Computer Society, 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; Pulungan, Reza.

2005 International Conference on Dependable Systems and Networks (DSN'05). ed. / Andrea Bondavalli; Boudewijn Haverkort; Dong Tang. Los Alamitos, NJ : IEEE Computer Society, 2005. p. 722-731.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-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 Computer Society

CY - Los Alamitos, NJ

ER -

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