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 contributionAcademicpeer-review

    73 Citations (Scopus)
    122 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 languageEnglish
    Title of host publication2009 Sixth International Conference on the Quantitative Evaluation of Systems
    Place of PublicationLos Alamitos, CA
    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/

    Conference

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

    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