Skip to main content
SpringerLink
Log in

A Saturation Method for Collapsible Pushdown Systems

  • Conference paper
Automata, Languages, and Programming (ICALP 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7392))

Included in the following conference series:

Abstract

We introduce a natural extension of collapsible pushdown systems called annotated pushdown systems that replaces collapse links with stack annotations. We believe this new model has many advantages. We present a saturation method for global backwards reachability analysis of these models that can also be used to analyse collapsible pushdown systems. Beginning with an automaton representing a set of configurations, we build an automaton accepting all configurations that can reach this set. We also improve upon previous saturation techniques for higher-order pushdown systems by significantly reducing the size of the automaton constructed and simplifying the algorithm and proofs.

Supported by Fond. Sci. Math. Paris, AMIS (ANR 2010 JCJC 0203 01 AMIS), FREC (ANR 2010 BLAN 0202 02 FREC) and VAPF (Région IdF). The full version of this paper is available from http://hal.archives-ouvertes.fr/hal-00694991 .

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Atig, M.F.: Global model checking of ordered multi-pushdown systems. In: FSTTCS, pp. 216–227 (2010)

    Google Scholar 

  2. Ball, T., Rajamani, S.K.: The SLAM project: Debugging system software via static analysis. In: POPL, pp. 1–3 (2002)

    Google Scholar 

  3. Benois, M.: Parties rationnelles du groupe libre. Comptes-Rendus de l’Acamdémie des Sciences de Paris, Série A, 1188–1190 (1969)

    Google Scholar 

  4. Bouajjani, A., Esparza, J., Maler, O.: Reachability Analysis of Pushdown Automata: Application to Model-Checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  5. Bouajjani, A., Meyer, A.: Symbolic Reachability Analysis of Higher-Order Context-Free Processes. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 135–147. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  6. Broadbent, C.H., Carayol, A., Ong, C.-H.L., Serre, O.: Recursion schemes and logical reflection. In: LiCS, pp. 120–129 (2010)

    Google Scholar 

  7. Cachat, T.: Games on Pushdown Graphs and Extensions. PhD thesis, RWTH Aachen (2003)

    Google Scholar 

  8. Carayol, A.: Regular Sets of Higher-Order Pushdown Stacks. In: Jedrzejowicz, J., Szepietowski, A. (eds.) MFCS 2005. LNCS, vol. 3618, pp. 168–179. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  9. Carayol, A., Wöhrle, S.: The Caucal Hierarchy of Infinite Graphs in Terms of Logic and Higher-Order Pushdown Automata. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 112–123. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  10. Chandra, A.K., Kozen, D., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114–133 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  11. Damm, W.: The IO- and OI-hierarchies. Theor. Comput. Sci. 20, 95–207 (1982)

    Article  MathSciNet  MATH  Google Scholar 

  12. Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient Algorithms for Model Checking Pushdown Systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  13. Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. Electr. Notes Theor. Comput. Sci. 9, 27–37 (1997)

    Article  Google Scholar 

  14. Hague, M., Murawski, A.S., Ong, C.-H.L., Serre, O.: Collapsible pushdown automata and recursion schemes. In: LiCS, pp. 452–461 (2008)

    Google Scholar 

  15. Hague, M., Ong, C.-H.L.: Symbolic backwards-reachability analysis for higher-order pushdown systems. Logical Methods in Computer Science 4(4) (2008)

    Google Scholar 

  16. Hague, M., Ong, C.-H.L.: Analysing Mu-Calculus Properties of Pushdown Systems. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol. 6349, pp. 187–192. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  17. Hague, M., Ong, C.-H.L.: A saturation method for the modal μ-calculus over pushdown systems. Inf. Comput. 209(5), 799–821 (2010)

    Article  MathSciNet  Google Scholar 

  18. Kartzow, A., Parys, P.: Strictness of the Collapsible Pushdown Hierarchy. arXiv:1201.3250v1 [cs.FL] (2012)

    Google Scholar 

  19. Knapik, T., Niwiński, D., Urzyczyn, P.: Higher-Order Pushdown Trees Are Easy. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 205–222. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  20. Knapik, T., Niwiński, D., Urzyczyn, P., Walukiewicz, I.: Unsafe Grammars and Panic Automata. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1450–1461. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  21. Kobayashi, N.: Higher-order model checking: From theory to practice. In: LiCS, pp. 219–224 (2011)

    Google Scholar 

  22. Kobayashi, N.: A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 260–274. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  23. Maslov, A.N.: Multilevel stack automata. Problems of Information Transmission 15, 1170–1174 (1976)

    Google Scholar 

  24. Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: LiCS, pp. 81–90 (2006)

    Google Scholar 

  25. Ong, C.-H.L., Ramsay, S.J.: Verifying higher-order functional programs with pattern-matching algebraic data types. In: POPL, pp. 587–598 (2011)

    Google Scholar 

  26. Parys, P.: Collapse operation increases expressive power of deterministic higher order pushdown automata. In: STACS, pp. 603–614 (2011)

    Google Scholar 

  27. Reps, T.W., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program. 58(1-2), 206–263 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  28. Salvati, S., Walukiewicz, I.: Krivine Machines and Higher-Order Schemes. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 162–173. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  29. Schwoon, S.: Model-checking Pushdown Systems. PhD thesis, Technical University of Munich (2002)

    Google Scholar 

  30. Seth, A.: An alternative construction in symbolic reachability analysis of second order pushdown systems. In: RP, pp. 80–95 (2007)

    Google Scholar 

  31. Seth, A.: Games on Higher Order Multi-stack Pushdown Systems. In: Bournez, O., Potapov, I. (eds.) RP 2009. LNCS, vol. 5797, pp. 203–216. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  32. Suwimonteerabuth, D., Esparza, J., Schwoon, S.: Symbolic Context-Bounded Analysis of Multithreaded Java Programs. In: Havelund, K., Majumdar, R. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 270–287. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  33. Suwimonteerabuth, D., Schwoon, S., Esparza, J.: Efficient Algorithms for Alternating Pushdown Systems with an Application to the Computation of Certificate Chains. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 141–153. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIAFA, Université Paris Diderot – Paris 7 & CNRS, France

    Chris Broadbent, Matthew Hague & Olivier Serre

  2. LIGM, Université Paris-Est & CNRS, France

    Arnaud Carayol & Matthew Hague

Authors
  1. Chris Broadbent
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Arnaud Carayol
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Matthew Hague
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Olivier Serre
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Centre for Discrete Mathematics and its Applications, University of Warwick, Warwick, UK

    Artur Czumaj

  2. Max-Planck-Institut für Informatik, Saarbrücken, Germany

    Kurt Mehlhorn

  3. Computer Laboratory,, University of Cambridge, UK

    Andrew Pitts

  4. ETH Zurich, Switzerland

    Roger Wattenhofer

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Broadbent, C., Carayol, A., Hague, M., Serre, O. (2012). A Saturation Method for Collapsible Pushdown Systems. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds) Automata, Languages, and Programming. ICALP 2012. Lecture Notes in Computer Science, vol 7392. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31585-5_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31585-5_18

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31584-8

  • Online ISBN: 978-3-642-31585-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation