A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes
A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes
复制标题
DOI：
10.1109/lics.2009.29
复制
发表时间：
2009-08
期刊：
影响因子：
--
通讯作者：
N. Kobayashi;C. Ong
中科院分区：
文献类型：
--
作者：
N. Kobayashi;C. Ong
高阶递归方案的模型检查在验证高阶程序中具有重要的应用。 ONG先前已经表明，订单-N递归方案生成的树的模态MU-Calculus模型检查已完成，但他的算法及其正确性证明非常复杂。我们提供了一种基于类型的验证方法：给定模态MU-Calculus公式，我们可以构建一个类型系统，在该系统中，只有该方案生成的（可能是无限，排名）的树时，递归方案是典型的。满足公式。因此，模型检查问题将减少为类型检查问题。我们基于类型的方法产生了一种简单的验证算法，其正确性证明（无需求助于游戏语义）就相对易于理解。此外，假设递归方案的非末端的公式和最大的阶和最大的顺序和最大阶段是固定的，则该算法是递归方案大小的多项式时间。
The model checking of higher-order recursion schemes has important applications in the verification of higher-order programs. Ong has previously shown that the modal mu-calculus model checking of trees generated by order-n recursion scheme is n-EXPTIME complete, but his algorithm and its correctness proof were rather complex. We give an alternative, type-based verification method: Given a modal mu-calculus formula, we can construct a type system in which a recursion scheme is typable if, and only if, the (possibly infinite, ranked) tree generated by the scheme satisfies the formula. The model checking problem is thus reduced to a type checking problem. Our type-based approach yields a simple verification algorithm, and its correctness proof (constructed without recourse to game semantics) is comparatively easy to understand. Furthermore, the algorithm is polynomial-time in the size of the recursion scheme, assuming that the formula and the largest order and arity of non-terminals of the recursion scheme are fixed.