异步系统公平停顿精化的证明归约及其应用

我们提出了一系列定义和定理，展示了如何减少证明系统精化的要求，以确保包含公平停顿运行。这项工作的主要成果是能够将关于交互状态机系统运行的必要证明，归约为一组定义和检查，这些检查针对少量状态机的单步操作，对应于无饥饿和无死锁的直观概念。我们进一步细化了这些定义，以便在某些有限状态情况下提供高效的显式状态检查过程。我们在 Bakery 算法的多个版本上演示了这种证明归约。