|Version 25 (modified by ivan.zapreev, 5 years ago)|
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 (CTMDPIs).
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:
- Mac OS X.