A Traversal-based Algorithm for Higher-Order Model Checking

Robin Neatherway

Higher-order model checking, the model checking of trees generated by higher-order recursion schemes (HORS), is a natural generalisation of finite-state and pushdown model checking. HORS can serve as an abstract model of functional programs, and we view them in this light as part of a verification procedure. In this talk we will explain where the HORS model checking problem fits into such a verification framework, extend them with a 'case' construct, and exhibit a new algorithm for solving the model checking problem. Kobayashi's work on HORS model checking showed how the problem can be reduced to one of type inference in an intersection type system. For our new, richer, abstract model -- higher-order recursion schemes with cases (HORSC) -- a more expressive type system with a limited form of union types is needed. Using this, together with the notion of 'traversals' from Ong's original proof of decidability of the HORS model checking problem, we obtain our algorithm.