Skip to content

Markov Reward Model Checker - 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 r…

License

Notifications You must be signed in to change notification settings

ivan-zapreev/MRMC

Repository files navigation

MRMC

Markov Reward Model Checker http://www.mrmc-tool.org/trac/

For years I was the lead developer of the MRMC project. Here are the papers and the presentations created by me, also the test scripts I've created and the source files, the make scripts, including the tool's documentation and etc.

About

Markov Reward Model Checker - 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 r…

Resources

License

Stars

Watchers

Forks

Packages

No packages published