Performability assessment by model checking of Markov reward models

Christel Baier, Lucia Cloth, Boudewijn R. Haverkort, Holger Hermanns, Joost P. Katoen

Research output: Contribution to journalArticleAcademicpeer-review

21 Citations (Scopus)

Abstract

This paper describes efficient procedures for model checking Markov reward models, that allow us to evaluate, among others, the performability of computer-communication systems. We present the logic CSRL (Continuous Stochastic Reward Logic) to specify performability measures. It provides flexibility in measure specification and paves the way for the numerical evaluation of a wide variety of performability measures. The formal measure specification in CSRL also often helps in reducing the size of the Markov reward models that need to be numerically analysed. The paper presents background on Markov-reward models, as well as on the logic CSRL (syntax and semantics), before presenting an important duality result between reward and time. We discuss CSRL model-checking algorithms, and present five numerical algorithms and their computational complexity for verifying time- and reward-bounded until-properties, one of the key operators in CSRL. The versatility of our approach is illustrated through a performability case study.
Original languageEnglish
Pages (from-to)1-36
Number of pages36
JournalFormal methods in system design
Volume36
Issue number1
DOIs
Publication statusPublished - 2010

Fingerprint

Performability
Model checking
Reward
Model Checking
Logic
Specifications
Computational complexity
Communication systems
Semantics
Model
Specification
Numerical Algorithms
Communication Systems
Duality
Computational Complexity
Flexibility

Keywords

  • Model checking
  • Performability
  • Markov reward models

Cite this

@article{fb0ce23588f04ccf8553239099ca8d2a,
title = "Performability assessment by model checking of Markov reward models",
abstract = "This paper describes efficient procedures for model checking Markov reward models, that allow us to evaluate, among others, the performability of computer-communication systems. We present the logic CSRL (Continuous Stochastic Reward Logic) to specify performability measures. It provides flexibility in measure specification and paves the way for the numerical evaluation of a wide variety of performability measures. The formal measure specification in CSRL also often helps in reducing the size of the Markov reward models that need to be numerically analysed. The paper presents background on Markov-reward models, as well as on the logic CSRL (syntax and semantics), before presenting an important duality result between reward and time. We discuss CSRL model-checking algorithms, and present five numerical algorithms and their computational complexity for verifying time- and reward-bounded until-properties, one of the key operators in CSRL. The versatility of our approach is illustrated through a performability case study.",
keywords = "Model checking, Performability, Markov reward models",
author = "Christel Baier and Lucia Cloth and Haverkort, {Boudewijn R.} and Holger Hermanns and Katoen, {Joost P.}",
year = "2010",
doi = "10.1007/s10703-009-0088-7",
language = "English",
volume = "36",
pages = "1--36",
journal = "Formal methods in system design",
issn = "0925-9856",
publisher = "Springer",
number = "1",

}

Performability assessment by model checking of Markov reward models. / Baier, Christel; Cloth, Lucia; Haverkort, Boudewijn R.; Hermanns, Holger; Katoen, Joost P.

In: Formal methods in system design, Vol. 36, No. 1, 2010, p. 1-36.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Performability assessment by model checking of Markov reward models

AU - Baier, Christel

AU - Cloth, Lucia

AU - Haverkort, Boudewijn R.

AU - Hermanns, Holger

AU - Katoen, Joost P.

PY - 2010

Y1 - 2010

N2 - This paper describes efficient procedures for model checking Markov reward models, that allow us to evaluate, among others, the performability of computer-communication systems. We present the logic CSRL (Continuous Stochastic Reward Logic) to specify performability measures. It provides flexibility in measure specification and paves the way for the numerical evaluation of a wide variety of performability measures. The formal measure specification in CSRL also often helps in reducing the size of the Markov reward models that need to be numerically analysed. The paper presents background on Markov-reward models, as well as on the logic CSRL (syntax and semantics), before presenting an important duality result between reward and time. We discuss CSRL model-checking algorithms, and present five numerical algorithms and their computational complexity for verifying time- and reward-bounded until-properties, one of the key operators in CSRL. The versatility of our approach is illustrated through a performability case study.

AB - This paper describes efficient procedures for model checking Markov reward models, that allow us to evaluate, among others, the performability of computer-communication systems. We present the logic CSRL (Continuous Stochastic Reward Logic) to specify performability measures. It provides flexibility in measure specification and paves the way for the numerical evaluation of a wide variety of performability measures. The formal measure specification in CSRL also often helps in reducing the size of the Markov reward models that need to be numerically analysed. The paper presents background on Markov-reward models, as well as on the logic CSRL (syntax and semantics), before presenting an important duality result between reward and time. We discuss CSRL model-checking algorithms, and present five numerical algorithms and their computational complexity for verifying time- and reward-bounded until-properties, one of the key operators in CSRL. The versatility of our approach is illustrated through a performability case study.

KW - Model checking

KW - Performability

KW - Markov reward models

U2 - 10.1007/s10703-009-0088-7

DO - 10.1007/s10703-009-0088-7

M3 - Article

VL - 36

SP - 1

EP - 36

JO - Formal methods in system design

JF - Formal methods in system design

SN - 0925-9856

IS - 1

ER -