Higher-Order Model Checking
NII Shonan Meeting:
@ Shonan Village Center, March 14-17, 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.