Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

9

QEST
2005
IEEE

favoriteEmaildiscussreport

109views Modeling and Simulation» more QEST 2005»

A Markov Reward Model Checker

13 years 10 months ago

A Markov Reward Model Checker

Download www.mrmc-tool.org

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 veriﬁcation 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

Real-time Traffic

Continuous-time Markov Reward | Paper Introduces Mrmc | QEST 2005 | Quantitative Evaluation Of Systems | Reward Extensions |

claim paper

Related Content

» The Ins and Outs of the Probabilistic Model Checker MRMC

» The Performability Tool Pility

» iLTLChecker A Probabilistic Model Checker for Multiple DTMCs

» Model Checking Markov Reward Models with Impulse Rewards

» BoundPreserving Composition for Markov Reward Models

» Symblicit Calculation of LongRun Averages for Concurrent Probabilistic Systems

» A Markov Chain Model Checker

» DiscreteTime Rewards ModelChecked

» Learning Reward Modalities for HumanRobotInteraction in a Cooperative Training Task

Post Info
More Details (n/a)

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)