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

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

Research output: Book/ReportReportProfessional

7 Citations (Scopus)
40 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 languageUndefined
Place of PublicationEnschede
PublisherElektrotechniek, Wiskunde & Informatica
Number of pages30
Publication statusPublished - 2004

Publication series

Name1381-3625
PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
No.03-50

Keywords

  • METIS-221438
  • IR-49256

Cite this

Baier, C., Haverkort, B. R. H. M., Hermanns, H., & Katoen, J. P. (2004). Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. (1381-3625; No. 03-50). Enschede: Elektrotechniek, Wiskunde & Informatica.
Baier, Christel ; Haverkort, Boudewijn R.H.M. ; Hermanns, H. ; Katoen, Joost P. / Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Enschede : Elektrotechniek, Wiskunde & Informatica, 2004. 30 p. (1381-3625; 03-50).
@book{9506ac857e7943e4b62a533f74e7b000,
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 = "METIS-221438, IR-49256",
author = "Christel Baier and Haverkort, {Boudewijn R.H.M.} and H. Hermanns and Katoen, {Joost P.}",
year = "2004",
language = "Undefined",
series = "1381-3625",
publisher = "Elektrotechniek, Wiskunde & Informatica",
number = "03-50",

}

Baier, C, Haverkort, BRHM, Hermanns, H & Katoen, JP 2004, Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. 1381-3625, no. 03-50, Elektrotechniek, Wiskunde & Informatica, Enschede.

Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. / Baier, Christel; Haverkort, Boudewijn R.H.M.; Hermanns, H.; Katoen, Joost P.

Enschede : Elektrotechniek, Wiskunde & Informatica, 2004. 30 p. (1381-3625; No. 03-50).

Research output: Book/ReportReportProfessional

TY - BOOK

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

AU - Baier, Christel

AU - Haverkort, Boudewijn R.H.M.

AU - Hermanns, H.

AU - Katoen, Joost P.

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 - METIS-221438

KW - IR-49256

M3 - Report

T3 - 1381-3625

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

PB - Elektrotechniek, Wiskunde & Informatica

CY - Enschede

ER -

Baier C, Haverkort BRHM, Hermanns H, Katoen JP. Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Enschede: Elektrotechniek, Wiskunde & Informatica, 2004. 30 p. (1381-3625; 03-50).