Changes between Version 7 and Version 8 of WikiStart


Ignore:
Timestamp:
Jun 17, 2008, 12:08:25 PM (11 years ago)
Author:
Christina Jansen
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • WikiStart

    v7 v8  
    2323MRMC 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.
    2424
    25 A sketch of the tool architecture can be found below:
     25A sketch of the tool architecture can be found below (ToDo: Add the current MRMC architecture!!):
    2626
    2727[[Image(mrmc_arch.jpg)]]
     28
     29== Implemented Algorithms ==
     30MRMC supports
     31 * 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].
     32 * 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]
     33 * 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]
    2834
    2935"[wiki:TracAdmin trac-admin] ''yourenvdir'' initenv" created