The ins and outs of the probabilistic model checker MRMC

Joost-Pieter Katoen, Ivan S. Zapreev, Ernst Moritz Hahn, Holger Hermanns, David N. Jansen

Research output: Contribution to journalArticlepeer-review

150 Citations (Scopus)

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.
Original languageEnglish
Pages (from-to)90-104
Number of pages15
JournalPerform. Eval.
Volume68
Issue number2
DOIs
Publication statusPublished - 2011
Externally publishedYes

Fingerprint

Dive into the research topics of 'The ins and outs of the probabilistic model checker MRMC'. Together they form a unique fingerprint.

Cite this