Publication details

Optimal Continuous Time Markov Decisions



Year of publication 2015
Type Article in Proceedings
Conference ATVA 2015
MU Faculty or unit

Faculty of Informatics

Field Informatics
Keywords Continuous time Markov decision process; time bounded reachability; uniformisation; experimental evaluation
Description In the context of Markov decision processes running in continuous time, one of the most intriguing challenges is the efficient approximation of finite horizon reachability objectives. A multitude of sophisticated model checking algorithms have been proposed for this. However, no proper benchmarking has been performed thus far. This paper presents a novel and yet simple solution: an algorithm originally developed for a restricted subclass of models and a subclass of schedulers can be twisted so as to become competitive with the more sophisticated algorithms in full generality. As the second main contribution, we perform a comparative evaluation of the core algorithmic concepts on an extensive set of benchmarks varying over all key parameters: model size, amount of non-determinism, time horizon, and precision.
Related projects: