The Ins and Outs of the Probabilistic Model Checker MRMC

Author

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

Author_Institution

RWTH Aachen Univ., Aachen, Germany

fYear

2009

fDate

13-16 Sept. 2009

Firstpage

167

Lastpage

176

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.

Keywords

Markov processes; minimisation; probability; program verification; reachability analysis; software tools; trees (mathematics); MRMC probabilistic model checker; Markov reward model checker; automated verification property; bisimulation minimization; discrete-event simulation; probabilistic computation tree logic; reward-bounded reachability probability; software tool; steady-state detection; time reachability probability; Computer vision; Discrete event simulation; Engines; IEC standards; Performance analysis; Probabilistic logic; Reachability analysis; Software tools; Steady-state; Testing; none;

fLanguage

English

Publisher

ieee

Conference_Titel

Quantitative Evaluation of Systems, 2009. QEST '09. Sixth International Conference on the

Conference_Location

Budapest

Print_ISBN

978-0-7695-3808-2

Type

conf

DOI

10.1109/QEST.2009.11

Filename

5290843