Optimal time-abstract schedulers for CTMDPs and continuous-time Markov games

We study time-bounded reachability in continuous-time Markov decision processes (CTMDPs) and games (CTGs) for time-abstract scheduler classes. Reachability problems play a paramount role in probabilistic model checking. Consequently, their analysis has been studied intensively, and approximation techniques are well understood. From a mathematical point of view, however, the question of approximation is secondary compared to the fundamental question whether or not optimal control exists. In this article, we demonstrate the existence of optimal schedulers for the time-abstract scheduler classes for CTMDPs. For CTGs, we distinguish two cases: the simple case where both players face the same restriction to use time-abstract strategies (symmetric CTGs) and the case where one player is a completely informed adversary (asymmetric CTGs). While for the former case optimal strategies exist, we prove that for asymmetric CTGs there is not necessarily a scheduler that attains the optimum. It turns out that for CTMDPs and symmetric CTGs optimal time-abstract schedulers have an amazingly simple structure: they converge to a memoryless scheduling policy after a finite number of steps. This allows us to compute time-abstract strategies with finite memory. (C) 2012 Elsevier B.V. All rights reserved.