TY - JOUR
T1 - Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
AU - Baier, Christel
AU - Hermanns, Holger
AU - Katoen, Joost-Pieter
AU - Haverkort, Boudewijn R.
PY - 2005
Y1 - 2005
N2 - 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. This paper presents 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. It furthermore proves that these probabilities coincide for (time-abstract) history-dependent and Markovian schedulers that
resolve nondeterminism either deterministically or in a randomized way.
AB - 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. This paper presents 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. It furthermore proves that these probabilities coincide for (time-abstract) history-dependent and Markovian schedulers that
resolve nondeterminism either deterministically or in a randomized way.
KW - Continuous-time Markov decision process (CTMDP)
KW - Temporal logic
KW - Model checking
KW - Time-bounded reachability
U2 - 10.1016/j.tcs.2005.07.022
DO - 10.1016/j.tcs.2005.07.022
M3 - Article
VL - 345
SP - 2
EP - 26
JO - Theoretical computer science
JF - Theoretical computer science
SN - 0304-3975
IS - 1
ER -