Abstract
This short tool paper introduces MRMC, a model checker for discrete-time and continuous-time Markov reward models. It supports reward extensions of PCTL and CSL, 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. Several numerical algorithms and extensions thereof are included in MRMC.
Original language | Undefined |
---|---|
Title of host publication | 2nd Int. Conf. on Quantitative Evaluation of Systems |
Place of Publication | Los Alamitos, California |
Publisher | IEEE |
Pages | 243-245 |
Number of pages | 3 |
ISBN (Print) | 0 7695 2427 3 |
DOIs | |
Publication status | Published - 2005 |
Event | 2nd International Conference on the Quantitative Evaluation of Systems, QEST 2005 - Torino Incontra Conference Centre, Turin, Italy Duration: 19 Sept 2005 → 22 Sept 2005 Conference number: 2 http://www.qest.org/qest2005/ |
Publication series
Name | |
---|---|
Publisher | IEEE CS Press |
Conference
Conference | 2nd International Conference on the Quantitative Evaluation of Systems, QEST 2005 |
---|---|
Abbreviated title | QEST |
Country/Territory | Italy |
City | Turin |
Period | 19/09/05 → 22/09/05 |
Internet address |
Keywords
- EWI-1545
- IR-54782
- METIS-229271