Changes between Version 16 and Version 17 of WikiStart


Ignore:
Timestamp:
Jun 18, 2008, 4:54:43 PM (11 years ago)
Author:
Dr. Ivan S. Zapreev
Comment:

Too much information is too bad, remove the unnecessary thins, It is all in the manual.

Legend:

Unmodified
Added
Removed
Modified
  • WikiStart

    v16 v17  
    22
    33= Welcome to the Markov Reward Model Checker =
    4 A tool developed at the Formal Methods Group, University of Twente and Software Modeling and Verification group at RWTH Aachen University.
     4
     5A tool developed at the Formal Methods Group, University
     6of Twente and Software Modeling and Verification group at
     7RWTH Aachen University.
     8
     9If you are looking for detailed information about MRMC,
     10please consider reading [wiki:Specifications MRMC Manual].
     11
    512[[PageOutline(2-3, Content:, inline)]]
    613
     
    815
    916== What is MRMC? ==
    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
     18MRMC 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
     25Hence, 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
     31MRMC allows for numerical model checking on all types of
     32input models. In addition, verification of CSL properties
     33on CTMCs can be done using model checking by Discrete Event
     34Simulation.
    1135
    1236----
     
    1640[[Image(mrmc_cmd.jpg, border=1, align=right, 20%)]]
    1741
    18 MRMC is a command-line tool written in C-language. Which allows MRMC to be small and fast.
    19 Currently we support Windows, Linux and Mac OS X platforms.
     42MRMC is a command-line tool written in C-language. This allows
     43MRMC to be small and fast. Currently, the supported platforms are:
     44
     45 * Windows,
     46 * Linux,
     47 * Mac OS X.
     48
    2049The tool is distributed under the [http://www.gnu.org/licenses/gpl.html GNU General Public License (GPL)].
    2150
     
    2453----
    2554
    26 == ETMCC as a predecessor ==
    27 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.
     55== Getting MRMC models ==
    2856
    29 For details on ETMCC consider reading [wiki:HermansKMS_IJSTTT03 HermansKMS_IJSTTT03].
     57MRMC models can be generated using [http://www.prismmodelchecker.org/ Prism],
     58starting from the version 3.0.
    3059
    3160----
    3261
    33 == MRMC Tool Architecture ==
     62== ETMCC as a predecessor ==
    3463
    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.
     64MRMC 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.
    4565
    4666----
    4767
    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