Game semantics, recursion schemes and collapsible pushdown automata: a new approach to the algorithmics of infinite structures

Despite considerable progress over the past decade, the computer-aided verification of software remains a hugely challenging problem. There are two main reasons. First, programs are infinite-state systems, but verification tools of industrial scale are essentially finite-state technologies. Secondly, modern programs -- in which unbounded data types, complex memory operations, non-local control flow, higher-order constructs, and name bindings of various kinds etc. are key features -- can only be accurately modelled using highly-structured mathematical models, as studied in semantics. Relatively little is known about the algorithmic properties of such rich, often higher-order'', mathematical structures.This project concerns an approach to software verification by developing automatic techniques which deal directly with infinite-state systems that are highly accurate models of programs. Striking examples of such infinite-state models are fully abstract game semantics of higher-order procedural programs; these models can be represented as (variant classes of higher-order) pushdown automata. In recent years, there have been remarkable advances in the study of algorithmic properties of hierarchies of generically-defined infinite structures. A notable result is that ranked trees that are generated by higher-order recursion schemes have decidable monadic second-order theories (Ong LICS'06). Further there is a new variant hierarchy of higher-order pushdown automata, called collapsible pushdown automata, that are equi-expressive with higher-order recursion schemes (in the sense that they generate the same class of trees), subsuming well-known structures at low orders: trees at order 0 and 1 are respectively the regular (Rabin 1969) and algebraic (Courcelle 1995) trees. The discovery of this rich, unifying and robust hierarchy of trees with excellent model-checking properties sparked the present research proposal.We have two general goals: - First we plan to study the connexions between the two closely-related higher-order families of generators (i.e. recursion schemes and collapsible pushdown automata), to explore the logical-algorithmic theory of infinite structures generated by them, and to derive (local and global) model checking algorithms. - Secondly we aim to develop verification techniques and construct efficient implementations of symbolic model-chekcers of reachability and temporal logics for these infinite structures of low orders. Why is it important to pursue these goals?- First, these hierarchies of infinite structures lie at the very frontier of infinite-state verification. The family of ranked trees thus generated is, to date, the largest generically-defined family of trees known to have decidable monadic second-order (MSO) theories; the family of transition graphs thus generated (does not have decidable MSO theories but) is, to date, the largest that is known to have decidable modal mu-calculus theories. These are significant indicators of our understanding of the subject, as MSO logic is the gold standard of languages for describing model-checking properties in computer-aided verification. - Secondly, these hierarchies of infinite structures are (representations of) highly accurate models of computation for higher-order procedural programs (such as OCAML, Haskell and F#). Recent results in (algorithmic) game semantics have shown that they underpin the computer-aided verification of these programs, an important and challenging direction for the next generation of software model checkers.