Title :
Probably on Time and within BudgetOn Reachability in Priced Probabilistic Timed Automata
Author :
Berendsen, J. ; Jansen, D.N. ; Katoen, Joost-Pieter
Author_Institution :
Formal Methods & Tools Group, Twente Univ., Enschede
Abstract :
This paper presents an algorithm for cost-bounded probabilistic reachability in timed automata extended with prices (on edges and locations) and discrete probabilistic branching. The algorithm determines whether the probability to reach a (set of) goal location(s) within a given price bound (and time bound) can exceed a threshold p isin [0,1]. We prove that the algorithm is partially correct and show an example for which termination cannot be guaranteed
Keywords :
computational complexity; probabilistic automata; probability; reachability analysis; cost-bounded probabilistic reachability; discrete probabilistic branching; priced probabilistic timed automata;
Conference_Titel :
Quantitative Evaluation of Systems, 2006. QEST 2006. Third International Conference on
Conference_Location :
Riverside, CA
Print_ISBN :
0-7695-2665-9
DOI :
10.1109/QEST.2006.43
