10 | | 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. |
| 17 | |
| 18 | MRMC is a model checker for: |
| 19 | * Discrete time Markov chains (DTMCs), |
| 20 | * Continuous time Markov chains (CTMCs), |
| 21 | * Discrete time Markov Reward models (DMRMs), |
| 22 | * Continuous time Markov Reward models (CMRMs), |
| 23 | * Continuous time Markov decision processes (CTMDPIs1). |
| 24 | |
| 25 | Hence, MRMC supports: |
| 26 | * Probabilistic Computation Tree Logic (PCTL), |
| 27 | * Continuous Stochastic Logic (CSL), |
| 28 | * Probabilistic Reward Computation Tree Logic (PRCTL), |
| 29 | * Continuous Stochastic Reward Logic (CSRL). |
| 30 | |
| 31 | MRMC allows for numerical model checking on all types of |
| 32 | input models. In addition, verification of CSL properties |
| 33 | on CTMCs can be done using model checking by Discrete Event |
| 34 | Simulation. |
35 | | [[Image(mrmc_arch.jpg, border=1, align=right, 20%)]] |
36 | | |
37 | | MRMC is a command-line tool. It accepts the following input files: |
38 | | * '''.tra''' - file specifying a CTMC or a DTMC, |
39 | | * '''.ctmdpi''' - file specifying a CTMDP, |
40 | | * '''.lab''' - file indicating the state-labeling with atomic propositions, |
41 | | * '''.rew''' - file specifying the state reward structure, |
42 | | * '''.rewi''' - file specifying the impulse reward structure. |
43 | | |
44 | | A sketch of the tool architecture can be found on the right. |
| 64 | MRMC was inspired by a well known tool called [http://www7.informatik.uni-erlangen.de/etmcc/ Erlangen-Twente Markov Chain Checker (ETMCC)], which is a CTMCs model checker supporting CSL and aCSL properties. |
48 | | == Implemented Algorithms == |
49 | | MRMC supports |
50 | | * Two algorithms for time- and reward bounded until-formulae. One is based on discretization [wiki:TijmsV_99 TijmsV_99], the other on uniformization and path truncation [wiki:QureshiS_ISFTC96 QureshiS_ISFTC96]. This includes state- and impulse rewards. For details on these algorithms we refer to [wiki:BaierHHK_ICALP00 BaierHHK_ICALP00], [wiki:ClothKKP_DSN05 ClothKKP_DSN05], [wiki:HaverkortCHKB_DSN02 HaverkortCHKB_DSN02]. |
51 | | * Safe on-the-fly steady-state detection for time-bounded reachability (see time bounded until operator of CSL logic). [wiki:KatoenZ_QEST06_pdf PDF] [wiki:KatoenZ_QEST06 BibTex] |
52 | | * Bisimulation minimisation for PCTL, CSL, PRCTL and CSRL logics, for the latter two in case without impulse rewards. [wiki:KatoenKZJ_TACAS_pdf PDF] [wiki:KatoenKZJ_TACAS BibTex] |
53 | | |
54 | | ---- |
55 | | |
56 | | == Getting MRMC models == |
57 | | MRMC models can be generated using [http://www.prismmodelchecker.org/ Prism], |
58 | | starting from the version 3.0. For more information on generating MRMC models, |
59 | | see [wiki:Specifications MRMC Manual]. |
60 | | |
61 | | ---- |
62 | | |