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

    73 Citations (Scopus)
    115 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