MRMC - Markov Reward Model Checker
Subproject |
S3 |
Categories |
Model checker for hard & soft real-time systems, Model checker / solver for probabilistic systems |
Overview |
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. |
J.-P. Katoen, I.S. Zapreev, E.M. Hahn, H. Hermanns, and D.N. Jansen. The Ins and Outs of the Probabilistic Model Checker MRMC. To appear in Performance Evaluation. Online version available from ScienceDirect. The new sparse matrix data structure described in this article has not been inserted in the main version of MRMC, but is available as a patch from the download page. J.-P. Katoen, I.S. Zapreev, E.M. Hahn, H. Hermanns, D.N. Jansen. The Ins and Outs of The Probabilistic Model Checker MRMC. In International Conference on Quantitative Evaluation of Systems (QEST), pages 167-176, 2009. |
|
Fault-tolerant Work Station Cluster, ETCS Application Level 2, Mutual Exclusion with Random Times |
|
Download |
|
Manual |
|
Status |
Stable |