@article{ac8a8db20e8a44f1869be3f2ffb6e75b,
title = "Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes",
abstract = "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.",
keywords = "Continuous-time Markov decision process (CTMDP), Temporal logic, Model checking, Time-bounded reachability",
author = "Christel Baier and Holger Hermanns and Joost-Pieter Katoen and Haverkort, {Boudewijn R.}",
year = "2005",
doi = "10.1016/j.tcs.2005.07.022",
language = "English",
volume = "345",
pages = "2--26",
journal = "Theoretical computer science",
issn = "0304-3975",
publisher = "Elsevier B.V.",
number = "1",
}