Sciweavers

Share
CAV
2000
Springer

Binary Reachability Analysis of Discrete Pushdown Timed Automata

10 years 2 months ago
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...
Zhe Dang, Oscar H. Ibarra, Tevfik Bultan, Richard
Added 02 Aug 2010
Updated 02 Aug 2010
Type Conference
Year 2000
Where CAV
Authors Zhe Dang, Oscar H. Ibarra, Tevfik Bultan, Richard A. Kemmerer, Jianwen Su
Comments (0)
books