Advertisement

On Removing the Pushdown Stack in Reachability Constructions

  • Oscar H. Ibarra
  • Zhe Dang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2223)

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 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    R. Alur and D. Dill. “The theory of timed automata,” TCS, 126(2):183–236, 1994MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    P. Abdulla and B. Jonsson. “Verifying programs with unreliable channels,” Information and Computation, 127(2): 91–101, 1996MathSciNetCrossRefzbMATHGoogle Scholar
  3. 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. 4.
    G. Cece and A. Finkel. “Programs with Quasi-Stable Channels are Effectively Recognizable,” CAV’97, LNCS 1254, pp. 304–315 244Google Scholar
  5. 5.
    H. Comon and V. Cortier. “Flatness is not a weakness,” Proc. Computer Science Logic, 2000Google Scholar
  6. 6.
    H. Comon and Y. Jurski. “Multiple counters automata, safety analysis and Presburger arithmetic,” CAV’98, LNCS 1427, pp. 268–279Google Scholar
  7. 7.
    H. Comon and Y. Jurski. “Timed automata and the theory of real numbers,” CONCUR’99, LNCS 1664, pp. 242–257Google Scholar
  8. 8.
    Z. Dang. “Binary reachability analysis of timed pushdown automata with dense clocks,” CAV’01, LNCS 2102, pp. 506–517Google Scholar
  9. 9.
    Z. Dang and O. H. Ibarra. “Liveness verification of reversal-bounded counter machines with a free counter,” submitted, 2001Google Scholar
  10. 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. 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. 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. 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. 14.
    A. Finkel, B. Willems, and P. Wolper. “A direct symbolic approach to model checking pushdown systems,” INFINITY’97 Google Scholar
  15. 15.
    S. Ginsburg and E. Spanier. “Bounded Algol-like languages,” Transactions of American Mathematical Society, 113, pp. 333–368, 1964.MathSciNetzbMATHGoogle Scholar
  16. 16.
    O. H. Ibarra. “Reversal-bounded multicounter machines and their decision problems,” J. ACM, 25 (1978) 116–133MathSciNetCrossRefzbMATHGoogle Scholar
  17. 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. 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. 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. 20.
    O. H. Ibarra, Z. Dang, and P. San Pietro, “Verification in Loosely Synchronous Queue-Connected Discrete Timed Automata,” submitted. 2001Google Scholar
  21. 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. 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. 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. 24.
    W. Peng and S. Purushothaman. “Analysis of a Class of Communicating Finite State Machines,” Acta Informatica, 29(6/7): 499–522, 1992MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Oscar H. Ibarra
    • 1
  • Zhe Dang
    • 2
  1. 1.Department of Computer ScienceUniversity of California Santa BarbaraUSA
  2. 2.School of Electrical Engineering and Computer ScienceWashington State UniversityPullmanUSA

Personalised recommendations