[[TracNav(nocollapse|noreorder)]]

= What is MRMC? =

[[Image(http://www.mrmc-tool.org/images/house.gif, nolink, align=right, 25%)]]

'''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 [http://www.gnu.org/licenses/gpl.html GNU Public License].

''A Video Tutorial (Flash) about MRMC'' can be found below. ''A static snapshot of the tool usage'' can be found [attachment:mrmc_cmd.jpg here], for more details, consider visiting the [wiki:Specifications Specifications] page.

{{{
#!html
<center>
<embed src="http://blip.tv/play/AcbPPgA" type="application/x-shockwave-flash" width="672" height="494" allowscriptaccess="always" allowfullscreen="true"></embed><center>												
}}}

----