Binary Reachability Analysis of Discrete Pushdown Timed Automata

We introduce discrete pushdown timed automata that are timed automata with integer-valued clocks augmented with a pushdown stack. A con guration of a discrete pushdown timed automaton includes a control state, nitely 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 con gurations ( ), 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 multicounter machine. Thus, the binary reachability is Presburger. By using the known fact that the emptiness problem is decidable for reversalbounded NPCMs, the results can be used...

• Type: Conference
• Year: 2000
• Where: CAV
• Authors: Zhe Dang, Oscar H. Ibarra, Tevfik Bultan, Richard A. Kemmerer, Jianwen Su
• Keywords: CAV 2000, Discrete Pushdown, Hardware, Pushdown, Pushdown Timed Automata