A Markov reward model checker

Joost P. Katoen; M. Maneesh Khattri; I.S. Zapreev; I.S. Zapreev

doi:10.1109/QEST.2005.2

A Markov reward model checker

Joost P. Katoen, M. Maneesh Khattri, I.S. Zapreev, I.S. Zapreev

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

191 Citations (Scopus)

223 Downloads (Pure)

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	https://doi.org/10.1109/QEST.2005.2
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	http://www.qest.org/qest2005/

Keywords

EWI-1545
IR-54782
METIS-229271

Access to Document

10.1109/QEST.2005.2

http://doi.ieeecomputersociety.org/10.1109/QEST.2005.2

Cite this

@inproceedings{9aeb2cd33d0a4038ba201aa53bc9f810,

title = "A Markov reward model checker",

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.",

keywords = "EWI-1545, IR-54782, METIS-229271",

author = "Katoen, {Joost P.} and {Maneesh Khattri}, M. and I.S. Zapreev and I.S. Zapreev",

note = "eemcs1545 ; 2nd International Conference on the Quantitative Evaluation of Systems, QEST 2005 ; Conference date: 19-09-2005 Through 22-09-2005",

year = "2005",

doi = "10.1109/QEST.2005.2",

language = "Undefined",

isbn = "0 7695 2427 3",

publisher = "IEEE",

pages = "243--245",

booktitle = "2nd Int. Conf. on Quantitative Evaluation of Systems",

address = "United States",

url = "http://www.qest.org/qest2005/",

}

TY - GEN

T1 - A Markov reward model checker

AU - Katoen, Joost P.

AU - Maneesh Khattri, M.

AU - Zapreev, I.S.

N1 - Conference code: 2

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

CY - Los Alamitos, California

T2 - 2nd International Conference on the Quantitative Evaluation of Systems, QEST 2005

Y2 - 19 September 2005 through 22 September 2005

ER -