The Ins and Outs of the Probabilistic Model Checker MRMC

Joost-Pieter Katoen; Ivan S. Zapreev; Ernst Moritz Hahn; Holger Hermanns; David N. Jansen

doi:10.1109/QEST.2009.11

The Ins and Outs of the Probabilistic Model Checker MRMC

Joost-Pieter Katoen, Ivan S. Zapreev, Ernst Moritz Hahn, Holger Hermanns, David N. Jansen

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

79 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 language	English
Title of host publication	QEST 2009, Sixth International Conference on the Quantitative Evaluation of Systems, Budapest, Hungary, 13-16 September 2009
Pages	167-176
Number of pages	10
DOIs	https://doi.org/10.1109/QEST.2009.11
Publication status	Published - 2009
Externally published	Yes

Access to Document

10.1109/QEST.2009.11

https://doi.org/10.1109/QEST.2009.11

Cite this

@inproceedings{f8ab85c8d9bd43c483b687af4bd8fff5,

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.",

author = "Joost-Pieter Katoen and Zapreev, {Ivan S.} and Hahn, {Ernst Moritz} and Holger Hermanns and Jansen, {David N.}",

year = "2009",

doi = "10.1109/QEST.2009.11",

language = "English",

pages = "167--176",

booktitle = "QEST 2009, Sixth International Conference on the Quantitative Evaluation of Systems, Budapest, Hungary, 13-16 September 2009",

}

TY - GEN

T1 - The Ins and Outs of the Probabilistic Model Checker MRMC

AU - Katoen, Joost-Pieter

AU - Zapreev, Ivan S.

AU - Hahn, Ernst Moritz

AU - Hermanns, Holger

AU - Jansen, David N.

PY - 2009

Y1 - 2009

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.

U2 - 10.1109/QEST.2009.11

DO - 10.1109/QEST.2009.11

M3 - Conference contribution

SP - 167

EP - 176

BT - QEST 2009, Sixth International Conference on the Quantitative Evaluation of Systems, Budapest, Hungary, 13-16 September 2009

ER -

The Ins and Outs of the Probabilistic Model Checker MRMC

Abstract

Access to Document

Fingerprint

Cite this