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. (2011) The ins and outs of the probabilistic model checker MRMC. Performance Evaluation, 68 (2). pp. 90-104. ISSN 0166-5316

[img]PDF
Restricted to UT campus only
: Request a copy
258Kb
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:Article
Copyright:© 2011 Elsevier
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/79364
Official URL:http://dx.doi.org/10.1016/j.peva.2010.04.001
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page