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

Christel BaierChristel Baier, Holger HermannsHolger Hermanns, Joost-Pieter KatoenJoost-Pieter Katoen, Boudewijn R. HaverkortBoudewijn R. Haverkort

DOI Link

Christel Baier, Holger Hermanns, Joost-Pieter Katoen, Boudewijn R. Haverkort
Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
Theoretical Computer Science, 345(1):2--26, 2005

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@article{BHKH2005,
  author  = {Christel Baier and Holger Hermanns and Joost-Pieter Katoen and
             Boudewijn R. Haverkort},
  title   = {Efficient computation of time-bounded reachability probabilities in
             uniform continuous-time Markov decision processes},
  journal = {Theoretical Computer Science},
  volume  = {345},
  number  = {1},
  year    = {2005},
  pages   = {2--26},
  doi     = {10.1016/J.TCS.2005.07.022}
}