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

Christel Baier; Holger Hermanns; Joost-Pieter Katoen; Boudewijn R. Haverkort

doi:10.1016/j.tcs.2005.07.022

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

Christel Baier, Holger Hermanns, Joost-Pieter Katoen, Boudewijn R. Haverkort

Research output: Contribution to journal › Article › Academic › peer-review

98 Citations (Scopus)

31 Downloads (Pure)

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 language	English
Pages (from-to)	2-26
Number of pages	25
Journal	Theoretical computer science
Volume	345
Issue number	1
DOIs	https://doi.org/10.1016/j.tcs.2005.07.022
Publication status	Published - 2005

Keywords

Continuous-time Markov decision process (CTMDP)
Temporal logic
Model checking
Time-bounded reachability

Access to Document

10.1016/j.tcs.2005.07.022

Baier2005efficientAccepted author version, 281 KB

98 Citations
1 Report
1 Conference contribution

Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
Baier, C., Haverkort, B., Hermanns, H. & Katoen, J-P., 2004, Tools and Algorithms for the Construction and Analysis of Systems: 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004. Proceedings. Jensen, K. & Podelski, A. (eds.). Berlin, Heidelberg: Springer, p. 61-76 16 p. (Lecture Notes in Computer Science; vol. 2988).
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

Open Access
File
7 Downloads (Pure)
Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
Baier, C., Haverkort, B., Hermanns, H. & Katoen, J. P., Oct 2003, Enschede: Centre for Telematics and Information Technology (CTIT). 30 p. (CTIT technical report series; no. 03-50)
Research output: Book/Report › Report › Professional

Open Access
File

Cite this

@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",

number = "1",

}

TY - JOUR

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

AU - Baier, Christel

AU - Hermanns, Holger

AU - Katoen, Joost-Pieter

AU - Haverkort, Boudewijn R.

PY - 2005

Y1 - 2005

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

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

KW - Continuous-time Markov decision process (CTMDP)

KW - Temporal logic

KW - Model checking

KW - Time-bounded reachability

U2 - 10.1016/j.tcs.2005.07.022

DO - 10.1016/j.tcs.2005.07.022

M3 - Article

VL - 345

SP - 2

EP - 26

JO - Theoretical computer science

JF - Theoretical computer science

SN - 0304-3975

IS - 1

ER -

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

Abstract

Keywords

Access to Document

Fingerprint

Research output