What is MRMC?

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

Downloads

For binaries (Windows, Linux and MacOS) and the sources for versions 1.0b to 1.5 (latest), head to our Downloads folder.

Test Suites

  • For MRMC 1.5 (53MB): [Download] md5sum: cb8a55b4c826fa4971b0c514c050f7a2
  • For MRMC 1.4.1 (50MB): [Download] md5sum: 96a882b5dcdacfb68e4faf7a71b3108d
  • For MRMC 1.4 (48.8MB): [Download] md5sum: 15e9687359d7b0e66d908a6cef580db0
  • For MRMC 1.3 (48.8MB): [Download] md5sum: ca99fa3c8523256cb9d6bc3c47cf5eaf

Related Patches

  • For MRMC 1.5: David N. Jansen's patch for a new sparse matrix data structure: optimized for bisimulation minimisation. This patch may cause a performance hit in the simulation engine.

    To apply this patch, download the source distribution of version 1.5 and this patch, go to the directory where you placed the source distribution and call patch from your shell with a command like:

    cd ..../mrmc_src_v1.5
patch -p0 < mrmc-1.5-alternate-matrix.patch

    After that, continue compiling MRMC with make all as usual.

Impressum & Contact

See our contact page.