MRMC
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 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.
Keywords for this software
References in zbMATH (referenced in 46 articles )
Showing results 1 to 20 of 46.
Sorted by year (- Esmaeil Zadeh Soudjani, Sadegh; Abate, Alessandro; Majumdar, Rupak: Dynamic Bayesian networks for formal verification of structured stochastic processes (2017)
- Bortolussi, Luca; Milios, Dimitrios; Sanguinetti, Guido: Smoothed model checking for uncertain continuous-time Markov chains (2016)
- Fearnley, John; Rabe, Markus N.; Schewe, Sven; Zhang, Lijun: Efficient approximation of optimal control for continuous-time Markov games (2016)
- Xu, Ming; Zhang, Lijun; Jansen, David N.; Zhu, Huibiao; Yang, Zongyuan: Multiphase until formulas over Markov reward models: an algebraic approach (2016)
- Abate, Alessandro; Soudjani, Sadegh Esmaeil Zadeh: Quantitative approximation of the probability distribution of a Markov process by formal abstractions (2015)
- Baier, Christel; Daum, Marcus; Engel, Benjamin; Härtig, Hermann; Klein, Joachim; Klüppelholz, Sascha; Märcker, Steffen; Tews, Hendrik; Völp, Marcus: Locks: picking key methods for a scalable quantitative analysis (2015)
- Noll, Thomas: Safety, dependability and performance analysis of aerospace systems (2015)
- Aarts, Fides; Kuppens, Harco; Tretmans, Jan; Vaandrager, Frits; Verwer, Sicco: Improving active Mealy machine learning for protocol conformance testing (2014)
- Konur, Savas; Fisher, Michael; Dobson, Simon; Knox, Stephen: Formal verification of a pervasive messaging system (2014)
- Tkachev, Ilya; Abate, Alessandro: Characterization and computation of infinite-horizon specifications over Markov processes (2014)
- Turrini, Andrea; Hermanns, Holger: Cost preserving bisimulations for probabilistic automata (2014)
- Wimmer, Ralf; Jansen, Nils; Ábrahám, Erika; Katoen, Joost-Pieter; Becker, Bernd: Minimal counterexamples for linear-time probabilistic verification (2014)
- Gao, Yang; Hahn, Ernst Moritz; Zhan, Naijun; Zhang, Lijun: CCMC: a conditional CSL model checker for continuous-time Markov chains (2013)
- Kiefer, Stefan; Murawski, Andrzej S.; Ouaknine, Joël; Wachter, Björn; Worrell, James: Algorithmic probabilistic game semantics. Playing games with automata (2013)
- Norman, Gethin; Parker, David; Sproston, Jeremy: Model checking for probabilistic timed automata (2013)
- Barbot, Beno^ıt; Haddad, Serge; Picaronny, Claudine: Coupling and importance sampling for statistical model checking (2012)
- Filieri, Antonio; Ghezzi, Carlo; Tamburrelli, Giordano: A formal approach to adaptive software: continuous assurance of non-functional requirements (2012)
- Katoen, Joost-Pieter: Model checking: one can do much more than you think! (2012)
- Katoen, Joost-Pieter; Klink, Daniel; Leucker, Martin; Wolf, Verena: Three-valued abstraction for probabilistic systems (2012)
- Larsen, Kim G.: Statistical model checking, refinement checking, optimization, $\cdots$ for stochastic hybrid systems (2012)
Further publications can be found at: http://mrmc-tool.org/trac/wiki/Bibliography