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 › Academic › peer-review

79 Citations (Scopus)

193 Downloads (Pure)

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	2009 Sixth International Conference on the Quantitative Evaluation of Systems
Place of Publication	Los Alamitos, CA
Publisher	IEEE
Pages	167-176
Number of pages	10
ISBN (Print)	978-1-42444-942-2
DOIs	https://doi.org/10.1109/QEST.2009.11
Publication status	Published - Sept 2009
Event	6th International Conference on Quantitative Evaluation of SysTems, QEST 2009 - Technical University of Budapest, Budapest, Hungary Duration: 13 Sept 2009 → 16 Sept 2009 Conference number: 6 http://www.qest.org/qest2009/

Conference

Conference	6th International Conference on Quantitative Evaluation of SysTems, QEST 2009
Abbreviated title	QEST
Country/Territory	Hungary
City	Budapest
Period	13/09/09 → 16/09/09
Internet address	http://www.qest.org/qest2009/

Access to Document

10.1109/QEST.2009.11

Cite this

@inproceedings{06a553eeae614bc99f7135bcdc3256dc,

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

month = sep,

doi = "10.1109/QEST.2009.11",

language = "English",

isbn = "978-1-42444-942-2",

pages = "167--176",

booktitle = "2009 Sixth International Conference on the Quantitative Evaluation of Systems",

publisher = "IEEE",

address = "United States",

note = "6th International Conference on Quantitative Evaluation of SysTems, QEST 2009, QEST ; Conference date: 13-09-2009 Through 16-09-2009",

url = "http://www.qest.org/qest2009/",

}

Katoen, J-P, Zapreev, IS, Hahn, EM, Hermanns, H & Jansen, DN 2009, The Ins and Outs of the Probabilistic Model Checker MRMC. in 2009 Sixth International Conference on the Quantitative Evaluation of Systems. IEEE, Los Alamitos, CA, pp. 167-176, 6th International Conference on Quantitative Evaluation of SysTems, QEST 2009, Budapest, Hungary, 13/09/09. https://doi.org/10.1109/QEST.2009.11

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.

N1 - Conference code: 6

PY - 2009/9

Y1 - 2009/9

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

SN - 978-1-42444-942-2

SP - 167

EP - 176

BT - 2009 Sixth International Conference on the Quantitative Evaluation of Systems

PB - IEEE

CY - Los Alamitos, CA

T2 - 6th International Conference on Quantitative Evaluation of SysTems, QEST 2009

Y2 - 13 September 2009 through 16 September 2009

ER -

The Ins and Outs of the Probabilistic Model Checker MRMC

Abstract

Conference

Access to Document

Fingerprint

Cite this