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

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 68 articles )

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

1 2 3 4 next

  1. Bartocci, Ezio; Kovács, Laura; Stankovič, Miroslav: Automatic generation of moment-based invariants for prob-solvable loops (2019)
  2. Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian: Formal reliability analysis of redundancy architectures (2019)
  3. Bakir, Mehmet Emin; Gheorghe, Marian; Konur, Savas; Stannett, Mike: Comparative analysis of statistical model checking tools (2017)
  4. 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)
  5. Esmaeil Zadeh Soudjani, Sadegh; Abate, Alessandro; Majumdar, Rupak: Dynamic Bayesian networks for formal verification of structured stochastic processes (2017)
  6. Feng, Yuan; Zhang, Lijun: Precisely deciding CSL formulas through approximate model checking for CTMCs (2017)
  7. Hölzl, Johannes: Markov chains and Markov decision processes in Isabelle/HOL (2017)
  8. Junges, Sebastian; Guck, Dennis; Katoen, Joost-Pieter; Rensink, Arend; Stoelinga, Mariëlle: Fault trees on a diet: automated reduction by graph rewriting (2017)
  9. Ahmed, Waqar; Hasan, Osman; Tahar, Sofiène: Formal dependability modeling and analysis: a survey (2016)
  10. Bortolussi, Luca; Gast, Nicolas: Mean-field limits beyond ordinary differential equations (2016)
  11. Bortolussi, Luca; Milios, Dimitrios; Sanguinetti, Guido: Smoothed model checking for uncertain continuous-time Markov chains (2016)
  12. Fearnley, John; Rabe, Markus N.; Schewe, Sven; Zhang, Lijun: Efficient approximation of optimal control for continuous-time Markov games (2016)
  13. Hermanns, Holger; Krčál, Jan; Vester, Steen: Distributed synthesis in continuous time (2016)
  14. Vandin, Andrea; Tribastone, Mirco: Quantitative abstractions for collective adaptive systems (2016)
  15. Xu, Ming; Zhang, Lijun; Jansen, David N.; Zhu, Huibiao; Yang, Zongyuan: Multiphase until formulas over Markov reward models: an algebraic approach (2016)
  16. Abate, Alessandro; Soudjani, Sadegh Esmaeil Zadeh: Quantitative approximation of the probability distribution of a Markov process by formal abstractions (2015)
  17. 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) ioport
  18. Biscaia, M.; Henriques, D.; Mateus, P.: Decidability of approximate Skolem problem and applications to logical verification of dynamical properties of Markov chains (2015)
  19. Dannenberg, Frits; Hahn, Ernst Moritz; Kwiatkowska, Marta: Computing cumulative rewards using fast adaptive uniformization (2015)
  20. Noll, Thomas: Safety, dependability and performance analysis of aerospace systems (2015) ioport

1 2 3 4 next


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