Empty stack Pushdown ω-tree automata

  • Wuxu Peng
  • S. Purushothaman
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 581)


In this paper we consider Pushdown automata on infinite trees with empty stack as the accepting condition (ω-EPDTA). We provide the following regarding ω-EPDTA (a) its a relationship to other Pushdown automata on infinite trees, (b) a Kleene-Closure theorem and (c) a single exponential time algorithm for checking emptiness. We also discuss the relevance of the results presented here to modelchecking.


Model Check Leaf Node Tree Automaton Finite Tree Pushdown Automaton 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    J. C. M. Baeten, J. A. Bergstra, J. W. Klop. Decidability of Bisimulation Equivalence for Processes Generating Context-Free Languages. In LNCS 259, pp: 93–114. Springer-Verlag, 1987.Google Scholar
  2. [2]
    J. Bradfield and C. Stirling, Local Model Checking for Infinite State Spaces. To appear in Theoretical Comp. Sci. Google Scholar
  3. [3]
    E. M. Clarke, E. A. Emerson, A. P. Sistla, Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications: a Practical Approach. Proc. of the 10th ACM Symp. on Principles of Prog. Lang., 1983, pp.117–126.Google Scholar
  4. [4]
    R. Cleaveland, Tableau-Based Model Checking in the Prepositional Mu-Calculus. Acta Informatica, Vol.27, 1990, pp.725–747.Google Scholar
  5. [5]
    R. S. Cohen and A. Y. Gold, Theory of ω-Languages I: Characterizations of ω-Context-Free Languages. J. of Comp. and Sys. Sci., Vol. 15, 1977, pp.169–184.Google Scholar
  6. [6]
    I. Guessarian, Pushdown Tree Automata. Math. Sys. Theory, Vol. 16, 1983, pp.237–263.Google Scholar
  7. [7]
    D. Harel and D. Raz, Deciding Properties of Nonregular Programs. IEEE 31st Symp. on Found. of Comp. Sci., 1990, pp.652–661.Google Scholar
  8. [8]
    H. Hüttel and C. Stirling, Actions Speak Louder Than Words: Proving Bisimilarity for Context-Free Processes. Report ECS-LFCS-91-145, Dept. of Comp. Sci., Univ. of Edinburgh, April 1991. Also in Proc. of 6th Symp. on Logic in Comp. Sci., 1991.Google Scholar
  9. [9]
    M. Linna, On ω-Sets Associated with Context-Free Languages. Information and Control, Vol. 31, 1976, pp.272–293.Google Scholar
  10. [10]
    T. S. E. Maibaum, Pumping Lemmas for Term Languages. J. of Comp. and Sys. Sci., Vol. 17, 1978, pp.319–330.Google Scholar
  11. [11]
    A. Saoudi, Pushdown Automata on Infinite Trees and Omega-Kleene Closure of Context-Free Tree Sets. Proc. of Math. Found. of Comp. Sci., LNCS 379, Springer-Verlag, 1989.Google Scholar
  12. [12]
    S. Tanaka and T. Kasai, The Emptiness Problem for Indexed Language is Exponential-Time Complete. Sys. and Comp. in Japan, Vol. 17(9), 1986, pp.29–37.Google Scholar
  13. [13]
    W. Thomas. Automata on Infinite Objects. In Handbook of Theoretical Computer Science, Vol B. (ed) J. van Leeuwen, pp:133–192, MIT Press, 1990.Google Scholar
  14. [14]
    M. Y. Vardi and P. Wolper, Automata-Theoretic Techniques for Modal Logics of Programs. J. of Comp. and Sys. Sci., Vol. 32, 1986, pp.183–221.Google Scholar
  15. [15]
    M. Y. Vardi and P. Wolper, An Automata-Theoretic Approach to Automatic Program Verification. Proc. of 1st Symp. on Logic in Comp. Sci., 1986, pp.332–344.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Wuxu Peng
    • 1
  • S. Purushothaman
    • 2
  1. 1.Department of Computer ScienceSouthwest Texas State UniversitySan Marcos
  2. 2.Department of Computer ScienceThe Pennsylvania State UniversityUniversity Park

Personalised recommendations