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: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

71 Citations (Scopus)
61 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 languageUndefined
Title of host publicationSixth International Conference on the Quantitative Evaluation of Systems
Place of PublicationLos Alamitos
PublisherIEEE Computer Society Press
Pages167-176
Number of pages10
ISBN (Print)978-1-42444-942-2
DOIs
Publication statusPublished - Sep 2009
Event6th International Conference on Quantitative Evaluation of SysTems, QEST 2009 - Technical University of Budapest, Budapest, Hungary
Duration: 13 Sep 200916 Sep 2009
Conference number: 6
http://www.qest.org/qest2009/

Publication series

Name
PublisherIEEE Computer Society Press

Conference

Conference6th International Conference on Quantitative Evaluation of SysTems, QEST 2009
Abbreviated titleQEST
CountryHungary
CityBudapest
Period13/09/0916/09/09
Internet address

Keywords

  • METIS-264291
  • EWI-17104
  • IR-69308

Cite this

Katoen, J. P., Zapreev, I. S., Hahn, E. M., Hermanns, H., & Jansen, D. N. (2009). The Ins and Outs of the Probabilistic Model Checker MRMC. In Sixth International Conference on the Quantitative Evaluation of Systems (pp. 167-176). [10.1109/QEST.2009.11] Los Alamitos: IEEE Computer Society Press. https://doi.org/10.1109/QEST.2009.11
Katoen, Joost P. ; Zapreev, I.S. ; Hahn, Ernst Moritz ; Hermanns, H. ; Jansen, D.N. / The Ins and Outs of the Probabilistic Model Checker MRMC. Sixth International Conference on the Quantitative Evaluation of Systems. Los Alamitos : IEEE Computer Society Press, 2009. pp. 167-176
@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.",
keywords = "METIS-264291, EWI-17104, IR-69308",
author = "Katoen, {Joost P.} and I.S. Zapreev and Hahn, {Ernst Moritz} and H. Hermanns and D.N. Jansen",
note = "10.1109/QEST.2009.11",
year = "2009",
month = "9",
doi = "10.1109/QEST.2009.11",
language = "Undefined",
isbn = "978-1-42444-942-2",
publisher = "IEEE Computer Society Press",
pages = "167--176",
booktitle = "Sixth International Conference on the Quantitative Evaluation of Systems",

}

Katoen, JP, Zapreev, IS, Hahn, EM, Hermanns, H & Jansen, DN 2009, The Ins and Outs of the Probabilistic Model Checker MRMC. in Sixth International Conference on the Quantitative Evaluation of Systems., 10.1109/QEST.2009.11, IEEE Computer Society Press, Los Alamitos, 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

The Ins and Outs of the Probabilistic Model Checker MRMC. / Katoen, Joost P.; Zapreev, I.S.; Hahn, Ernst Moritz; Hermanns, H.; Jansen, D.N.

Sixth International Conference on the Quantitative Evaluation of Systems. Los Alamitos : IEEE Computer Society Press, 2009. p. 167-176 10.1109/QEST.2009.11.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

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.1109/QEST.2009.11

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.

KW - METIS-264291

KW - EWI-17104

KW - IR-69308

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 - Sixth International Conference on the Quantitative Evaluation of Systems

PB - IEEE Computer Society Press

CY - Los Alamitos

ER -

Katoen JP, Zapreev IS, Hahn EM, Hermanns H, Jansen DN. The Ins and Outs of the Probabilistic Model Checker MRMC. In Sixth International Conference on the Quantitative Evaluation of Systems. Los Alamitos: IEEE Computer Society Press. 2009. p. 167-176. 10.1109/QEST.2009.11 https://doi.org/10.1109/QEST.2009.11