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

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

doi:10.1007/978-3-540-24730-2_5

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

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

16 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. We prove 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
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication	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
Editors	Kurt Jensen, Andreas Podelski
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	61-76
Number of pages	16
ISBN (Electronic)	978-3-540-24730-2
ISBN (Print)	978-3-540-21299-7
DOIs	https://doi.org/10.1007/978-3-540-24730-2_5
Publication status	Published - 2004
Event	10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004 - Barcelona, Spain Duration: 29 Mar 2004 → 2 Apr 2004 Conference number: 10

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	2988
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004
Abbreviated title	TACAS
Country/Territory	Spain
City	Barcelona
Period	29/03/04 → 2/04/04

Keywords

FMT-PM: PROBABILISTIC METHODS
FMT-MC: MODEL CHECKING
FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
Continuous-time Markov decision process (CTMDP)

Access to Document

10.1007/978-3-540-24730-2_5

Baier2005efficientAccepted author version, 281 KB

1 Article

Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
Baier, C., Hermanns, H., Katoen, J.-P. & Haverkort, B. R., 2005, In: Theoretical computer science. 345, 1, p. 2-26 25 p.
Research output: Contribution to journal › Article › Academic › peer-review

Open Access
File
100 Citations (Scopus)

58 Downloads (Pure)

Cite this

Baier, C., Haverkort, B., Hermanns, H., & Katoen, J.-P. (2004). Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. In K. Jensen, & A. Podelski (Eds.), 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 (pp. 61-76). (Lecture Notes in Computer Science; Vol. 2988). Springer. https://doi.org/10.1007/978-3-540-24730-2_5

Baier, Christel ; Haverkort, Boudewijn ; Hermanns, Holger et al. / Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. 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. editor / Kurt Jensen ; Andreas Podelski. Berlin, Heidelberg : Springer, 2004. pp. 61-76 (Lecture Notes in Computer Science).

@inproceedings{4a6cc9d758384d4ea2f8a7617c105bab,

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. We prove that these probabilities coincide for (time-abstract) history-dependent and Markovian schedulers that resolve nondeterminism either deterministically or in a randomized way.",

keywords = "FMT-PM: PROBABILISTIC METHODS, FMT-MC: MODEL CHECKING, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, Continuous-time Markov decision process (CTMDP)",

author = "Christel Baier and Boudewijn Haverkort and Holger Hermanns and Joost-Pieter Katoen",

year = "2004",

doi = "10.1007/978-3-540-24730-2_5",

language = "English",

isbn = "978-3-540-21299-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "61--76",

editor = "Kurt Jensen and Andreas Podelski",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

address = "Germany",

note = "10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004, TACAS ; Conference date: 29-03-2004 Through 02-04-2004",

}

Baier, C, Haverkort, B, Hermanns, H & Katoen, J-P 2004, Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. in K Jensen & A Podelski (eds), 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. Lecture Notes in Computer Science, vol. 2988, Springer, Berlin, Heidelberg, pp. 61-76, 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004, Barcelona, Spain, 29/03/04. https://doi.org/10.1007/978-3-540-24730-2_5

Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. / Baier, Christel; Haverkort, Boudewijn; Hermanns, Holger et al.
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. ed. / Kurt Jensen; Andreas Podelski. Berlin, Heidelberg: Springer, 2004. p. 61-76 (Lecture Notes in Computer Science; Vol. 2988).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

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

AU - Baier, Christel

AU - Haverkort, Boudewijn

AU - Hermanns, Holger

AU - Katoen, Joost-Pieter

N1 - Conference code: 10

PY - 2004

Y1 - 2004

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. We prove 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. We prove that these probabilities coincide for (time-abstract) history-dependent and Markovian schedulers that resolve nondeterminism either deterministically or in a randomized way.

KW - FMT-PM: PROBABILISTIC METHODS

KW - FMT-MC: MODEL CHECKING

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - Continuous-time Markov decision process (CTMDP)

U2 - 10.1007/978-3-540-24730-2_5

DO - 10.1007/978-3-540-24730-2_5

M3 - Conference contribution

SN - 978-3-540-21299-7

T3 - Lecture Notes in Computer Science

SP - 61

EP - 76

BT - Tools and Algorithms for the Construction and Analysis of Systems

A2 - Jensen, Kurt

A2 - Podelski, Andreas

PB - Springer

CY - Berlin, Heidelberg

T2 - 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004

Y2 - 29 March 2004 through 2 April 2004

ER -

Baier C, Haverkort B, Hermanns H, Katoen JP. Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. In Jensen K, Podelski A, editors, 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. Berlin, Heidelberg: Springer. 2004. p. 61-76. (Lecture Notes in Computer Science). doi: 10.1007/978-3-540-24730-2_5

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

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Research output

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

Cite this