A Markov reward model checker

Joost P. Katoen, M. Maneesh Khattri, I.S. Zapreev, I.S. Zapreev

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

    172 Citations (Scopus)
    73 Downloads (Pure)

    Abstract

    This short tool paper introduces MRMC, a model checker for discrete-time and continuous-time Markov reward models. It supports reward extensions of PCTL and CSL, and allows for the automated verification of properties concerning long-run and instantaneous rewards as well as cumulative rewards. In particular, it supports to check the reachability of a set of goal states (by only visiting legal states before) under a time and an accumulated reward constraint. Several numerical algorithms and extensions thereof are included in MRMC.
    Original languageUndefined
    Title of host publication2nd Int. Conf. on Quantitative Evaluation of Systems
    Place of PublicationLos Alamitos, California
    PublisherIEEE Computer Society
    Pages243-245
    Number of pages3
    ISBN (Print)0 7695 2427 3
    DOIs
    Publication statusPublished - 2005
    Event2nd International Conference on the Quantitative Evaluation of Systems, QEST 2005 - Torino Incontra Conference Centre, Turin, Italy
    Duration: 19 Sep 2005 → 22 Sep 2005
    Conference number: 2
    http://www.qest.org/qest2005/

    Publication series

    Name
    PublisherIEEE CS Press

    Conference

    Conference2nd International Conference on the Quantitative Evaluation of Systems, QEST 2005
    Abbreviated titleQEST
    CountryItaly
    CityTurin
    Period19/09/05 → 22/09/05
    Internet address

    Keywords

    • EWI-1545
    • IR-54782
    • METIS-229271

    Access to Document

      Cite this

      Katoen, J. P., Maneesh Khattri, M., Zapreev, I. S., & Zapreev, I. S. (2005). A Markov reward model checker. In 2nd Int. Conf. on Quantitative Evaluation of Systems (pp. 243-245). Los Alamitos, California: IEEE Computer Society. https://doi.org/10.1109/QEST.2005.2