Version 18 (modified by Dr. Ivan S. Zapreev, 10 years ago) (diff)



Welcome to the Markov Reward Model Checker

A tool developed at the Formal Methods Group, University of Twente and Software Modeling and Verification group at RWTH Aachen University.

If you are looking for detailed information about MRMC, see MRMC Manual.


  1. What is MRMC?
  2. A Command-line tool
  3. Getting MRMC models
  4. ETMCC as a predecessor

What is MRMC?

MRMC is a model checker for:

  • Discrete time Markov chains (DTMCs),
  • Continuous time Markov chains (CTMCs),
  • Discrete time Markov Reward models (DMRMs),
  • Continuous time Markov Reward models (CMRMs),
  • Continuous time Markov decision processes (CTMDPIs1).

Hence, MRMC supports:

  • Probabilistic Computation Tree Logic (PCTL),
  • Continuous Stochastic Logic (CSL),
  • Probabilistic Reward Computation Tree Logic (PRCTL),
  • Continuous Stochastic Reward Logic (CSRL).

MRMC allows for numerical model checking on all types of input models. In addition, verification of CSL properties on CTMCs can be done using model checking by Discrete Event Simulation.

A Command-line tool

MRMC is a command-line tool written in C-language. This allows MRMC to be small and fast. Currently, the supported platforms are:

  • Windows,
  • Linux,
  • Mac OS X.

The tool is distributed under the GNU General Public License (GPL).

An example of the tool usage can be found on the righ:

Getting MRMC models

MRMC models can be generated using Prism, starting from the version 3.0.

ETMCC as a predecessor

MRMC was inspired by a well known tool called Erlangen-Twente Markov Chain Checker (ETMCC), which is a CTMCs model checker supporting CSL and aCSL properties.

Attachments (1)

Download all attachments as: .zip