Model Checking for Performability

Christel BaierChristel Baier, Ernst-Moritz HahnErnst-Moritz Hahn, Boudewijn HaverkortBoudewijn Haverkort, Holger HermannsHolger Hermanns, Joost-Pieter KatoenJoost-Pieter Katoen

DOI Link

Christel Baier, Ernst-Moritz Hahn, Boudewijn Haverkort, Holger Hermanns, Joost-Pieter Katoen
Model Checking for Performability
Mathematical Structures in Computer Science, 23(4):751--795, 2013

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@article{BHHHK2013,
  author  = {Christel Baier and Ernst-Moritz Hahn and Boudewijn Haverkort and
             Holger Hermanns and Joost-Pieter Katoen},
  title   = {Model Checking for Performability},
  journal = {Mathematical Structures in Computer Science},
  volume  = {23},
  number  = {4},
  year    = {2013},
  pages   = {751--795},
  doi     = {10.1017/S0960129512000254}
}