Model checking for performability

C. Baier, E. M. Hahn, B. R. Haverkort, H. Hermanns, J.-P. Katoen

Research output: Contribution to journalArticle

15 Citations (Scopus)


This paper gives a bird's-eye view of the various ingredients that make up a modern, model-checking-based approach to performability evaluation: Markov reward models, temporal logics and continuous stochastic logic, model-checking algorithms, bisimulation and the handling of non-determinism. A short historical account as well as a large case study complete this picture. In this way, we show convincingly that the smart combination of performability evaluation with stochastic model-checking techniques, developed over the last decade, provides a powerful and unified method of performability evaluation, thereby combining the advantages of earlier approaches.
Original languageEnglish
Pages (from-to)751-795
Number of pages45
JournalMathematical Structures in Computer Science
Issue number4
Early online date08 Jul 2013
Publication statusPublished - Aug 2013
Externally publishedYes

Fingerprint Dive into the research topics of 'Model checking for performability'. Together they form a unique fingerprint.

  • Cite this

    Baier, C., Hahn, E. M., Haverkort, B. R., Hermanns, H., & Katoen, J-P. (2013). Model checking for performability. Mathematical Structures in Computer Science, 23(4), 751-795.