A Markov reward model checker

Share/Save/Bookmark

Katoen, J.P. and Maneesh Khattri, M. and Zapreev, I.S. (2005) A Markov reward model checker. In: Second International Conference on the Quantitative Evaluation of Systems, 2005.

[img]
Preview
PDF
164Kb
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.
Item Type:Conference or Workshop Item
Copyright:©2005 IEEE
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/54782
Official URL:http://dx.doi.org/10.1109/QEST.2005.2
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 229271