A Markov reward model checker


Katoen, J.P. and Maneesh Khattri, M. and Zapreev, I.S. (2005) A Markov reward model checker. In: Second International Conference on the Quantitative Evaluation of Systems, 2005 (pp. pp. 243-245).

open access
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.
Item Type:Conference or Workshop Item
Additional information:eemcs1545
Copyright:©2005 IEEE
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/54782
Official URL:https://doi.org/10.1109/QEST.2005.2
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 229271