Sciweavers

Share
QEST
2005
IEEE

A Markov Reward Model Checker

10 years 14 days ago
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.
Joost-Pieter Katoen, Maneesh Khattri, Ivan S. Zapr
Added 25 Jun 2010
Updated 25 Jun 2010
Type Conference
Year 2005
Where QEST
Authors Joost-Pieter Katoen, Maneesh Khattri, Ivan S. Zapreev
Comments (0)
books