Binary reachability analysis of discrete pushdown timed automata

Abstract

We introduce discrete pushdown timed automata that are timed automata with integer-valued clocks augmented with a pushdown stack. A configuration of a discrete pushdown timed automaton includes a control state, finitely many clock values and a stack word. Using a pure automata-theoretic approach, we show that the binary reachability (i.e., the set of all pairs of configurations (α, β), encoded as strings, such that α can reach β through 0 or more transitions) can be accepted by a nondeterministic pushdown machine augmented with reversal-bounded counters (NPCM). Since discrete timed automata with integer-valued clocks can be treated as discrete pushdown timed automata without the pushdown stack, we can show that the binary reachability of a discrete timed automaton can be accepted by a nondeterministic reversal-bounded multi-counter machine. Thus, the binary reachability is Presburger. By using the known fact that the emptiness problem is decidable for reversal- bounded NPCMs, the results can be used to verify a number of properties that cannot be expressed by timed temporal logics for discrete timed automata and CTL* for pushdown systems.