One of the most intriguing challenges in the verification of stochastic and non-deterministic systems is the time optimal scheduling of Markov decision processes running in continuous time. A multitude of sophisticated model checking algorithms have been proposed especially in the context of finite horizon reachability objectives since this is the basis of temporal-logic model checking. However, no proper benchmarking has been performed thus far.
We present 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. As the second main contribution, we discuss a novel and yet simple solution: an algorithm originally developed for a restricted subclass of both models and schedulers can be twisted so as to become competitive with the more sophisticated algorithms in full generality.
Joint work with Yuliya Butkova, Hassan Hatefi, and Jan Krcal