Axe 'Em：消除虚假状态的归纳公理

一阶逻辑 (FOL) 已被证明是作为抽象建模语言的通用且富有表达力的工具。用于验证具有无界域的复杂系统（如堆操作程序和分布式协议），FOL，特别是无解释函数和量词，在表达性和自动化便利性之间取得了平衡。然而，FOL 语义在重要方面可能与被建模系统的预期语义不同，例如，无法区分有限与无限的一阶结构，或无法在 FOL 中定义良基关系。这种语义差距可能导致虚假状态和不真实行为，这些只是作为一阶抽象的副产品，阻碍了验证过程。本文致力于弥合这一语义差距。我们提出了一种根据良基语义或有限域语义对一阶抽象进行 sound 细化的方法，利用归纳公理处理抽象顺序关系，这是一种常见的验证原语。我们首先基于良基归纳 formalize 了每种上述语义的 sound 公理模式。其次，我们展示如何利用必然为无限的虚假 counter-model 来指导这些公理模式的实例化。最后，我们提出了将良基语义和有限域语义 sound 且 complete 地归约到最近发现的有序自环 (OSC) 片段中的标准语义，并证明在 OSC 中，这些语义的可满足性是可判定的。我们实现了一个原型工具来评估 our 方法，并在各种虚假模型出现的例子中对其进行测试。我们的工具迅速找到细化语义所需的公理，成功完成了验证过程。