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

尽管在过去十年中取得了长足的进步，但计算机辅助软件验证仍然是一个极具挑战性的问题。这主要有两个原因。首先，程序是无限状态系统，但工业规模的验证工具本质上是有限状态技术。其次，现代程序--其中无界数据类型、复杂的内存操作、非本地控制流、高阶结构和各种类型的名称绑定等是关键特性--只能使用高度结构化的数学模型准确地建模，正如在语义中所研究的那样。关于这种丰富的，通常是更高阶的数学结构的算法性质，人们知之甚少。这个项目涉及一种通过开发自动技术来进行软件验证的方法，该技术直接处理无限状态系统，这些系统是程序的高精度模型。这种无限状态模型的显著例子是高阶过程性程序的完全抽象的博弈语义；这些模型可以表示为(高阶的变体类)下推自动机。近年来，对一般定义的无限结构层次的算法性质的研究取得了显著进展。一个值得注意的结果是，由高阶递归方案生成的排序树具有可判定的一元二阶理论(Ong LICs‘06)。此外，还有一个新的高阶下推自动机的变体系列，称为可折叠下推自动机，它与高阶递归方案等价(在某种意义上，它们生成相同的树)，在低阶包含众所周知的结构：0阶和1阶的树分别是正则树(Rabin 1969)和代数树(Courcelle 1995)。这种丰富的、统一的、健壮的、具有良好的模型检测性质的树层次结构的发现引发了目前的研究建议。我们有两个总体目标：-首先，我们计划研究两个密切相关的高阶生成器族(即递归方案和可折叠下推自动机)之间的联系，探索由它们生成无限结构的逻辑算法理论，并推导(局部和全局)模型检测算法。-其次，我们的目标是开发验证技术，并为这些低阶无限结构构建符号模型可达性检查器和时序逻辑的有效实现。为什么追求这些目标很重要？-首先，这些无限结构的层次结构位于无限状态验证的最前沿。这样生成的排序树族是迄今为止已知的具有可判定的一元二阶(MSO)理论的最大的通用定义树族；这样生成的转移图族(没有可判定的MSO理论，但)是迄今已知的具有可判定的模u-演算理论的最大的树族。这些是我们对这一主题理解的重要指标，因为MSO逻辑是描述计算机辅助验证中的模型检查属性的语言的黄金标准。-其次，这些无限结构的层次结构是高阶过程程序(如OCAML、Haskell和F#)的高精度计算模型(表示)。(算法)游戏语义学的最新结果表明，它们是这些程序的计算机辅助验证的基础，对于下一代软件模型检查器来说，这是一个重要且具有挑战性的方向。

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.