Version 21 (modified by Dr. Ivan S. Zapreev, 11 years ago) (diff)



Welcome to the MRMC home page

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


  1. What is MRMC?
  2. Getting MRMC models
  3. ETMCC as a predecessor

What is MRMC?

MRMC is a command-line 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).

The tool is written in C and supports verification of:

  • 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.

MRMC is available for the following platforms:

  • 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 above.

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 CTMC model checker supporting CSL and aCSL properties.

Attachments (1)

Download all attachments as: .zip