Sciweavers

TAMC
2009
Springer

Undecidability of Cost-Bounded Reachability in Priced Probabilistic Timed Automata

14 years 6 months ago
Undecidability of Cost-Bounded Reachability in Priced Probabilistic Timed Automata
Priced Probabilistic Timed Automata (PPTA) extend timed automata with cost-rates in locations and discrete probabilistic branching. The model is a natural combination of Priced Timed Automata and Probabilistic Timed Automata. In this paper we focus on cost-bounded probabilistic reachability for PPTA, which determines if the maximal probability to reach a goal location within a given cost bound (and time bound) exceeds a threshold p ∈ (0, 1]. We prove undecidability of the problem for simple PPTA in 3 variants: with 3 clocks and stopwatch cost-rates or strictly positive cost-rates. Because we encode a 2-counter machine in a new way, we can also show undecidability for cost-rates in Z and only 2 clocks.
Jasper Berendsen, Taolue Chen, David N. Jansen
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where TAMC
Authors Jasper Berendsen, Taolue Chen, David N. Jansen
Comments (0)