MRMC Related

In this sections we are going to list research projects, publications and other data, related to MRMC, and carried out by scientists all over the world.


  1. Projects
  2. Papers
  3. Presentations
  4. Encyclopedia
  5. Model Checking Tools


These are the projects that relate to MRMC:


  • COMPASS: An international research project for developing a theoretical and technological basis for the system-software co-engineering approach focusing on a coherent set of specification and analysis techniques for evaluation of system-level correctness, safety, dependability and performability of on-board computer-based aerospace systems. LINK


  • Quasimodo: A European research project aimed at developing new techniques and tools for model-driven design, analysis, testing and code-generation for advanced embedded systems. LINK
  • Basic Research in Informatics for Creating the Knowledge Society (BRICKS). Project AFM7:MOQS: Modeling and Analysis of QoS for Component-Based Designs. LINK
  • Davide D’Aprile: Timed and Stochastic Model Checking of Petri Nets. PhD Thesis, 2007 PDF
  • Marcel Oldenkamp: Probabilistic model checking, A comparison of tools. Master Thesis, 2007 LINK


  • Tim Kemna: Bisimulation Minimisation and Probabilistic Model Checking. Master Thesis, 2006 PDF
  • Reachability analysis in continuous-time Markov decision processes. Master Thesis, 2006 LINK
  • Mark Kattenbelt: Towards an Explicit-State Model Checking Framework. Master Thesis, 2006 PS
  • Probabilistic Model Checking: Von den Grundlagen zum Tool - ein Vergleich zwischen PRISM und MRMC. Bachelor Thesis, 2006 LINK
  • Heuristics-Guided Dependability Analysis. Bachelor Thesis, 2006 LINK


  • Project Ametist: Analysis and Tools: Tools and Tool Interaction. PDF


These are the papers that reference MRMC:


  • J.-P. Katoen, D. Klink, M. Leucker, and V. Wolf. Three-valued abstraction for continuous-time Markov chains. In proceedings of 19’th International Conference on Computer-Aided Verification (CAV’07), volume 4590 of Lecture Notes in Computer Science, pages 316-329. Springer, 2007 PDF.GZ
  • A. Donaldson, A. Miller and D. Parker. GRIP: Generic Representatives in PRISM. In Proc. 4th International Conference on Quantitative Evaluation of Systems (QEST'07). To appear. September 2007 PDF
  • R. De Nicola, J.-P. Katoen, D. Latella, M. Loreti, M. Massink: Model checking mobile stochastic logic. In Theoretical Computer Science, volume 382, issue 1, pages 42-70, Elsevier Science Publishers Ltd 2007
  • M. Kwiatkowska, G. Norman and D. Parker: Stochastic Model Checking. In Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation, volume 4486 of Lecture Notes in Computer Science (Tutorial Volume), pages 220-270, Springer. to appear, 2007 PDF
  • A. Aldini and M. Bernardo: Mixing Logics and Rewards for the Component-Oriented Specification of Performance Measures, to appear in Theoretical Computer Science PDF


  • D. Cerotti, D. D'Aprile, S. Donatelli and J. Sproston: Verifying Stochastic Well-formed Nets with CSL Model-Checking Tools. ACSD '06 PS.GZ
  • Davide Cerotti, Susanna Donatelli, Andras Horvath and Jeremy Sproston: CSL Model Checking for Generalized Stochastic Petri Nets. QEST '06 PS.GZ
  • Allan Clark and Stephen Gilmore: Evaluating quality of service for service level agreements. FMICS'06 PDF
  • Tamas Suto, Jeremy T. Bradley and William J. Knottenbelt: Performance Trees: A New Approach to Quantitative Performance Specification. MASCOTS '06 PDF
  • Muffy Calder, Stephen Gilmore, Jane Hillston, and Vladislav Vyshemirsky: Formal methods for biochemical signalling pathways. In BCS, 2006. To appear. PDF
  • Husain Aljazzar, Stefan Leue: Extended Directed Search for Probabilistic Timed Reachability. FORMATS'06 PDF
  • Mirco Tribastone and Stephen Gilmore: A New Generation PEPA Workbench. PASTA'06 PDF


These are the presentations that reference MRMC:


  • Probabilistic Model Checking and Reliability of Results. PDF


  • Inexact Arithmetic in Model Checking of DTMCs. PDF
  • A Markov Reward Model Checker & How Fast and Fat is Your Probabilistic Model Checker? PDF


  • Probabilistic Model Checking of Randomized Distributed Protocols using PRISM. PDF


These are the encyclopedia that reference MRMC:

Model Checking Tools

The following model checkers were, at some point, compared against MRMC. For more details see How Fast and Fat Is Your Probabilistic Model Checker? and Chapter 7 of Model Checking Markov Chains: Techniques and Tools.

  • Probabilistic Symbolic Model Checker: PRISM .
  • Erlangen-Twente Markov Chain Checker: ETMCC.
  • Statistical Model-checker and Analyzer for Probabilistic Systems: VESTA.
  • GSMP Model Checker: Ymer.

Since recently, it is no longer possible to download VESTA from its official web site. Therefore, we provide our local copy.

Last modified 10 years ago Last modified on Jun 30, 2008, 12:23:45 PM