Title :
A Markov reward model checker
Author :
Katoen, Joost-Pieter ; Khattri, Maneesh ; Zapreev, Ivan S.
Author_Institution :
Twente Univ., AE Enschede, Netherlands
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;
Conference_Titel :
Quantitative Evaluation of Systems, 2005. Second International Conference on the
Print_ISBN :
0-7695-2427-3
DOI :
10.1109/QEST.2005.2
