|Version 16 (modified by ivan.zapreev, 5 years ago)|
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.
- What is MRMC?
- A Command-line tool
- ETMCC as a predecessor
- MRMC Tool Architecture
- Implemented Algorithms
- 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
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.
- 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?