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:
- and Mac OS X
platforms. The tool is distributed under the GNU Public License.