wiki:WikiStart

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.


Last modified 8 years ago Last modified on Nov 13, 2008, 1:11:41 PM

Attachments (1)

Download all attachments as: .zip