A Markov Reward Model Checker

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Joost-Pieter Katoen Articles by Maneesh Khattri Articles by Ivan S. Zapreev

Second International Conference on the Quantitative Evaluation of Systems (QEST'05)

Torino, Italy

September 19-September 22

ISBN: 0-7695-2427-3

	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

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

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

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.