The ins and outs of the probabilistic model checker MRMC

Joost P. Katoen, I.S. Zapreev, Ernst Moritz Hahn, H. Hermanns, D.N. Jansen

Research output: Contribution to journalArticleAcademicpeer-review

135 Citations (Scopus)

Abstract

The Markov Reward Model Checker (MRMC) is a software tool for verifying properties over probabilistic models. It supports PCTL and CSL model checking, and their reward extensions. Distinguishing features of MRMC are its support for computing time- and reward-bounded reachability probabilities, (property-driven) bisimulation minimization, and precise on-the-fly steady-state detection. Recent tool features include time-bounded reachability analysis for uniform CTMDPs and CSL model checking by discrete-event simulation. This paper presents the tool’s current status and its implementation details.
Original languageUndefined
Pages (from-to)90-104
Number of pages15
JournalPerformance evaluation
Volume68
Issue number2
DOIs
Publication statusPublished - Feb 2011

Keywords

  • EWI-21246
  • Markov chains
  • Model Checking
  • DTMC
  • Discrete Event Simulation
  • MRM
  • METIS-285230
  • IR-79364
  • CTMDP
  • CTMC
  • Bisimulation minimization
  • Numerical analysis

Cite this

Katoen, Joost P. ; Zapreev, I.S. ; Hahn, Ernst Moritz ; Hermanns, H. ; Jansen, D.N. / The ins and outs of the probabilistic model checker MRMC. In: Performance evaluation. 2011 ; Vol. 68, No. 2. pp. 90-104.
@article{eaa683f2d0544e88941716bdcc1fde3a,
title = "The ins and outs of the probabilistic model checker MRMC",
abstract = "The Markov Reward Model Checker (MRMC) is a software tool for verifying properties over probabilistic models. It supports PCTL and CSL model checking, and their reward extensions. Distinguishing features of MRMC are its support for computing time- and reward-bounded reachability probabilities, (property-driven) bisimulation minimization, and precise on-the-fly steady-state detection. Recent tool features include time-bounded reachability analysis for uniform CTMDPs and CSL model checking by discrete-event simulation. This paper presents the tool’s current status and its implementation details.",
keywords = "EWI-21246, Markov chains, Model Checking, DTMC, Discrete Event Simulation, MRM, METIS-285230, IR-79364, CTMDP, CTMC, Bisimulation minimization, Numerical analysis",
author = "Katoen, {Joost P.} and I.S. Zapreev and Hahn, {Ernst Moritz} and H. Hermanns and D.N. Jansen",
note = "10.1016/j.peva.2010.04.001",
year = "2011",
month = "2",
doi = "10.1016/j.peva.2010.04.001",
language = "Undefined",
volume = "68",
pages = "90--104",
journal = "Performance evaluation",
issn = "0166-5316",
publisher = "Elsevier",
number = "2",

}

Katoen, JP, Zapreev, IS, Hahn, EM, Hermanns, H & Jansen, DN 2011, 'The ins and outs of the probabilistic model checker MRMC' Performance evaluation, vol. 68, no. 2, pp. 90-104. https://doi.org/10.1016/j.peva.2010.04.001

The ins and outs of the probabilistic model checker MRMC. / Katoen, Joost P.; Zapreev, I.S.; Hahn, Ernst Moritz; Hermanns, H.; Jansen, D.N.

In: Performance evaluation, Vol. 68, No. 2, 02.2011, p. 90-104.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - The ins and outs of the probabilistic model checker MRMC

AU - Katoen, Joost P.

AU - Zapreev, I.S.

AU - Hahn, Ernst Moritz

AU - Hermanns, H.

AU - Jansen, D.N.

N1 - 10.1016/j.peva.2010.04.001

PY - 2011/2

Y1 - 2011/2

N2 - The Markov Reward Model Checker (MRMC) is a software tool for verifying properties over probabilistic models. It supports PCTL and CSL model checking, and their reward extensions. Distinguishing features of MRMC are its support for computing time- and reward-bounded reachability probabilities, (property-driven) bisimulation minimization, and precise on-the-fly steady-state detection. Recent tool features include time-bounded reachability analysis for uniform CTMDPs and CSL model checking by discrete-event simulation. This paper presents the tool’s current status and its implementation details.

AB - The Markov Reward Model Checker (MRMC) is a software tool for verifying properties over probabilistic models. It supports PCTL and CSL model checking, and their reward extensions. Distinguishing features of MRMC are its support for computing time- and reward-bounded reachability probabilities, (property-driven) bisimulation minimization, and precise on-the-fly steady-state detection. Recent tool features include time-bounded reachability analysis for uniform CTMDPs and CSL model checking by discrete-event simulation. This paper presents the tool’s current status and its implementation details.

KW - EWI-21246

KW - Markov chains

KW - Model Checking

KW - DTMC

KW - Discrete Event Simulation

KW - MRM

KW - METIS-285230

KW - IR-79364

KW - CTMDP

KW - CTMC

KW - Bisimulation minimization

KW - Numerical analysis

U2 - 10.1016/j.peva.2010.04.001

DO - 10.1016/j.peva.2010.04.001

M3 - Article

VL - 68

SP - 90

EP - 104

JO - Performance evaluation

JF - Performance evaluation

SN - 0166-5316

IS - 2

ER -