On Removing the Pushdown Stack in Reachability Constructions

A discrete pushdown timed automaton is a pushdown machine with integer-valued clocks. It has been shown recently that the binary reachability of a discrete pushdown timed automaton can be accepted by a 2-tape pushdown acceptor with reversal-bounded counters. We improve this result by showing that the stack can be removed from the acceptor, i.e., the binary reachability can be accepted by a 2-tape finite-state acceptor with reversal-bounded counters. We also obtain similar results for more general machine models. Our characterizations can be used to verify certain properties concerning these machines that were not verifiable before using previous techniques. We are also able to formulate a subset of Presburger LTL that is decidable for satisfiability-checking with respect to these machines.

• Type: Conference
• Year: 2001
• Where: ISAAC
• Authors: Oscar H. Ibarra, Zhe Dang
• Keywords: Algorithms, Binary Reachability, Discrete Pushdown, ISAAC 2001, Pushdown Timed Automaton