一句话：提出一族几乎公平模拟关系及演绎系统，用于证明带Büchi公平条件的迁移系统的公平迹包含。
标准模拟无法证明活性性质；公平模拟虽可处理公平性假设与要求，但定义常涉及归纳与余归纳的复杂嵌套，难以用于交互式验证。本文针对带 Büchi 公平条件的迁移系统，从已有公平模拟技术出发，逐步构造一族 almost fair simulation 关系，控制不动点交替，并为每种关系给出直观推理规则，形成证明公平迹包含的演绎系统。作者在 Rocq 证明助手中机器化这些关系及演绎系统，证明其可靠性，并通过若干示例展示其可用性。
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 Büchi 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.