论文标题
从单调理论中具有可证明的复杂性的不变推论
Invariant Inference With Provable Complexity From the Monotone Theory
论文作者
论文摘要
不变的推理算法（例如基于插值的推理和IC3/PDR）表明，在实践中，为许多有趣的系统找到归纳不变性是可行的，但是对于此类算法的计算复杂性，非平凡的上限是稀缺的，并且限于简单语法形式的不变形式。在本文中，我们在命题过渡系统的领域中实现了不变的推理算法，在SAT呼叫的数量上具有可证明的上限。我们通过基于单调理论的构建来做到这一点，该理论由Bshouty开发，用于精确学习布尔公式。我们证明了两个不变推理框架的结果：（i）基于模型的插值，在其中，我们表明了一种算法，在某些条件下，在有关可及性的某些条件下，当它们具有短的CNF和DNF表示时（超越有关单调不变的先前结果）时，它们有效地渗透了不变性。 （ii）基于单调理论的域中的抽象解释，该理论先前已经研究了有关属性指导的可达性，我们提出了有效的最佳抽象变压器的实施，从而导致SAT呼叫数量的总体复杂性界限。这些结果建立在一个新的程序上，用于计算最小单调过度贴imimation。
Invariant inference algorithms such as interpolation-based inference and IC3/PDR show that it is feasible, in practice, to find inductive invariants for many interesting systems, but non-trivial upper bounds on the computational complexity of such algorithms are scarce, and limited to simple syntactic forms of invariants. In this paper we achieve invariant inference algorithms, in the domain of propositional transition systems, with provable upper bounds on the number of SAT calls. We do this by building on the monotone theory, developed by Bshouty for exact learning Boolean formulas. We prove results for two invariant inference frameworks: (i) model-based interpolation, where we show an algorithm that, under certain conditions about reachability, efficiently infers invariants when they have both short CNF and DNF representations (transcending previous results about monotone invariants); and (ii) abstract interpretation in a domain based on the monotone theory that was previously studied in relation to property-directed reachability, where we propose an efficient implementation of the best abstract transformer, leading to overall complexity bounds on the number of SAT calls. These results build on a novel procedure for computing least monotone overapproximations.
