wiki:WikiStart

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

minor fixes

noreorder)?

What is MRMC?

http://www.mrmc-tool.org/images/house.gif

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 (CTMDPIs).

The tool 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,
  • Model checking by Discrete Event Simulation on CTMCs,
  • Formula-dependent and formula-independent bisimulation.

MRMC is a command-line tool, written in C. It is available for:

  • Windows,
  • Linux,
  • and Mac OS X

platforms. The tool is distributed under the GPL License.

An example of the tool usage can be found on the right. If you are looking for detailed information about MRMC, consider reading the MRMC Manual.


Attachments (1)

Download all attachments as: .zip