Abstract
We propose a model-based approach to the model checking problem for recursive schemes. Since simply typed lambda calculus with the fixpoint operator, λY-calculus, is equivalent to schemes, we propose the use a model of λY to discriminate the terms that satisfy a given property. If a model is finite in every type, this gives a decision procedure. We provide a construction of such a model for every property expressed by automata with trivial acceptance conditions and divergence testing. Such properties pose already interesting challenges for model construction. Moreover, we argue that having models capturing some class of properties has several other virtues in addition to providing decidability of the model-checking problem. As an illustration, we show a very simple construction transforming a scheme to a scheme reflecting a property captured by a given model.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aehlig, K.: A finite semantics of simply-typed lambda terms for infinite runs of automata. Logical Methods in Computer Science 3(3) (2007)
Amadio, R.M., Curien, P.-L.: Domains and Lambda-Calculi. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (1998)
Barendregt, H.: The Lambda Calculus, Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland (1984)
Broadbent, C., Carayol, A., Ong, L., Serre, O.: Recursion schemes and logical reflection. In: LICS, pp. 120–129 (2010)
Broadbent, C., Carayol, A., Hague, M., Serre, O.: A saturation method for collapsible pushdown systems. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol. 7392, pp. 165–176. Springer, Heidelberg (2012)
Eilenberg, S.: Automata, Languages and Machines. Academic Press, New York (1974)
Haddad, A.: IO vs OI in higher-order recursion schemes. In: FICS. EPTCS, vol. 77, pp. 23–30 (2012)
Hague, M., Murawski, A.S., Ong, C.-H.L., Serre, O.: Collapsible pushdown automata and recursion schemes. In: LICS, pp. 452–461 (2008)
Kobayashi, N.: Higher-order program verification and language-based security. In: Datta, A. (ed.) ASIAN 2009. LNCS, vol. 5913, pp. 17–23. Springer, Heidelberg (2009)
Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: POPL, pp. 416–428. ACM (2009)
Kobayashi, N.: Types and recursion schemes for higher-order program verification. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 2–3. Springer, Heidelberg (2009)
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)
Kobayashi, N., Ong, L.: A type system equivalent to modal mu-calculus model checking of recursion schemes. In: LICS, pp. 179–188 (2009)
Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS, pp. 81–90 (2006)
Ong, C.-H.L., Tsukada, T.: Two-level game semantics, intersection types, and recursion schemes. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol. 7392, pp. 325–336. Springer, Heidelberg (2012)
Salvati, S., Manzonetto, G., Gehrke, M., Barendregt, H.: Loader and Urzyczyn are logically related. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol. 7392, pp. 364–376. Springer, Heidelberg (2012)
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)
Salvati, S., Walukiewicz, I.: Recursive schemes, Krivine machines, and collapsible pushdown automata. In: Finkel, A., Leroux, J., Potapov, I. (eds.) RP 2012. LNCS, vol. 7550, pp. 6–20. Springer, Heidelberg (2012)
Salvati, S., Walukiewicz, I.: Using models to model-check recursive schemes. Technical report, LaBRI (2012), http://hal.inria.fr/hal-00741077
Terui, K.: Semantic evaluation, intersection types and complexity of simply typed lambda calculus. In: RTA. LIPIcs, vol. 15, pp. 323–338. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)
Walukiewicz, I.: Simple models for recursive schemes. In: Rovan, B., Sassone, V., Widmayer, P. (eds.) MFCS 2012. LNCS, vol. 7464, pp. 49–60. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Salvati, S., Walukiewicz, I. (2013). Using Models to Model-Check Recursive Schemes. In: Hasegawa, M. (eds) Typed Lambda Calculi and Applications. TLCA 2013. Lecture Notes in Computer Science, vol 7941. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38946-7_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-38946-7_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38945-0
Online ISBN: 978-3-642-38946-7
eBook Packages: Computer ScienceComputer Science (R0)