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中的实现所进行的实证评估表明，该方法与当前最优技术相比具有极强的竞争力。