It is well known that liveness properties cannot be proven using standard simulation arguments. This issue has been mitigated by extending standard notions of simulation for transition systems to fairness-preserving simulations for systems equipped with an additional fairness condition modeling liveness assumptions and/or liveness requirements. In the context of automated verification of finite-state systems, proofs by simulation are an appealing method as there exist efficient algorithms to find a simulation between two systems. However, applications of fair simulation to interactive verification have been much less studied. Perhaps one reason is that the definitions of fair simulation relations typically involve non-trivial nestings of inductive and coinductive relations, making them particularly difficult to use and to reason about. In this paper, we argue that in many cases, stronger notions of fair simulation involving more controlled alternations of fixed points are sufficient. Starting from known fair simulation techniques, we progressively build up a family of almost fair simulation relations for transition systems equipped with a Buechi fairness condition. The simulation relations we present can all be equipped with intuitive reasoning rules, leading to elegant deductive systems to prove fair trace inclusion. We mechanized our simulation relations and their associated deductive systems in the Rocq proof assistant, proved their soundness, and we demonstrate their use through a selection of examples.

翻译：众所周知，活性属性无法通过标准模拟论证来证明。这一问题已通过将转换系统的标准模拟概念扩展到带有额外公平性条件（模拟活性假设和/或活性需求）的系统的公平性保持模拟而得以缓解。在有限状态系统的自动验证背景下，模拟证明是一种有吸引力的方法，因为存在高效算法可寻找两个系统之间的模拟关系。然而，公平模拟在交互式验证中的应用研究却少得多。或许原因之一在于公平模拟关系的定义通常涉及归纳关系与共归纳关系的非平凡嵌套，这使得它们特别难以使用和推理。在本文中，我们认为在许多情况下，涉及更可控的不动点交替的更强公平模拟概念已足够。从已知的公平模拟技术出发，我们逐步构建了一个针对配备Buechi公平性条件的转换系统的几乎公平模拟关系族。我们所提出的模拟关系均可配备直观的推理规则，从而形成优雅的演绎系统来证明公平迹包含关系。我们在Rocq证明助手中实现了这些模拟关系及其关联的演绎系统，证明了它们的可靠性，并通过一系列示例展示了它们的应用。