Version 16 (modified by Dr. Ivan S. Zapreev, 11 years ago) (diff)

Adding borders to images


Welcome to the Markov Reward Model Checker

A tool developed at the Formal Methods Group, University of Twente and Software Modeling and Verification group at RWTH Aachen University.


  1. What is MRMC?
  2. A Command-line tool
  3. ETMCC as a predecessor
  4. MRMC Tool Architecture
  5. Implemented Algorithms
  6. Getting MRMC models

What is MRMC?

MRMC is a model checker for discrete-time and continuous-time Markov reward models. It supports reward extensions of PCTL and CSL (PRCTL and CSRL), and allows for the automated verification of properties concerning long-run and instantaneous rewards as well as cumulative rewards. In particular, it supports to check the reachability of a set of goal states (by only visiting legal states before) under a time and an accumulated reward constraint.

A Command-line tool

MRMC is a command-line tool written in C-language. Which allows MRMC to be small and fast. Currently we support Windows, Linux and Mac OS X platforms. The tool is distributed under the GNU General Public License (GPL).

An example of the tool usage can be found on the righ:

ETMCC as a predecessor

MRMC is a successor of a well known tool called ETMCC (Erlangen-Twente Markov Chain Checker) . Which is a prototype implementation of a model checker for continuous time Markov chains. ETMCC supports verification techniques to check CSL and aCSL (action based CSL) properties.

For details on ETMCC consider reading HermansKMS_IJSTTT03?.

MRMC Tool Architecture

No image "mrmc_arch.jpg" attached to WikiStart

MRMC is a command-line tool. It accepts the following input files:

  • .tra - file specifying a CTMC or a DTMC,
  • .ctmdpi - file specifying a CTMDP,
  • .lab - file indicating the state-labeling with atomic propositions,
  • .rew - file specifying the state reward structure,
  • .rewi - file specifying the impulse reward structure.

A sketch of the tool architecture can be found on the right.

Implemented Algorithms

MRMC supports

  • Two algorithms for time- and reward bounded until-formulae. One is based on discretization TijmsV_99?, the other on uniformization and path truncation QureshiS_ISFTC96?. This includes state- and impulse rewards. For details on these algorithms we refer to BaierHHK_ICALP00?, ClothKKP_DSN05?, HaverkortCHKB_DSN02?.
  • Safe on-the-fly steady-state detection for time-bounded reachability (see time bounded until operator of CSL logic). PDF? BibTex?
  • Bisimulation minimisation for PCTL, CSL, PRCTL and CSRL logics, for the latter two in case without impulse rewards. PDF? BibTex?

Getting MRMC models

MRMC models can be generated using Prism, starting from the version 3.0. For more information on generating MRMC models, see MRMC Manual.

Attachments (1)

Download all attachments as: .zip