We propose a new approach for proving safety of infinite state systems. It extends the analyzed system by transitive relations until its diameter D becomes finite, i.e., until constantly many steps suffice to cover all reachable states, irrespective of the initial state. Then we can prove safety by checking that no error state is reachable in D steps. To deduce transitive relations, we use recurrence analysis. While recurrence analyses can usually find conjunctive relations only, our approach also discovers disjunctive relations by combining recurrence analysis with projections. An empirical evaluation of the implementation of our approach in our tool LoAT shows that it is highly competitive with the state of the art.

翻译：我们提出了一种证明无限状态系统安全性的新方法。该方法通过传递关系扩展被分析系统，直至其直径D变为有限，即无论初始状态如何，仅需常数步即可覆盖所有可达状态。随后，我们可通过验证在D步内无法到达任何错误状态来证明安全性。为推导传递关系，我们采用递归分析法。虽然递归分析通常仅能发现合取关系，但本方法通过将递归分析与投影技术相结合，还能发现析取关系。我们在工具LoAT中实现本方法的实证评估表明，其性能与当前最优技术相比具有高度竞争力。