A Markov Reward Model Checker

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.

• Type: Conference
• Year: 2005
• Where: QEST
• Authors: Joost-Pieter Katoen, Maneesh Khattri, Ivan S. Zapreev
• Keywords: Continuous-time Markov Reward, Paper Introduces Mrmc, QEST 2005, Quantitative Evaluation Of Systems, Reward Extensions