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

    168 Citations (Scopus)
    35 Downloads (Pure)


    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
    Pages (from-to)90-104
    Number of pages15
    JournalPerformance evaluation
    Issue number2
    Publication statusPublished - Feb 2011


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


    Dive into the research topics of 'The ins and outs of the probabilistic model checker MRMC'. Together they form a unique fingerprint.

    Cite this