Model checking meets performance evaluation

Christel BaierChristel Baier, Boudewijn R. HaverkortBoudewijn R. Haverkort, Holger HermannsHolger Hermanns, Joost-Pieter KatoenJoost-Pieter Katoen

DOI Link

Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen
Model checking meets performance evaluation
SIGMETRICS Performance Evaluation Review, 32(4):10--15, 2005

Details
Bibtex

KurzfassungAbstract
Markov chains are one of the most popular models for the evaluation of performance and dependability of information processing systems. To obtain performance measures, typically long-run or transient state probabilities of Markov chains are determined. Sometimes the Markov chain at hand is equipped with rewards and computations involve determining long-run or instantaneous reward probabilities.This note summarises a technique to determine performance and dependability guarantees of Markov chains. Given a precise description of the desired guarantee, all states in the Markov chain are determined that surely meet the guarantee. This is done in a fully automated way. Guarantees are described using logics. The use of logics yields an expressive framework that allows to express well-known measures, but also (new) intricate and complex performance guarantees. The power of this technique is that no matter how complex the logical guarantee, it is automatically checked which states in the Markov chain satisfy it. Neither manual manipulations of Markov chains (or their high-level descriptions) are needed, nor the knowledge of any numerical technique to analyze them efficiently. This applies to any (time-homogeneous) Markov chain of any structure specified in any high-level formalism.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@article{BHHK2005,
  author  = {Christel Baier and Boudewijn R. Haverkort and Holger Hermanns and
             Joost-Pieter Katoen},
  title   = {Model checking meets performance evaluation},
  journal = {SIGMETRICS Performance Evaluation Review},
  volume  = {32},
  number  = {4},
  year    = {2005},
  pages   = {10--15},
  doi     = {10.1145/1059816.1059819}
}