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.


References in zbMATH (referenced in 73 articles )

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

1 2 3 4 next

  1. Pandya, Paritosh K.; Wakankar, Amol: Specification and optimal reactive synthesis of run-time enforcement shields (2022)
  2. Stankovič, Miroslav; Bartocci, Ezio; Kovács, Laura: Moment-based analysis of Bayesian network properties (2022)
  3. Cardelli, Luca; Grosu, Radu; Larsen, Kim G.; Tribastone, Mirco; Tschaikowski, Max; Vandin, Andrea: Lumpability for uncertain continuous-time Markov chains (2021)
  4. Mathur, Umang; Bauer, Matthew S.; Chadha, Rohit; Sistla, A. Prasad; Viswanathan, Mahesh: Exact quantitative probabilistic model checking through rational search (2020)
  5. Bartocci, Ezio; Kovács, Laura; Stankovič, Miroslav: Automatic generation of moment-based invariants for prob-solvable loops (2019)
  6. Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian: Formal reliability analysis of redundancy architectures (2019)
  7. Drechsler, Rolf (ed.): Formal system verification. State-of the-art and future trends (2018)
  8. Bakir, Mehmet Emin; Gheorghe, Marian; Konur, Savas; Stannett, Mike: Comparative analysis of statistical model checking tools (2017)
  9. Bohy, Aaron; Bruyère, Véronique; Raskin, Jean-François; Bertrand, Nathalie: Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes (2017)
  10. Esmaeil Zadeh Soudjani, Sadegh; Abate, Alessandro; Majumdar, Rupak: Dynamic Bayesian networks for formal verification of structured stochastic processes (2017)
  11. Feng, Yuan; Zhang, Lijun: Precisely deciding CSL formulas through approximate model checking for CTMCs (2017)
  12. Hölzl, Johannes: Markov chains and Markov decision processes in Isabelle/HOL (2017)
  13. Junges, Sebastian; Guck, Dennis; Katoen, Joost-Pieter; Rensink, Arend; Stoelinga, Mariëlle: Fault trees on a diet: automated reduction by graph rewriting (2017)
  14. Ahmed, Waqar; Hasan, Osman; Tahar, Sofiène: Formal dependability modeling and analysis: a survey (2016)
  15. Bortolussi, Luca; Gast, Nicolas: Mean-field limits beyond ordinary differential equations (2016)
  16. Bortolussi, Luca; Milios, Dimitrios; Sanguinetti, Guido: Smoothed model checking for uncertain continuous-time Markov chains (2016)
  17. Fearnley, John; Rabe, Markus N.; Schewe, Sven; Zhang, Lijun: Efficient approximation of optimal control for continuous-time Markov games (2016)
  18. Hermanns, Holger; Krčál, Jan; Vester, Steen: Distributed synthesis in continuous time (2016)
  19. Vandin, Andrea; Tribastone, Mirco: Quantitative abstractions for collective adaptive systems (2016)
  20. Xu, Ming; Zhang, Lijun; Jansen, David N.; Zhu, Huibiao; Yang, Zongyuan: Multiphase until formulas over Markov reward models: an algebraic approach (2016)

1 2 3 4 next


Further publications can be found at: http://mrmc-tool.org/trac/wiki/Bibliography