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理论，但是）是迄今为止已知的具有可确定模态模微积分理论的最大的。这些是我们对主题理解的重要指标，因为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.