wiki:WikiStart

Version 44 (modified by Viet Yen Nguyen, 10 years ago) (diff)

--

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 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.


Attachments (1)

Download all attachments as: .zip