DocumentCode
2619528
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
fYear
2006
fDate
11-14 Sept. 2006
Firstpage
311
Lastpage
322
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Quantitative Evaluation of Systems, 2006. QEST 2006. Third International Conference on
Conference_Location
Riverside, CA
Print_ISBN
0-7695-2665-9
Type
conf
DOI
10.1109/QEST.2006.43
Filename
1704025
Link To Document