近乎公平的仿真

众所周知，活性属性无法使用标准仿真论证来证明。通过为配备额外公平条件（建模活性假设或活性要求的系统）的系统扩展标准仿真概念，已缓解了这一问题。在有限状态系统的自动化验证中，仿真证明是一种引人注目的办法，因为存在高效算法来查找两个系统之间的仿真。然而，公平仿真在交互式验证中的应用要少得多。或许一个原因是，公平仿真关系的定义通常涉及归纳和共理关系的非平凡嵌套，使得它们在使用和推理方面尤为困难。本文我们论证，在许多情况下，使用包含更多受控固定点交替的更强的公平仿真概念就足够了。从已知的公平仿真技术出发，我们逐步构建一套针对配备Buechi公平条件的迁移系统的近乎公平仿真关系。我们提出的仿真关系都可以配合直观的推理规则，导致优雅的公平迹路包含的演绎系统。我们在Rocq证明助手中实现了我们的仿真关系及其相关的演绎系统，证明了它们的可靠性，并通过一组示例展示了它们的用途。