Welcome to the Markov Reward Model Checker

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 may be found below:

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

MRMC is a command-line tool, and expects four input files: a .tra-file describing the probability or rate matrix, a .lab-file indicating the state-labeling with atomic propositions, a .rew-file specifying the state reward structure, and a .rewi-file specifying the impulse reward structure. For CSL and PCTL verification, the latter two files may be omitted.

A sketch of the tool architecture can be found below (ToDo?: Add the current MRMC architecture!!):

Error: Macro Image(mrmc_arch.jpg) failed

Attachment 'wiki:WikiStart: mrmc_arch.jpg' does not exist.

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?

"trac-admin yourenvdir initenv" created a new Trac environment, containing a default set of wiki pages and some sample data. This newly created environment also contains documentation to help you get started with your project.

You can use trac-admin to configure  Trac to better fit your project, especially in regard to components, versions and milestones.

TracGuide is a good place to start.

Enjoy!
The Trac Team

Starting Points

• TracGuide -- Built-in Documentation
•  The Trac project -- Trac Open Source Project
•  Trac FAQ -- Frequently Asked Questions
• TracSupport -- Trac Support

For a complete list of local wiki pages, see TitleIndex.