The following technical report is available from http://aib.informatik.rwth-aachen.de:
Time-Bounded Reachability in Continuous-Time Markov Decision Processes Martin Neuhäußer, Lijun Zhang AIB 2009-12
This paper solves the problem of computing the maximum and minimum probability to reach a set of goal states within a given time bound for locally uniform continuous-time Markov decision processes (CTMDPs). As this model allows for nondeterministic choices between exponentially delayed transitions, we define total time positional (TTP) schedulers which rely on the CTMDP's current state and the total elapsed time when taking a decision. In this paper, TTP schedulers are proved to be sufficient to maximize timed reachability even w.r.t. fully time- and history-dependent schedulers; further, they allow us to derive a fixed point characterization of the optimal timed-reachability probability. The main contribution of this paper is a discretization technique which, for an a priori given error bound epsilon, induces a discrete-time MDP that approximates the optimal timed reachability probability in the underlying CTMDP up to epsilon.