The Ins and Outs of the Probabilistic Model Checker MRMC


Share/Save/Bookmark

Katoen, Joost-Pieter and Zapreev, Ivan S. and Hahn, Ernst Moritz and Hermanns, Holger and Jansen, David N. (2009) The Ins and Outs of the Probabilistic Model Checker MRMC. In: Sixth International Conference on the Quantitative Evaluation of Systems, QEST, 13-16 Sept 2009, Budapest, Hungary (pp. pp. 167-176).

open access
[img]
Preview
PDF
264kB
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.
Item Type:Conference or Workshop Item
Copyright:© 2009 IEEE
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/69308
Official URL:http://dx.doi.org/10.1109/QEST.2009.11
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page