Markov Reward Model Checker (MRMC)
From Wikipedia, the free encyclopedia
Contents |
[edit] What is Model Checking?
Please, consider reading: Model checking
[edit] 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.
The official MRMC tool web-page
[edit] Who develops MRMC?
- Formal Methods & Tools (FMT) group at The University of Twente, The Netherlands
- Software Modeling and Verification (MOVES) group at RWTH Aachen University, Germany
[edit] 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 Linux platform only, but on Microsoft Windows it can be built and run under Cygwin. The tool is distributed under the GNU General Public License (GPL).
An example of the tool usage may be found below:
[edit] 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.
[edit] 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 is provided on the picture below:
[edit] Implemented algorithms
MRMC supports:
1. 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.
2. Safe on-the-fly steady-state detection for time-bounded reachability (see time bounded until operator of CSL logic).
3. Bisimulation minimisation for PCTL, CSL, PRCTL and CSRL logics, for the latter two in case without impulse rewards.
[edit] Getting MRMC models
MRMC models can be generated from Prism models, using the command line Prism starting from the version 3.0
The required options of "prism" are listed here and were obtained by running "prism -help":
-exportmrmc .................... When exporting matrices/vectors/labels, use MRMC format
-exportlabels <file> ........... Export the list of labels and satisfying states to a file
-exporttrans <file> ............ Export the transition matrix to a file
-exportstaterewards <file> ..... Export the state rewards vector to a file
-exporttransrewards <file> ...... Export the transition rewards matrix to a file
NOTE: The "transition rewards" are what we refer to as "impulse rewards".
A typical example of generating MRMC model from the Prism model would be:
$ prism model.sm model.csl -exportmrmc -exportlabels model.lab -exporttrans model.tra -exportstaterewards model.rew -exporttransrewards model.rewi
The resulting model.tra, model.lab, model.rew and model.rewi files can be immediately consumed by MRMC.
Some more information on generating MRMC models using Prism can be found here.
[edit] News & Downloads
For more news and information of the MRMC tool please visit the official News page
In order to download the tool please consider visiting the official Downloads page
