loading...
A Markov Reward Model Checker
Torino, Italy September 19-September 22
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/QEST.2005.2Second International Conference on th ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ASCII Text
x 
 
Joost-Pieter Katoen, Maneesh Khattri, Ivan S. Zapreev, "A Markov Reward Model Checker," Quantitative Evaluation of Systems, International Conference on, pp. 243-244, Second International Conference on the Quantitative Evaluation of Systems (QEST'05), 2005.
 
 
BibTex
x
 
@article{ 10.1109/QEST.2005.2,
author = {Joost-Pieter Katoen and Maneesh Khattri and Ivan S. Zapreev},
title = {A Markov Reward Model Checker},
journal ={Quantitative Evaluation of Systems, International Conference on},
volume = {0},
year = {2005},
isbn = {0-7695-2427-3},
pages = {243-244},
doi = {http://doi.ieeecomputersociety.org/10.1109/QEST.2005.2},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Quantitative Evaluation of Systems, International Conference on
TI - A Markov Reward Model Checker
SN - 0-7695-2427-3
SP243
EP244
A1 - Joost-Pieter Katoen,
A1 - Maneesh Khattri,
A1 - Ivan S. Zapreev,
PY - 2005
KW - null
VL - 0
JA - Quantitative Evaluation of Systems, International Conference on
ER -
 
Joost-Pieter Katoen, RWTH Aachen, , Germany
Maneesh Khattri, University of Twente, Netherlands
Ivan S. Zapreev, University of Twente, Netherlands
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.
Citation:
Joost-Pieter Katoen, Maneesh Khattri, Ivan S. Zapreev, "A Markov Reward Model Checker," qest, pp.243-244, Second International Conference on the Quantitative Evaluation of Systems (QEST'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.