TY - BOOK

T1 - Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes

AU - Baier, Christel

AU - Haverkort, Boudewijn

AU - Hermanns, Holger

AU - Katoen, Joost P.

PY - 2003/10

Y1 - 2003/10

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. We prove 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. We prove that these probabilities coincide for (time-abstract) history-dependent and Markovian schedulers that resolve nondeterminism either deterministically or in a randomized way.

M3 - Report

T3 - CTIT technical report series

BT - Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -