Abstract
| Original language | Undefined |
|---|---|
| Title of host publication | 2nd Int. Conf. on Quantitative Evaluation of Systems |
| Place of Publication | Los Alamitos, California |
| Publisher | IEEE Computer Society |
| 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 Sep 2005 → 22 Sep 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 | Italy |
| City | Turin |
| Period | 19/09/05 → 22/09/05 |
| Internet address |
Keywords
- EWI-1545
- IR-54782
- METIS-229271
Cite this
}
A Markov reward model checker. / Katoen, Joost P.; Maneesh Khattri, M.; Zapreev, I.S.; Zapreev, I.S.
2nd Int. Conf. on Quantitative Evaluation of Systems. Los Alamitos, California : IEEE Computer Society, 2005. p. 243-245.Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
TY - GEN
T1 - A Markov reward model checker
AU - Katoen, Joost P.
AU - Maneesh Khattri, M.
AU - Zapreev, I.S.
AU - Zapreev, I.S.
N1 - eemcs1545
PY - 2005
Y1 - 2005
N2 - 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.
AB - 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.
KW - EWI-1545
KW - IR-54782
KW - METIS-229271
U2 - 10.1109/QEST.2005.2
DO - 10.1109/QEST.2005.2
M3 - Conference contribution
SN - 0 7695 2427 3
SP - 243
EP - 245
BT - 2nd Int. Conf. on Quantitative Evaluation of Systems
PB - IEEE Computer Society
CY - Los Alamitos, California
ER -