Dennis Guck

 

Analysis and scheduler synthesis of time-bounded reachability in
continuous-time Markov decision processes

 

Abstract:

 Continuous-time Markov decision processes (CTMDPs) are stochastic
models in which probabilistic and nondeterministic choices
co-exist. Lately, a discretization technique has been developed to
compute time-bounded reachability probabilities in locally uniform
CTMDPs, i.e. CTMDPs with state-wise constant sojourn-times. We extend
the underlying value iteration algorithm, such that it computes an
epsilon-optimal scheduler for time-bounded reachability probabilities
in CTMDPs as a byproduct. Further, we give a proof of correctness that
the scheduler is epsilon-optimal. The epsilon-optimality stands for an
error epsilon > 0, that is induced by the approximation algorithm, and
can be specified a priori. As a second contribution, we extend the
value iteration algorithm with an incremental computation for several
time bounds and prove that we obey the error bound epsilon with this
method.