|Version 7 (modified by christinajansen, 5 years ago)|
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:
"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.
TracGuide is a good place to start.
The Trac Team
- 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.