Changes between Version 12 and Version 13 of WikiStart


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

Making thins beautiful

Legend:

Unmodified
Added
Removed
Modified
  • WikiStart

    v12 v13  
    55[[PageOutline(2-3, Content:, inline)]]
    66
     7----
     8
    79== What is MRMC? ==
    810MRMC 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.
    911
     12----
     13
    1014== A Command-line tool ==
     15
     16[[Image(mrmc_cmd.jpg, align=right, 20%)]]
     17
    1118MRMC is a command-line tool written in C-language. Which allows MRMC to be small and fast.
    1219Currently we support Windows, Linux and Mac OS X platforms.
    1320The tool is distributed under the [http://www.gnu.org/licenses/gpl.html GNU General Public License (GPL)].
    1421
    15 An example of the tool usage may be found below:
     22An example of the tool usage can be found on the righ:
    1623
    17 [[Image(mrmc_cmd.jpg, 30%)]]
     24----
    1825
    1926== ETMCC as a predecessor ==
     
    2229For details on ETMCC consider reading [wiki:HermansKMS_IJSTTT03 HermansKMS_IJSTTT03].
    2330
     31----
     32
    2433== MRMC Tool Architecture ==
    25 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.
    2634
    27 A sketch of the tool architecture can be found below (ToDo: Add the current MRMC architecture!!):
     35[[Image(mrmc_arch.jpg, align=right, 20%)]]
    2836
    29 [[Image(mrmc_arch.jpg, 30%)]]
     37MRMC 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
     44A sketch of the tool architecture can be found on the right.
     45
     46----
    3047
    3148== Implemented Algorithms ==
     
    3451 * 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]
    3552 * 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----
    3655
    3756== Getting MRMC models ==
     
    6079Some more information on generating MRMC models using Prism can be found [http://www.prismmodelchecker.org/manual/RunningPRISM/ExportingTheModel here].
    6180
     81----
     82