Probably on Time and within BudgetOn Reachability in Priced Probabilistic Timed Automata
Joost-Pieter Katoen, David N. Jansen, J. Berendsen, Joost-Pieter Katoen, D.N. Jansen, J. Berendsen · 2006
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.