Efficient Computation of Time-Bounded Reachability Probabilities in Uniform Continuous-Time Markov Decision Processes

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

DOI Link

Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen
Efficient Computation of Time-Bounded Reachability Probabilities in Uniform Continuous-Time Markov Decision Processes
10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2988 of Lecture Notes in Computer Science, 61--76, 2004. Springer

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. We prove 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

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-540-24730-2_5.

@inproceedings{BHHK2004,
  author    = {Christel Baier and Boudewijn R. Haverkort and Holger Hermanns and
               Joost-Pieter Katoen},
  title     = {Efficient Computation of Time-Bounded Reachability Probabilities
               in Uniform Continuous-Time Markov Decision Processes},
  booktitle = {10th International Conference on Tools and Algorithms for the
               Construction and Analysis of Systems (TACAS)},
  series    = {Lecture Notes in Computer Science},
  volume    = {2988},
  publisher = {Springer},
  year      = {2004},
  pages     = {61--76},
  doi       = {10.1007/978-3-540-24730-2_5}
}