参数化系统中陷阱不变量的诱导
Abduction of trap invariants in parameterized systems
摘要：
在之前的一篇论文中，我们提出了一种CEGAR方法，用于验证具有任意数量的以阵列或环形式组织的进程的参数化系统。该技术基于参数化不变量的迭代计算，即，系统的无穷多个实例的无穷多个不变量族。安全性证明了检查，满足所有参数化的不变量的系统的每一个全球配置也满足的财产，我们已经证明，这种检查可以减少到一元二阶的可满足性问题的话，这是可判定的。该方法的一个很大的局限性是过程只能有固定数量的变量和固定的有限范围。特别是，它们不能使用范围为[0，N-1]的变量，其中N是进程的数量，这出现在许多标准的分布式算法中。在本文中，我们将我们的技术扩展到这种情况。在进行检查是否安全属性是归纳假设一组计算的不变量变得不可判定，我们展示了如何减少它检查满足的一阶公式。我们报告的实验表明，自动一阶定理证明器仍然可以执行这种检查的非平凡的例子的集合。此外，我们可以为这些检查提供一小部分可读的不变量。
英文摘要：
In a previous paper we have presented a CEGAR approach for the verification of parameterized systems with an arbitrary number of processes organized in an array or a ring. The technique is based on the iterative computation of parameterized invariants, i.e., infinite families of invariants for the infinitely many instances of the system. Safety properties are proved by checking that every global configuration of the system satisfying all parameterized invariants also satisfies the property; we have shown that this check can be reduced to the satisfiability problem for Monadic Second Order on words, which is decidable. A strong limitation of the approach is that processes can only have a fixed number of variables with a fixed finite range. In particular, they cannot use variables with range [0,N-1], where N is the number of processes, which appear in many standard distributed algorithms. In this paper, we extend our technique to this case. While conducting the check whether a safety property is inductive assuming a computed set of invariants becomes undecidable, we show how to reduce it to checking satisfiability of a first-order formula. We report on experiments showing that automatic first-order theorem provers can still perform this check for a collection of non-trivial examples. Additionally, we can give small sets of readable invariants for these checks.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
