Changes between Version 6 and Version 7 of WikiStart


Ignore:
Timestamp:
Jun 17, 2008, 11:58:14 AM (11 years ago)
Author:
Christina Jansen
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • WikiStart

    v6 v7  
    1212
    1313An example of the tool usage may be found below:
    14 [[Image(mrmc_cmd.jpg)]]
     14
     15[[Image(mrmc_cmd.jpg)]]
     16
     17== ETMCC as a predecessor ==
     18MRMC 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.
     19
     20For details on ETMCC consider reading [wiki:HermansKMS_IJSTTT03 HermansKMS_IJSTTT03].
     21
     22== MRMC Tool Architecture ==
     23MRMC 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.
     24
     25A sketch of the tool architecture can be found below:
     26
     27[[Image(mrmc_arch.jpg)]]
    1528
    1629"[wiki:TracAdmin trac-admin] ''yourenvdir'' initenv" created