# On Removing the Pushdown Stack in Reachability Constructions

## Abstract

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.

## Keywords

Mode Change Time Automaton Input Tape Counter Machine Clock Constraint## Preview

Unable to display preview. Download preview PDF.

## References

- 1.R. Alur and D. Dill. “
*The theory of timed automata*,”*TCS*, 126(2):183–236, 1994MathSciNetCrossRefzbMATHGoogle Scholar - 2.P. Abdulla and B. Jonsson. “
*Verifying programs with unreliable channels*,”*Information and Computation*, 127(2): 91–101, 1996MathSciNetCrossRefzbMATHGoogle Scholar - 3.A. Bouajjani, J. Esparza, and O. Maler. “
*Reachability analysis of pushdown automata: application to model-Checking*,”*CONCUR’97*,**LNCS**1243, pp. 135–150Google Scholar - 4.G. Cece and A. Finkel. “
*Programs with Quasi-Stable Channels are Effectively Recognizable*,”*CAV’97*,**LNCS**1254, pp. 304–315 244Google Scholar - 5.H. Comon and V. Cortier. “
*Flatness is not a weakness*,”*Proc. Computer Science Logic*, 2000Google Scholar - 6.H. Comon and Y. Jurski. “
*Multiple counters automata, safety analysis and Presburger arithmetic*,”*CAV’98*,**LNCS**1427, pp. 268–279Google Scholar - 7.H. Comon and Y. Jurski. “
*Timed automata and the theory of real numbers*,”*CONCUR’99*,**LNCS**1664, pp. 242–257Google Scholar - 8.Z. Dang. “
*Binary reachability analysis of timed pushdown automata with dense clocks*,”*CAV’01*,**LNCS**2102, pp. 506–517Google Scholar - 9.Z. Dang and O. H. Ibarra. “
*Liveness verification of reversal-bounded counter machines with a free counter*,” submitted, 2001Google Scholar - 10.Z. Dang, O. H. Ibarra, T. Bultan, R. A. Kemmerer and J. Su. “
*Binary Reachability Analysis of Discrete Pushdown Timed Automata*,”*CAV’00*,**LNCS**1855, pp. 69–84Google Scholar - 11.Z. Dang, P. San Pietro, and R. A. Kemmerer. “
*On Presburger Liveness of Discrete Timed Automata*,”*STACS’01*,**LNCS**2010, pp. 132–143Google Scholar - 12.J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. “
*Effcient Algorithms for Model Checking Pushdown Systems*,”*CAV’00*,**LNCS**1855, pp. 232–247Google Scholar - 13.A. Finkel and G. Sutre. “
*Decidability of Reachability Problems for Classes of Two Counter Automata*,”*STACS’00*,**LNCS**1770, pp. 346–357 244Google Scholar - 14.A. Finkel, B. Willems, and P. Wolper. “
*A direct symbolic approach to model checking pushdown systems*,”*INFINITY’97*Google Scholar - 15.S. Ginsburg and E. Spanier. “
*Bounded Algol-like languages*,”*Transactions of American Mathematical Society*, 113, pp. 333–368, 1964.MathSciNetzbMATHGoogle Scholar - 16.O. H. Ibarra. “
*Reversal-bounded multicounter machines and their decision problems*,”*J. ACM*,**25**(1978) 116–133MathSciNetCrossRefzbMATHGoogle Scholar - 17.O. H. Ibarra. “
*Reachability and safety in queue systems with counters and pushdown stack*,”*Proceedings of the International Conference on Implementation and Application of Automata*, pp. 120–129, 2000.Google Scholar - 18.O. H. Ibarra, T. Bultan, and J. Su. “
*Reachability analysis for some models of infinite-state transition systems*,”*CONCUR’00*, pp. 183–198, 2000.Google Scholar - 19.O. H. Ibarra. “
*Reachability and safety in queue systems with counters and pushdown stack*,”*Proceedings of the International Conference on Implementation and Application of Automata*, pp. 120–129, 2000Google Scholar - 20.O. H. Ibarra, Z. Dang, and P. San Pietro, “
*Verification in Loosely Synchronous Queue-Connected Discrete Timed Automata*,” submitted. 2001Google Scholar - 21.O. H. Ibarra and J. Su. “
*Generalizing the discrete timed automaton*,”*Proceedings of the International Conference on Implementation and Application of Automata*, 206–215, 2000.Google Scholar - 22.O. H. Ibarra, J. Su, T. Bultan, Z. Dang, and R. A. Kemmerer. “
*Counter Machines: Decidable Properties and Applications to Verification Problems*,”,*MFCS’00*,**LNCS**1893, pp. 426–435Google Scholar - 23.K. L. McMillan. “
*Symbolic model-checking — an approach to the state explosion problem*,” PhD thesis, Department of Computer Science, Carnegie Mellon University, 1992Google Scholar - 24.W. Peng and S. Purushothaman. “
*Analysis of a Class of Communicating Finite State Machines*,”*Acta Informatica*, 29(6/7): 499–522, 1992MathSciNetCrossRefzbMATHGoogle Scholar