Skip to main content
SpringerLink
Log in

Recursion Schemes, Collapsible Pushdown Automata and Higher-Order Model Checking

  • Conference paper
Language and Automata Theory and Applications (LATA 2013)

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

Abstract

This paper is about two models of computation that underpin recent developments in the algorithmic verification of higher-order computation. Recursion schemes are in essence the simply-typed lambda calculus with recursion, generated from first-order symbols. Collapsible pushdown automata are a generalisation of pushdown automata to higher-order stacks — which are iterations of stack of stacks — that contain symbols equipped with links. We study and compare the expressive power of the two models and the algorithmic properties of infinite structures such as trees and graphs generated by them. We conclude with a brief overview of recent applications to the model checking of higher-order functional programs. A central theme of the work is the fruitful interplay of ideas between the neighbouring fields of semantics and algorithmic verification.

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. Aehlig, K.: A finite semantics of simply-typed lambda terms for infinite runs of automata. Logical Methods in Computer Science 3, 1–23 (2007)

    Article  MathSciNet  Google Scholar 

  2. Aehlig, K., de Miranda, J.G., Ong, C.-H.L.: The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidable. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 39–54. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  3. Aehlig, K., de Miranda, J.G., Ong, C.-H.L.: Safety Is not a Restriction at Level 2 for String Languages. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 490–504. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  4. Aho, A.: Indexed grammars - an extension of context-free grammars. J. ACM 15, 647–671 (1968)

    Article  MathSciNet  MATH  Google Scholar 

  5. de Bakker, J.W., de Roever, W.P.: A calculus for recursive program schemes. In: ICALP, pp. 167–196 (1972)

    Google Scholar 

  6. Blum, W.: The Safe Lambda Calculus. Ph.D. thesis, University of Oxford (2008)

    Google Scholar 

  7. Blum, W., Broadbent, C.: The CPDA-transform of a safe recursion scheme does not collapse (2009) (in preparation)

    Google Scholar 

  8. Blum, W., Ong, C.H.L.: The safe lambda calculus. LMCS 5(1) (2009)

    Google Scholar 

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

    Google Scholar 

  10. Carayol, A., Serre, O.: Collapsible pushdown automata and labeled recursion schemes: Equivalence, safety and effective selection. In: LICS, pp. 165–174 (2012)

    Google Scholar 

  11. Caucal, D.: On Infinite Transition Graphs Having a Decidable Monadic Theory. In: Meyer auf der Heide, F., Monien, B. (eds.) ICALP 1996. LNCS, vol. 1099, pp. 194–205. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  12. Caucal, D.: On Infinite Terms Having a Decidable Monadic Theory. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, pp. 165–176. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  13. Courcelle, B.: Fundamental properties of infinite trees. TCS 25, 95–169 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  14. Courcelle, B.: Recursive applicative program schemes. In: Handbook of Theoretical Computer Science, vol. B, pp. 459–492. MIT Press (1990)

    Google Scholar 

  15. Courcelle, B.: The monadic second-order logic of graphs IX: machines and their behaviours. Theoretical Computer Science 151, 125–162 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  16. Curien, P.L., Herbelin, H.: Computing with abstract Böhm trees. In: Fuji International Symposium on Functional and Logic Programming, pp. 20–39. World Scientific (1998)

    Google Scholar 

  17. Curien, P.L., Herbelin, H.: Abstract machines for dialogue games, coRR abs/0706.2544 (2007)

    Google Scholar 

  18. Damm, W.: Higher type program schemes and their tree languages. Theoretical Computer Science, pp. 51–72 (1977)

    Google Scholar 

  19. Damm, W.: The IO- and OI-hierarchy. TCS 20, 95–207 (1982)

    Article  MathSciNet  MATH  Google Scholar 

  20. Damm, W., Fehr, E., Indermark, K.: Higher type recursion and self-application as control structures. In: Neuhold, E. (ed.) Formal Descriptions of Programming Concepts, pp. 461–487. North-Holland, Amsterdam (1978)

    Google Scholar 

  21. Damm, W., Goerdt, A.: An automata-theoretical characterization of the OI-hierarchy. Information and Control 71, 1–32 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  22. Danos, V., Herbelin, H., Regnier, L.: Game semantics and abstract machines. In: LICS, pp. 394–405 (1996)

    Google Scholar 

  23. Duske, J., Parchmann, R.: Linear indexed languages. TCS 32, 47–60 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  24. Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: FOCS, pp. 368–377 (1991)

    Google Scholar 

  25. Engelfriet, J.: Interated stack automata and complexity classes. Information and Computation 95, 21–75 (1991)

    Article  MathSciNet  Google Scholar 

  26. Esparza, J., Schwoon, S.: A BDD-Based Model Checker for Recursive Programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 324–336. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  27. Gilman, R.H.: A shrinking lemma for indexed languages. TCS 163, 277–281 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  28. Guessarian, I.: Algebraic Semantics. Springer (1981)

    Google Scholar 

  29. 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 

  30. Hayashi, T.: On derivation trees of indexed grammars: An extension of the uvwxy-theorem. Publ. RIMS Kyoto Univ. 9, 61–92 (1983)

    Article  Google Scholar 

  31. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)

    Google Scholar 

  32. Hyland, J.M.E., Ong, C.H.L.: On Full Abstraction for PCF: I. Models, observables and the full abstraction problem, II. Dialogue games and innocent strategies, III. A fully abstract and universal game model. Information and Computation 163, 285–408 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  33. Inaba, K., Maneth, S.: The complexity of tree transducer output languages. In: FSTTCS, pp. 244–255 (2008)

    Google Scholar 

  34. Jones, N.D., Muchnick, S.S.: Complexity of finite memory programs with recursion. Journal of the Association for Computing Machinery 25, 312–321 (1978)

    Article  MathSciNet  MATH  Google Scholar 

  35. Kartzow, A., Parys, P.: Strictness of the Collapsible Pushdown Hierarchy. In: Rovan, B., Sassone, V., Widmayer, P. (eds.) MFCS 2012. LNCS, vol. 7464, pp. 566–577. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  36. 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 

  37. 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 

  38. Kobayashi, N.: Model-checking higher-order programs. In: PPDP, pp. 25–36 (2009)

    Google Scholar 

  39. Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: POPL, pp. 416–428 (2009)

    Google Scholar 

  40. Kobayashi, N., Ong, C.H.L.: A type theory equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In: LICS, pp. 179–188 (2009)

    Google Scholar 

  41. 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 

  42. Kobayashi, N., Ong, C.H.L.: Complexity of model checking recursion schemes for fragments of the modal mu-calculus. LMCS 7(4) (2011)

    Google Scholar 

  43. Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and cegar for higher-order model checking. In: PLDI, pp. 222–233 (2011)

    Google Scholar 

  44. Lautemann, C., Schwentick, T., Thérien, D.: Logics for Context-Free Languages. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 205–216. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  45. Maslov, A.N.: The hierarchy of indexed languages of an arbitrary level. Soviet Math. Dokl. 15, 1170–1174 (1974)

    MATH  Google Scholar 

  46. Maslov, A.N.: Multilevel stack automata. Problems of Information Transmission 12, 38–43 (1976)

    Google Scholar 

  47. de Miranda, J.: Structures generated by higher-order grammars and the safety constraint. Ph.D. thesis, University of Oxford (2006)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  49. Murawski, A.S., Ong, C.-H.L., Walukiewicz, I.: Idealized Algol with Ground Recursion, and DPDA Equivalence. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 917–929. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  50. Neatherway, R.P., Ramsay, S.J., Ong, C.H.L.: A traversal-based algorithm for higher-order model checking. In: ICFP, pp. 353–364 (2012)

    Google Scholar 

  51. Nivat, M.: Langages algébriques sur le magma libre et sémantique des schémas de programme. In: Proc. ICALP, pp. 293–308 (1972)

    Google Scholar 

  52. Nivat, M.: On the interpretation of recursive program schemes. Symposia Mathematica 15, 255–281 (1975)

    MathSciNet  Google Scholar 

  53. Ong, C.H.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS, pp. 81–90 (2006), www.cs.ox.ac.uk/people/luke.ong/personal/publications/lics06-long.pdf

  54. Ong, C.H.L.: Local computation of beta-reduction by game semantics (2012), www.cs.ox.ac.uk/people/luke.ong/personal/publications/locred.pdf (preprint)

  55. 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 

  56. Parchmann, R., Duske, J., Specht, J.: On deterministic indexed languages. Information and Control 45, 48–67 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  57. Park, D.M.R.: Fixpoint induction and proofs of program properties. In: Michie, D., Meltzer, B. (eds.) Machine Intelligence, vol. 5 (1970)

    Google Scholar 

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

    Google Scholar 

  59. Parys, P.: On the significance of the collapse operation. In: LICS, pp. 521–530 (2012)

    Google Scholar 

  60. Parys, P.: A pumping lemma for pushdown graphs of any level. In: STACS, pp. 54–65 (2012)

    Google Scholar 

  61. Patterson, M.: Equivalence problems in a model of computation. Ph.D. thesis, University of Cambridge (1967)

    Google Scholar 

  62. Plotkin, G.D.: LCF as a programming language. Theoretical Computer Science 5, 223–255 (1977)

    Article  MathSciNet  Google Scholar 

  63. Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. Amer. Maths. Soc. 141, 1–35 (1969)

    MathSciNet  MATH  Google Scholar 

  64. 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 

  65. Schwichtenberg, H.: Definierbare funktionen im lambda-kalkul mit typen. Archiv Logik Grundlagen-forsch 17 (1976)

    Google Scholar 

  66. Cachat, T.: Games on Pushdown Graphs and Extensions. Ph.D. thesis, RWTH Aachen (2003), http://www.liafa.jussieu.fr/~txc/Download/Cachat-PhD.pdf

  67. Walukiewicz, I.: Pushdown processes: games and model-checking. Information and Computation 157, 234–263 (2001)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Oxford, UK

    Luke Ong

Authors
  1. Luke Ong
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Research Group on Mathematical Linguistics, Universitat Rovira i Virgili, Avinguda Catalunya, 35, 43002, Tarragona, Spain

    Adrian-Horia Dediu  & Carlos Martín-Vide  & 

  2. Fakultät für Informatik, Institut für Wissens- und Sprachverarbeitung, Otto-von-Guericke-Universität Magdeburg, Universitätsplatz 2, 39106, Magdeburg, Germany

    Bianca Truthe

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ong, L. (2013). Recursion Schemes, Collapsible Pushdown Automata and Higher-Order Model Checking. In: Dediu, AH., Martín-Vide, C., Truthe, B. (eds) Language and Automata Theory and Applications. LATA 2013. Lecture Notes in Computer Science, vol 7810. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37064-9_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-37064-9_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-37063-2

  • Online ISBN: 978-3-642-37064-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation