Sciweavers

Share
QEST
2009
IEEE

The Ins and Outs of the Probabilistic Model Checker MRMC

9 years 2 months ago
The Ins and Outs of the Probabilistic Model Checker MRMC
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.
Joost-Pieter Katoen, Ivan S. Zapreev, Ernst Moritz
Added 21 May 2010
Updated 21 May 2010
Type Conference
Year 2009
Where QEST
Authors Joost-Pieter Katoen, Ivan S. Zapreev, Ernst Moritz Hahn, Holger Hermanns, David N. Jansen
Comments (0)
books