行为时序逻辑：Liveness 和 Fairness

TLA 里有两大逻辑：命题逻辑（Propositional Logic）和时序逻辑（Temporal Logic）。第七章是是《Specifying Systems》中时序逻辑的引入章，从仅仅讨论命题逻辑到开始讨论时序逻辑，命题逻辑可以规约系统的 Safety 特性，有了时序逻辑后，我们终于可以规约系统的 Liveness 特性了。本文是第七章的小结。文章不仅仅是公式笔记，也包括了少许的个人观点。