DocumentCode
3280860
Title
A Markov reward model checker
Author
Katoen, Joost-Pieter ; Khattri, Maneesh ; Zapreev, Ivan S.
Author_Institution
Twente Univ., AE Enschede, Netherlands
fYear
2005
fDate
19-22 Sept. 2005
Firstpage
243
Lastpage
244
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
Markov processes; formal verification; probabilistic logic; reachability analysis; temporal logic; CSL; MRMC; Markov reward model checker; PCTL; automated verification; continuous stochastic logic; continuous-time Markov reward model; discrete-time model; numerical algorithm; reachability analysis; reward constraint; Algebra; Costs; Law; Legal factors; Probabilistic logic; Stochastic processes; System recovery;
fLanguage
English
Publisher
ieee
Conference_Titel
Quantitative Evaluation of Systems, 2005. Second International Conference on the
Print_ISBN
0-7695-2427-3
Type
conf
DOI
10.1109/QEST.2005.2
Filename
1595801
Link To Document