Time-Bounded Reachability in Continuous-Time Markov Decision Processes
Martin Neuhäußer, Lijun Zhang
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.