The ins and outs of the probabilistic model checker MRMC
In Performance Evaluation
, 68: 90-104, 2011.
Downloads: pdf, bibURL: http://dx.doi.org/10.1016/j.peva.2010.04.001
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 continuous-time Markov decision processes (CTMDPs) and CSL model
checking by discrete-event simulation. This paper presents the tool's current
status and its implementation details.