形式陈述

可容许执行是在系统转移规则之外还满足环境假设的执行，例如最多 $f$$f$ 个崩溃、消息最终交付、弱公平调度或特定同步界。算法性质应量化于所有可容许执行；安全性常对更宽执行集成立，活性则依赖公平性和时序假设。把环境承诺藏在证明中会导致错误规格。

直觉

状态机列出所有可能动作，可容许性再排除模型明确不考虑的恶意调度或过多故障。

例子与边界

若活性要求每个持续启用动作最终执行，就必须写出公平性。异步可靠信道可允许任意长但有限延迟，不等于已知上界。FLP 的不终止执行满足其模型中的可容许条件；随意称其“不现实调度”不能反驳定理。

推论与应用

可容许执行精确承载故障、调度和网络假设，是陈述共识、选主和自稳定正确性的基础。

参考资料

• Nancy A. Lynch, Distributed Algorithms, Morgan Kaufmann, 1996，Chs. 1–25。
• Hagit Attiya and Jennifer Welch, Distributed Computing: Fundamentals, Simulations, and Advanced Topics, 2nd ed., Wiley, 2004，Chs. 1–18。