Model checking for performability

C Baier, E.M. Hahn, Boudewijn R.H.M. Haverkort, H. Hermanns, Joost P. Katoen

Research output: Contribution to journalArticleScientificpeer-review

20 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 numberSpecial Issue 04
Publication statusPublished - Aug 2013
Externally publishedYes


  • EC Grant Agreement nr.: FP7/318490
  • EC Grant Agreement nr.: FP7/2007-2013
  • IR-87378
  • METIS-299989
  • EWI-23612


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

Cite this