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.

References in zbMATH (referenced in 45 articles )

Showing results 1 to 20 of 45.
Sorted by year (citations)

1 2 3 next

  1. Bortolussi, Luca; Milios, Dimitrios; Sanguinetti, Guido: Smoothed model checking for uncertain continuous-time Markov chains (2016)
  2. Fearnley, John; Rabe, Markus N.; Schewe, Sven; Zhang, Lijun: Efficient approximation of optimal control for continuous-time Markov games (2016)
  3. Xu, Ming; Zhang, Lijun; Jansen, David N.; Zhu, Huibiao; Yang, Zongyuan: Multiphase until formulas over Markov reward models: an algebraic approach (2016)
  4. Abate, Alessandro; Soudjani, Sadegh Esmaeil Zadeh: Quantitative approximation of the probability distribution of a Markov process by formal abstractions (2015)
  5. 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)
  6. Noll, Thomas: Safety, dependability and performance analysis of aerospace systems (2015)
  7. Aarts, Fides; Kuppens, Harco; Tretmans, Jan; Vaandrager, Frits; Verwer, Sicco: Improving active Mealy machine learning for protocol conformance testing (2014)
  8. Konur, Savas; Fisher, Michael; Dobson, Simon; Knox, Stephen: Formal verification of a pervasive messaging system (2014)
  9. Tkachev, Ilya; Abate, Alessandro: Characterization and computation of infinite-horizon specifications over Markov processes (2014)
  10. Turrini, Andrea; Hermanns, Holger: Cost preserving bisimulations for probabilistic automata (2014)
  11. Wimmer, Ralf; Jansen, Nils; Ábrahám, Erika; Katoen, Joost-Pieter; Becker, Bernd: Minimal counterexamples for linear-time probabilistic verification (2014)
  12. Gao, Yang; Hahn, Ernst Moritz; Zhan, Naijun; Zhang, Lijun: CCMC: a conditional CSL model checker for continuous-time Markov chains (2013)
  13. Kiefer, Stefan; Murawski, Andrzej S.; Ouaknine, Joël; Wachter, Björn; Worrell, James: Algorithmic probabilistic game semantics. Playing games with automata (2013)
  14. Norman, Gethin; Parker, David; Sproston, Jeremy: Model checking for probabilistic timed automata (2013)
  15. Barbot, Beno{^i}t; Haddad, Serge; Picaronny, Claudine: Coupling and importance sampling for statistical model checking (2012)
  16. Filieri, Antonio; Ghezzi, Carlo; Tamburrelli, Giordano: A formal approach to adaptive software: continuous assurance of non-functional requirements (2012)
  17. Katoen, Joost-Pieter: Model checking: one can do much more than you think! (2012)
  18. Katoen, Joost-Pieter; Klink, Daniel; Leucker, Martin; Wolf, Verena: Three-valued abstraction for probabilistic systems (2012)
  19. Larsen, Kim G.: Statistical model checking, refinement checking, optimization, $\cdots$ for stochastic hybrid systems (2012)
  20. Zhang, Lijun; Jansen, David N.; Nielson, Flemming; Hermanns, Holger: Efficient CSL model checking using stratification (2012)

1 2 3 next

Further publications can be found at: