Model checking meets performance evaluation

Christel Baier, Boudewijn R.H.M. Haverkort, H. Hermanns, Joost P. Katoen

Research output: Contribution to journalArticleScientificpeer-review

Abstract

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.
Original languageEnglish
Pages (from-to)10-16
Number of pages7
JournalPerformance Evaluation Review
Volume32
Issue number4
DOIs
Publication statusPublished - 2005
Externally publishedYes

Keywords

  • METIS-225813
  • EWI-1434
  • IR-53274

Fingerprint Dive into the research topics of 'Model checking meets performance evaluation'. Together they form a unique fingerprint.

  • Cite this