title: Model checking rewards, time, choices, and risks
topics: Dependability, security and performance
committee: Mariƫlle Stoelinga ,
Dennis Guck


Markov Reward Automata (MRA) are a model that incorporate nondeterminstic choices, rewards/cost, timing and probability. Typical questions that can be formulated in this model are: what is the average time to reach a certain state? And what is the minimal probability to reach a certain goal, in a certain time?

Goal of this project is to design model checking algorithms for these automata. For several subclasses of MRA (eg without rewards, or without nondetermism), such algorithms exist, and can serve as a basis

Also, the paper below investigates three basic algorithms for model checking MRA.


  1. Modelling and analysis of Markov reward automata. By Guck, D. and Timmer, M. and Hatefi, H and Ruijters, E.J.J. and Stoelinga, M.I.A. (Digital version available here)