Skip to main content
SpringerLink
Log in
Book cover

International Conference on Logic for Programming Artificial Intelligence and Reasoning

LPAR 2002: Logic for Programming, Artificial Intelligence, and Reasoning pp 262–277Cite as

Pushdown Specifications

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2514))

Abstract

Traditionally, model checking is applied to finite-state systems and regular specifications. While researchers have successfully extended the applicability of model checking to infinite-state systems, almost all existing work still consider regular specification formalisms. There are, however, many interesting non-regular properties one would like to model check.

In this paper we study model checking of pushdown specifications. Our specification formalism is nondeterministic pushdown parity tree automata (PD-NPT). We show that the model-checking problem for regular systems and PD-NPT specifications can be solved in time exponential in the system and the specification. Our model-checking algorithm involves a new solution to the nonemptiness problem of nondeterministic pushdown tree automata, where we improve the best known upper bound from a triple-exponential to a single exponential. We also consider the model-checking problem for context-free systems and PD-NPT specifications and show that it is undecidable.

Supported in part by BSF grant 9800096.

Supported in part by NSF grants CCR-9988322,IIS-9908435,IIS-9978135, and EIA-0086264, by BSF grant 9800096, and by a grant from the Intel Corporation.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2–34, May 1993.

    Google Scholar 

  2. A. Bouajjani, R. Echahed, and P. Habermehl. On the verification problem of nonregular properties for nonregular processes. In 10th LICS, pp. 123–133, 1995. IEEE.

    Google Scholar 

  3. A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In 8th Concur, LNCS 1243, pp. 135–150, 1997.

    Google Scholar 

  4. A. Bouajjani, R. Echahed, and R. Robbana. Verification of nonregular temporal properties for context-free processes. In 5th Concur, LNCS 836, pp. 81–97, 1994.

    Google Scholar 

  5. P. Biesse, T. Leonard, and A. Mokkedem. Finding bugs in an alpha microprocessors using satisfiability solvers. In 13th CAV, LNCS 2102, pp. 454–464. 2001.

    Google Scholar 

  6. J.R. Büchi. On a decision method in restricted second order arithmetic. In Proc. Internat. Congr. Logic, Method. and Philos. Sci. 1960, pages 1–12, Stanford, 1962.

    Google Scholar 

  7. O. Burkart. Model checking rationally restricted right closures of recognizable graphs. In 2nd INFINITY, 1997.

    Google Scholar 

  8. E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, January 1986.

    Google Scholar 

  9. F. Copty, L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella, and M.Y. Vardi. Benefits of bounded model checking at an industrial setting. In 13th CAV, LNCS 2102, pp. 436–453. Springer-Verlag, 2001.

    Google Scholar 

  10. E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.

    Google Scholar 

  11. E.A. Emerson and C. Jutla. Tree automata, μ-calculus and determinacy. In 32nd FOCS, pp. 368–377, 1991.

    Google Scholar 

  12. E.A. Emerson, C. Jutla, and A.P. Sistla. On model-checking for fragments of μ-calculus. In 5th CAV, LNCS 697, pp. 385–396, 1993. Springer-Verlag.

    Google Scholar 

  13. E.A. Emerson. Uniform inevitability is tree automaton ineffable. Information Processing Letters, 24(2):77–79, January 1987.

    Google Scholar 

  14. J.E. Hopcroft, R. Motwani, and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation (2nd Edition). Addison-Wesley, 2000.

    Google Scholar 

  15. D. Harel and D. Raz. Deciding emptiness for stack automata on infinite trees. Information and Computation, 113(2):278–299, September 1994.

    Google Scholar 

  16. D. Janin and I. Walukiewicz. Automata for the modal μ-calculus and related results. In Proc. 20th MFCS, LNCS 969, pp. 552–562. Springer-Verlag, 1995.

    Google Scholar 

  17. O. Kupferman, N. Piterman, and M.Y. Vardi. Model checking linear properties of prefix-recognizable systems. In Proc. 14th CAV, LNCS 2404, pp. 371–385. 2002.

    Google Scholar 

  18. O. Kupferman and M.Y. Vardi. An automata-theoretic approach to reasoning about infinite-state systems. In 12th CAV, LNCS 1855, pp. 36–52. Springer-Verlag, 2000.

    Google Scholar 

  19. O. Kupferman and M.Y. Vardi. On clopen specifications. In Proc. 8th LPAR, LNAI 2250, pp. 24–38. Springer-Verlag, 2001.

    Google Scholar 

  20. O. Kupferman, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312–360, March 2000.

    Google Scholar 

  21. L. Lamport. Sometimes is sometimes “not never”-on the temporal logic of programs. In 7th POPL, pp. 174–185, 1980.

    Google Scholar 

  22. O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In 12th POPL, pp. 97–107, 1985.

    Google Scholar 

  23. M.L. Minsky. Computation: Finite and Infinite Machines. Prentice Hall, 1967.

    Google Scholar 

  24. D.E. Muller and P.E. Schupp. The theory of ends, pushdown automata, and second order logic. Theoretical Computer Science, 37:51–75, 1985.

    Article  MATH  MathSciNet  Google Scholar 

  25. D.E. Muller and P.E. Schupp. Alternating automata on infinite trees. Theoretical Computer Science, 54:267–276, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  26. W. Peng and S. P. Iyer. A new typee of pushdown automata on infinite tree. IJFCS, 6(2):169–186, 1995.

    Article  MATH  Google Scholar 

  27. A. Pnueli. The temporal logic of programs. In 18th FOCS, pp. 46–57, 1977.

    Google Scholar 

  28. A. Pnueli. Linear and branching structures in the semantics and logics of reactive systems. In 12th ICALP, pp. 15–32. Springer-Verlag, 1985.

    Google Scholar 

  29. J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th Int. Symp. on Programming, LNCS 137, pp. 337–351, 1981.

    Google Scholar 

  30. M.O. Rabin. Decidability of second order theories and automata on infinite trees. Transaction of the AMS, 141:1–35, 1969.

    Article  MATH  MathSciNet  Google Scholar 

  31. A. Sistla, E.M. Clarke, N. Francez, and Y Gurevich. Can message buffers be axiomatized in linear temporal logic. Information and Control, 63(1/2):88–112, 1984.

    Article  MATH  MathSciNet  Google Scholar 

  32. W. Thomas. A short introduction to infinite automata. In 5th. DLT, LNCS 2295, pp. 130–144. Springer-Verlag, July 2001.

    Google Scholar 

  33. M.Y. Vardi. Reasoning about the past with two-way automata. In 25th ICALP, LNCS 1443, pp. 628–641. Springer-Verlag, 1998.

    Google Scholar 

  34. M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In 1st LICS, pp. 332–344, 1986.

    Google Scholar 

  35. I. Walukiewicz. Pushdown processes: Games and model-checking. Information and Computation, 164(2):234–263, 2001.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Engineering and Computer Science, Hebrew University, Jerusalem, 91904, Israel

    Orna Kupferman

  2. Department of Computer Science, Weizmann Institute of Science, Rehovot, 76100, Israel

    Nir Piterman

  3. Department of Computer Science, Rice University, Houston, TX, 77251-1892, USA

    Moshe Y. Vardi

Authors
  1. Orna Kupferman
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nir Piterman
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Moshe Y. Vardi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Abteilung für Theoretische Informatik, Institut für Algebra und Diskrete Mathematik, Wiedner Hauptstr. 8-10, 1040, Wien, Austria

    Matthias Baaz

  2. Department of Computer Science, University of Manchester, Kilburn Building, Oxford Road, Manchester, M13, 9PL, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kupferman, O., Piterman, N., Vardi, M.Y. (2002). Pushdown Specifications. In: Baaz, M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2002. Lecture Notes in Computer Science(), vol 2514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36078-6_18

Download citation

  • DOI: https://doi.org/10.1007/3-540-36078-6_18

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00010-5

  • Online ISBN: 978-3-540-36078-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation