时序性质

这里从 safety 扩展到更难的系统性质。

前面的章节主要检查“坏事不会发生”。这里开始讨论“好事是否最终发生”、系统是否可能卡住，以及公平性假设为什么会改变验证结论。

计划覆盖：

safety
deadlock
liveness
fairness
temporal property