wiki:WikiStart

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

Damn, may be this is too concise but this is what people need to know at first.

TracNav?

Welcome to the MRMC home page

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 GPL License. An example of the tool usage can be found above. If you are looking for detailed information about MRMC, consider reading the MRMC Manual.


Attachments (1)

Download all attachments as: .zip