A Markov reward model checker

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

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

169 Citations (Scopus)
55 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 languageUndefined
Title of host publication2nd Int. Conf. on Quantitative Evaluation of Systems
Place of PublicationLos Alamitos, California
PublisherIEEE Computer Society
Pages243-245
Number of pages3
ISBN (Print)0 7695 2427 3
DOIs
Publication statusPublished - 2005
Event2nd International Conference on the Quantitative Evaluation of Systems, QEST 2005 - Torino Incontra Conference Centre, Turin, Italy
Duration: 19 Sep 200522 Sep 2005
Conference number: 2
http://www.qest.org/qest2005/

Publication series

Name
PublisherIEEE CS Press

Conference

Conference2nd International Conference on the Quantitative Evaluation of Systems, QEST 2005
Abbreviated titleQEST
CountryItaly
CityTurin
Period19/09/0522/09/05
Internet address

Keywords

  • EWI-1545
  • IR-54782
  • METIS-229271

Cite this

Katoen, J. P., Maneesh Khattri, M., Zapreev, I. S., & Zapreev, I. S. (2005). A Markov reward model checker. In 2nd Int. Conf. on Quantitative Evaluation of Systems (pp. 243-245). Los Alamitos, California: IEEE Computer Society. https://doi.org/10.1109/QEST.2005.2
Katoen, Joost P. ; Maneesh Khattri, M. ; Zapreev, I.S. ; Zapreev, I.S. / A Markov reward model checker. 2nd Int. Conf. on Quantitative Evaluation of Systems. Los Alamitos, California : IEEE Computer Society, 2005. pp. 243-245
@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",
year = "2005",
doi = "10.1109/QEST.2005.2",
language = "Undefined",
isbn = "0 7695 2427 3",
publisher = "IEEE Computer Society",
pages = "243--245",
booktitle = "2nd Int. Conf. on Quantitative Evaluation of Systems",
address = "United States",

}

Katoen, JP, Maneesh Khattri, M, Zapreev, IS & Zapreev, IS 2005, A Markov reward model checker. in 2nd Int. Conf. on Quantitative Evaluation of Systems. IEEE Computer Society, Los Alamitos, California, pp. 243-245, 2nd International Conference on the Quantitative Evaluation of Systems, QEST 2005, Turin, Italy, 19/09/05. https://doi.org/10.1109/QEST.2005.2

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 proceedingConference contributionAcademicpeer-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 -

Katoen JP, Maneesh Khattri M, Zapreev IS, Zapreev IS. A Markov reward model checker. In 2nd Int. Conf. on Quantitative Evaluation of Systems. Los Alamitos, California: IEEE Computer Society. 2005. p. 243-245 https://doi.org/10.1109/QEST.2005.2