The ins and outs of the probabilistic model checker MRMC

Joost P. Katoen; I.S. Zapreev; Ernst Moritz Hahn; H. Hermanns; D.N. Jansen

doi:10.1016/j.peva.2010.04.001

The ins and outs of the probabilistic model checker MRMC

Joost P. Katoen, I.S. Zapreev, Ernst Moritz Hahn, H. Hermanns, D.N. Jansen

Research output: Contribution to journal › Article › Academic › peer-review

171 Citations (Scopus)

35 Downloads (Pure)

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.

Original language	English
Pages (from-to)	90-104
Number of pages	15
Journal	Performance evaluation
Volume	68
Issue number	2
DOIs	https://doi.org/10.1016/j.peva.2010.04.001
Publication status	Published - Feb 2011

Keywords

EWI-21246
Markov chains
Model Checking
DTMC
Discrete Event Simulation
MRM
METIS-285230
IR-79364
CTMDP
CTMC
Bisimulation minimization
Numerical analysis

Access to Document

10.1016/j.peva.2010.04.001

Cite this

@article{eaa683f2d0544e88941716bdcc1fde3a,

title = "The ins and outs of the probabilistic model checker MRMC",

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{\textquoteright}s current status and its implementation details.",

keywords = "EWI-21246, Markov chains, Model Checking, DTMC, Discrete Event Simulation, MRM, METIS-285230, IR-79364, CTMDP, CTMC, Bisimulation minimization, Numerical analysis",

author = "Katoen, {Joost P.} and I.S. Zapreev and Hahn, {Ernst Moritz} and H. Hermanns and D.N. Jansen",

year = "2011",

month = feb,

doi = "10.1016/j.peva.2010.04.001",

language = "English",

volume = "68",

pages = "90--104",

journal = "Performance evaluation",

issn = "0166-5316",

publisher = "Elsevier B.V.",

number = "2",

}

TY - JOUR

T1 - The ins and outs of the probabilistic model checker MRMC

AU - Katoen, Joost P.

AU - Zapreev, I.S.

AU - Hahn, Ernst Moritz

AU - Hermanns, H.

AU - Jansen, D.N.

PY - 2011/2

Y1 - 2011/2

N2 - 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.

AB - 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.

KW - EWI-21246

KW - Markov chains

KW - Model Checking

KW - DTMC

KW - Discrete Event Simulation

KW - MRM

KW - METIS-285230

KW - IR-79364

KW - CTMDP

KW - CTMC

KW - Bisimulation minimization

KW - Numerical analysis

U2 - 10.1016/j.peva.2010.04.001

DO - 10.1016/j.peva.2010.04.001

M3 - Article

SN - 0166-5316

VL - 68

SP - 90

EP - 104

JO - Performance evaluation

JF - Performance evaluation

IS - 2

ER -

The ins and outs of the probabilistic model checker MRMC

Abstract

Keywords

Access to Document

Fingerprint

Cite this