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 proceedingConference contribution

73 Citations (Scopus)


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 languageEnglish
Title of host publicationQEST 2009, Sixth International Conference on the Quantitative Evaluation of Systems, Budapest, Hungary, 13-16 September 2009
Number of pages10
Publication statusPublished - 2009
Externally publishedYes

Fingerprint Dive into the research topics of 'The Ins and Outs of the Probabilistic Model Checker MRMC'. Together they form a unique fingerprint.

Cite this