Markov Reward Model Checker (MRMC)
Encyclopedia
The Markov Reward Model Checker (MRMC)http://www.mrmc-tool.org/ 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.
MRMC has been developed by the Formal Methods & Tools (FMT) group at the University of Twente, The Netherlands and the Software Modeling and Verification (MOVES) group at RWTH Aachen University, Germany
under the guidance of Prof. Dr. Ir. Joost-Pieter Katoen.
An example snapshot of the tool usage is provided on the right.
representation. This allows MRMC to be small and fast. The empirical study of MRMC performance in comparison to other model checkers such as PRISM, ETMCC, Vesta, and Ymer is available here.
MRMC is supplied for Linux
, Mac OS X
and Microsoft Windows
(compilable under Cygwin
) platforms. The tool is distributed under the GNU General Public License
(GPL).
MRMC expects five input files:
which have a simple text format. For CSL and PCTL
verification, the latter two files may be omitted. Additionally when working with MDPs, the .tra-file is substituted by the .ctmdpi-file.
The properties of interest, specified in PCTL
, CSL, PRCTL or CSRL are accepted through the command-prompt interface of the tool.
A sketch of the tool architecture is provided on the right.
starting from version 3.0
The required options of "prism" are listed here and were obtained by running "prism -help":
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.
Markov
*Markov, Markova, or Markoff are surnames and may refer to:In academia:*Ivana Markova , Czechoslovak-British emeritus professor of psychology at the University of Stirling...
reward models. It supports reward extensions of PCTL
Probabilistic CTL
Probabilistic Computation Tree Logic is an extension of CTL which allows for probabilistic quantification of described properties. It has been defined in the paper by ....
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.
MRMC has been developed by the Formal Methods & Tools (FMT) group at the University of Twente, The Netherlands and the Software Modeling and Verification (MOVES) group at RWTH Aachen University, Germany
Germany
Germany , officially the Federal Republic of Germany , is a federal parliamentary republic in Europe. The country consists of 16 states while the capital and largest city is Berlin. Germany covers an area of 357,021 km2 and has a largely temperate seasonal climate...
under the guidance of Prof. Dr. Ir. Joost-Pieter Katoen.
An example snapshot of the tool usage is provided on the right.
MRMC details
MRMC is a command-line tool written in the C programming language and based on a sparse matrixSparse matrix
In the subfield of numerical analysis, a sparse matrix is a matrix populated primarily with zeros . The term itself was coined by Harry M. Markowitz....
representation. This allows MRMC to be small and fast. The empirical study of MRMC performance in comparison to other model checkers such as PRISM, ETMCC, Vesta, and Ymer is available here.
MRMC is supplied for Linux
Linux
Linux is a Unix-like computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds...
, Mac OS X
Mac OS X
Mac OS X is a series of Unix-based operating systems and graphical user interfaces developed, marketed, and sold by Apple Inc. Since 2002, has been included with all new Macintosh computer systems...
and Microsoft Windows
Microsoft Windows
Microsoft Windows is a series of operating systems produced by Microsoft.Microsoft introduced an operating environment named Windows on November 20, 1985 as an add-on to MS-DOS in response to the growing interest in graphical user interfaces . Microsoft Windows came to dominate the world's personal...
(compilable under Cygwin
Cygwin
Cygwin is a Unix-like environment and command-line interface for Microsoft Windows. Cygwin provides native integration of Windows-based applications, data, and other system resources with applications, software tools, and data of the Unix-like environment...
) platforms. The tool is distributed under the GNU General Public License
GNU General Public License
The GNU General Public License is the most widely used free software license, originally written by Richard Stallman for the GNU Project....
(GPL).
MRMC expects five input files:
- .tra-file describing the probability or rate matrix,
- .ctmdpi-file describing the rate matrix and indicating the transition-labeling,
- .lab-file indicating the state-labeling with atomic propositions,
- .rew-file specifying the state reward structure,
- .rewi-file specifying the impulse reward structure.
which have a simple text format. For CSL and PCTL
Probabilistic CTL
Probabilistic Computation Tree Logic is an extension of CTL which allows for probabilistic quantification of described properties. It has been defined in the paper by ....
verification, the latter two files may be omitted. Additionally when working with MDPs, the .tra-file is substituted by the .ctmdpi-file.
The properties of interest, specified in PCTL
Probabilistic CTL
Probabilistic Computation Tree Logic is an extension of CTL which allows for probabilistic quantification of described properties. It has been defined in the paper by ....
, CSL, PRCTL or CSRL are accepted through the command-prompt interface of the tool.
A sketch of the tool architecture is provided on the right.
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.Implemented algorithms
Among others, 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).
- Bisimulation minimisation for PCTLProbabilistic CTLProbabilistic Computation Tree Logic is an extension of CTL which allows for probabilistic quantification of described properties. It has been defined in the paper by ....
, CSL, PRCTL and CSRL logics, for the latter two in case without impulse rewards.
Getting MRMC models
MRMC models can be generated from PRISM models, using the command line,starting from 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........... Export the list of labels and satisfying states to a file
-exporttrans............ Export the transition matrix to a file
-exportstaterewards..... Export the state rewards vector to a file
-exporttransrewards...... 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.