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

Christel Baier, H. Hermanns, Joost P. Katoen, Boudewijn R.H.M. Haverkort

Research output: Contribution to journalArticleScientificpeer-review

96 Citations (Scopus)

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.
Original languageEnglish
Pages (from-to)2-26
Number of pages25
JournalTheoretical Computer Science
Volume345
Issue number1
DOIs
Publication statusPublished - 2005
Externally publishedYes

Keywords

  • EWI-1431
  • METIS-225905
  • IR-54792

Fingerprint Dive into the research topics of 'Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes'. Together they form a unique fingerprint.

Cite this