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

Baier, Christel and Haverkort, Boudewijn and Hermanns, Holger and Katoen, Joost-Pieter (2004) Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. [Report]

Preview

PDF
256Kb

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.
Item Type:	Report
Copyright:	©2003 CTIT
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Design and Analysis of Communication Systems (DACS) Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/49256
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Repository Staff Only: item control page

Metis ID: 221438