NO.078 Higher-Order Model Checking
March 14 - 17, 2016 (Check-in: March 13, 2016 )
- Naoki Kobayashi
- The University of Tokyo, Japan
- Luke Ong
- University of Oxford, UK
- Igor Walukiewicz
- CNRS, LaBRI, Bordeaux University, France
Description of the meeting
Finite state model checking has been widely studied and successfully applied to system verification. The main theme of this meeting, higher-order model checking, is a generalization of finite state model checking, obtained by replacing finite state models with more expressive models called recursion schemes. Higher-order model checking has found applications in analysis of object-oriented and concurrent programs with recursion and higher-order procedures.
Recursion schemes are a kind of simply-typed grammar for generating possibly infinite ranked trees. A recursion scheme is a finite system of equations, defining a finite set of higher-order functions by mutual recursion. The order of a recursion scheme is given by the highest type-theoretic order of the functions defined by it. From a programming language perspective, recursion schemes may be viewed as programs (i.e. closed, ground-type terms) of the simply-typed lambda calculus with recursion, constructed from a set of uninterpreted function symbols. Higher-order model checking is the model checking of trees generated by recursion schemes. The higher-order model checking problem asks, given a recursion scheme G and a correctness property φ, whether the tree generated by G satisfies φ.
The early work in the 1970s on (tree-generating) higher-order recursion schemes was mostly about questions of expressivity. The decision problem was first posed in the present form by Knapik et al. [5, 6]. They considered recursion schemes subject to a syntactic constraint called safety. Their main result is that, when restricted to trees generated by safe recursion schemes, the higher-order model checking problem with respect to monadic second- order (MSO) properties is decidable. However the general MSO higher-order model checking problem was left open. In , Ong proved that the modal mu-calculus model checking problem of trees generated by arbitrary order-n recursion schemes is n-EXPTIME complete. Since MSO logic and the modal mu-calculus are equi-expressive over trees, the MSO higher-order model checking problem is decidable.
The last fifteen years or so have seen a growth of interest in higher-order model checking from both the theory and practice communities. Since the MSO decidability result , which was proved using insights from game semantics , a variety of semantic and algorithmic techniques and models of computation have been employed to design higher-order model checking algorithms, notably, intersection types [7, 11], collapsible pushdown automata  and Krivine machines . Algorithmic properties that refine and extend the decidability of MSO local model checking have also been introduced, such as logical reflection , effective selection  and transfer theorem . One recent trend, initiated by Salvati and Walukiewicz, is the development of effective denotational semantics for an approach to higher-order model checking by evaluation [18, 17, 21].
Recursion schemes are a very expressive family of generators of trees: the trees that are generated at orders 0, 1 and 2 are respectively the regular trees, algebraic trees (i.e. those generated by context-free tree grammars) and hyperalgebraic trees. There have been advances in the understanding of the relationship between higher-order families of generators. Hague et al.  showed that order-n recursion schemes generate the same class of trees as order-n collapsible pushdown automata. More recently, Parys  proved the Safety Conjecture, thus confirming the intuition that the safety constraint restricts the expressive power of recursion schemes, or equivalently that order-n collapsibile pushdown automata are more expressive than order-n pushdown automata.
Recursion schemes are thus an appealing abstract model for model checking higher-order programs: not only are they highly expressive, the trees they generate also enjoy a rich and decidable logical theory. In [7, 8], Kobayashi introduced an approach to the verification of safety properties of functional programs by reduction to higher-order model checking. His verification method is sound, complete, and automatic for a range of verification problems such as reachability, flow analysis, and resource usage for simply-typed recursive functional programs generated from finite base types. Although the worst-case complexity of higher-order model checking is hyper-exponential, there have been remarkable advances in the design of model checking algorithms. The time complexity of state-of-the-art model checking algorithms, PREFACE  and HORSATZDD , are fixed-parameter polynomial in the size of the recursion schemes, and scale readily to many thousands of rules. In addition to the model checking of object-oriented  and concurrent programs , higher-order model checking have found applications in program analysis , and data compression .
- Extensions of HOMC: beyond simple types (e.g. untyped and recursively typed recursion schemes, higher-type Böhm trees); beyond omega-regular properties: finitary parity, omega-B, stack unboundedness, etc.
- “Practical” HOMC algorithms. E.g. HORSATZDD, Preface, C-SHORe, etc.
- Applications of HOMC: program verification (functional, object-orientation, concurrency), program analysis, data compression, security, etc.
- Higher-order grammars and pushdown automata. Context sensitivity of unsafe Maslov languages and other open problems.
- Effective denotational semantics and strategy-aware models for HOMC. Compositional approaches to HOMC.
Format of the Meeting
We plan to organize some of the following activities:
- Survey and tutorial lectures
- Technical presentations
- Panel / thematic discussions
- Open problems session
- Demos of software tools
 Christopher H. Broadbent, Arnaud Carayol, C.-H. Luke Ong, and Olivier Serre. Recursion Schemes and Logical Reflection. In LICS, pages 120-129, 2010.
 Arnaud Carayol and Olivier Serre. Collapsible Pushdown Automata and Labeled Recursion Schemes: Equivalence, Safety and Effective Selection. In LICS, pages 165-174, 2012.
 Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre. Collapsible Pushdown Automata and Recursion Schemes. In LICS, pages 452-461, 2008.
 J. M. E. Hyland and C.-H. Luke Ong. On Full Abstraction for PCF: I, II and III. Information and Computation, 163(2):285-408, 2000.
 Teodor Knapik, Damian Niwiński, and Pawel Urzyczyn. Deciding monadic theories of hyperalgebraic trees. TLCA, pages 253-267, 2001.
 Teodor Knapik, Damian Niwiński, and Pawel Urzyczyn. Higher-order pushdown trees are easy. In FoSSaCS, pages 205-222, 2002.
 Naoki Kobayashi. Types and higher-order recursion schemes for verification of higher- order programs. In POPL, page 416, January 2009.
 Naoki Kobayashi. Model Checking Higher-Order Programs. JACM, 60(3), 2013.
 Naoki Kobayashi and Atsushi Igarashi. Model-Checking Higher-Order Programs with Recursive Types. In ESOP, pages 431-450, 2013.
 Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara, and Kazuya Yaguchi. Functional programs as compressed data. Higher-Order and Symbolic Computation, (2012):1-46, 2013.
 Naoki Kobayashi and C.-H. Luke Ong. A Type System Equivalent to the Modal Mu- Calculus Model Checking of Higher-Order Recursion Schemes. In LICS, pages 179-188, 2009.
 C.-H. Luke Ong. On Model Checking Trees Generated by Higher-Order Recursion Schemes. In LICS, pages 81-90, 2006.
 Pawe Parys. On the Significance of the Collapse Operation. In LICS, pages 521-530. IEEE, June 2012.
 Steven J. Ramsay, Robin P. Neatherway, and C.-H. Luke Ong. An Abstraction Refinement Approach to Higher-Order Model Checking. In POPL, pages 61-72, New York, USA, 2014. ACM Press.
 Sylvain Salvati and Igor Walukiewicz. Krivine machines and higher-order schemes. In ICALP, pages 162-173, 2011.
 Sylvain Salvati and Igor Walukiewicz. Evaluation is MSOL-compatible. In FSTTCS, pages 103-114, 2013.
 Sylvain Salvati and Igor Walukiewicz. Using Models to Model-Check Recursive Schemes. In TLCA, pages 189-204, 2013.
 Sylvain Salvati and Igor Walukiewicz. Typing Weak MSOL Properties. In FoSSaCS, volume 7794, pages 129-144, 2015.
 Taku Terao and Naoki Kobayashi. A ZDD-Based Efficient Higher-Order Model.?? In APLAS, pages 354-371, 2014.
 Yoshihiro Tobita, Takeshi Tsukada, and Naoki Kobayashi. Exact flow analysis by higher- order model checking. FLOPS, pages 275-289, 2012.
 Takeshi Tsukada and C.-H. Luke Ong. Compositional Higher-order Model Checking via omega-Regular Games over Boehm trees. In CSL-LICS, 2014.
 Kazuhide Yasukata, Naoki Kobayashi, and Kazutaka Matsuda. Pairwise Reachability Analysis for Higher Order Concurrent Programs by Higher-Order Model. In CONCUR, pages 312-326, 2014.