A continuous-time Markov decision process (CTMDP) is a
generalization of a continuous-time Markov chain in which both
probabilistic and nondeterministic choices co-exist. CTMDPs are
used in various application contexts ranging from systems biology
over artificial intelligence to embedded systems. In this talk
I present an efficient algorithm to compute the maximum (or minimum)
probability to reach a set of goal states within a given time bound
in a uniform CTMDP, i.e., a CTMDP in which the delay time
distribution per state visit is the same for all states. I will
prove that these probabilities coincide for (time-abstract)
history-dependent and Markovian schedulers that resolve
nondeterminism either deterministically or in a randomized
way.
joint work with C. Baier (Bonn), J.-P. Katoen (Aachen), and B.R. Haverkort
(Twente)