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. In: 10th International Conference Tools and Algorithms for the Construction and Analysis of Systems, TACAS, March 29 - April 2, 2004, Barcelona, Spain (pp. pp. 61-76).
Restricted to UT campus only : Request a copy
|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.
This work is supported by the NWO-DFG bilateral project Validation of Stochastic Systems.
|Item Type:||Conference or Workshop Item|
|Copyright:||© 2004 Springer|
Electrical Engineering, Mathematics and Computer Science (EEMCS)
|Link to this item:||http://purl.utwente.nl/publications/63329|
|Export this item as:||BibTeX|
Daily downloads in the past month
Monthly downloads in the past 12 months
Repository Staff Only: item control page