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

Christel Baier; Boudewijn Haverkort; Holger Hermanns; Joost P. Katoen

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

Christel Baier, Boudewijn Haverkort, Holger Hermanns, Joost P. Katoen

Research output: Book/Report › Report › Professional

8 Citations (Scopus)

107 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
Place of Publication	Enschede
Publisher	Centre for Telematics and Information Technology (CTIT)
Number of pages	30
Publication status	Published - Oct 2003

Publication series

Name	CTIT technical report series
Publisher	Centre for Telematics and Information Technology, University of Twente
No.	03-50
ISSN (Print)	1381-3625

Access to Document

Baier2003efficientFinal published version, 256 KB

8 Citations
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)

51 Downloads (Pure)

Cite this

@book{bf215a64e1754e6ea41d451af9663a37,

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

author = "Christel Baier and Boudewijn Haverkort and Holger Hermanns and Katoen, {Joost P.}",

year = "2003",

month = oct,

language = "English",

series = "CTIT technical report series",

publisher = "Centre for Telematics and Information Technology (CTIT)",

number = "03-50",

address = "Netherlands",

}

TY - BOOK

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

PY - 2003/10

Y1 - 2003/10

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.

M3 - Report

T3 - CTIT technical report series

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

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -

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

Abstract

Publication series

Access to Document

Fingerprint

Research output

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

Cite this