wiki:WikiStart

Version 7 (modified by Christina Jansen, 11 years ago) (diff)

--

TracNav?

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:

No image "mrmc_arch.jpg" attached to WikiStart

"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

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

Attachments (1)

Download all attachments as: .zip