Optimal Continuous Time Markov Decisions

TL;DR

This paper introduces a simple, adaptable algorithm for continuous-time Markov decision processes that effectively approximates reachability objectives and is validated through extensive benchmarking across various parameters.

Contribution

It presents a novel, simplified algorithm for continuous-time Markov decision processes and provides the first comprehensive benchmarking study of core algorithmic concepts.

Findings

The proposed algorithm is competitive with sophisticated methods.

Benchmarking covers diverse model sizes and parameters.

The approach is effective for finite horizon reachability objectives.

Abstract

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.