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 (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  GNU Public License.

A Video Tutorial (Flash) about MRMC can be found below. A static snapshot of the tool usage can be found here, for more details, consider visiting the Specifications page.

---