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



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:

"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.

The Trac Team

Starting Points

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

Attachments (1)

Download all attachments as: .zip