Third International Conference on the Quantitative Evaluation of Systems - (QEST'06)
Probably on Time and within BudgetOn Reachability in Priced Probabilistic Timed Automata
Riverside, California
September 11-September 14
ISBN: 0-7695-2665-9
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 e¸ [0, 1]. We prove that the algorithm is partially correct and show an example for which termination cannot be guaranteed.
Citation:
Jasper Berendsen, David N. Jansen, Joost-Pieter Katoen, "Probably on Time and within BudgetOn Reachability in Priced Probabilistic Timed Automata," qest, pp.311-322, Third International Conference on the Quantitative Evaluation of Systems - (QEST'06), 2006