Performability assessment by model checking of Markov reward models
Aus International Center for Computational Logic
Performability assessment by model checking of Markov reward models
Christel BaierChristel Baier, Lucia ClothLucia Cloth, Boudewijn R. HaverkortBoudewijn R. Haverkort, Holger HermannsHolger Hermanns, Joost-Pieter KatoenJoost-Pieter Katoen
Christel Baier, Lucia Cloth, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen
Performability assessment by model checking of Markov reward models
Formal Methods in System Design, 36(1):1--36, 2010
Performability assessment by model checking of Markov reward models
Formal Methods in System Design, 36(1):1--36, 2010
- KurzfassungAbstract
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. - Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science
@article{BCHHK2010,
author = {Christel Baier and Lucia Cloth and Boudewijn R. Haverkort and
Holger Hermanns and Joost-Pieter Katoen},
title = {Performability assessment by model checking of Markov reward models},
journal = {Formal Methods in System Design},
volume = {36},
number = {1},
year = {2010},
pages = {1--36},
doi = {10.1007/S10703-009-0088-7}
}
