形式陈述

安全性质可由有限坏前缀反驳：一旦违反，有限观察已经足够证明。活性质要求每个有限执行前缀都还能扩展为满足性质的执行，因此任何有限前缀都不足以永久反驳。

直觉

安全性说“始终不出错”，活性说“系统不会永远停滞”。完整协议通常必须同时说明两者以及所依赖的调度和故障假设。

例子与边界

互斥是安全性：两进程同时进入临界区即可有限见证违规。每个请求最终得到响应是活性；等待很久仍不能证明它永远不会响应。

推论与应用

任何线性时间性质都可分解为安全部分与活性部分。共识分别要求一致性/有效性与终止性。

参考资料

• Bowen Alpern and Fred B. Schneider, “Defining Liveness,” 1985.
• Leslie Lamport, “Proving the Correctness of Multiprocess Programs,” 1977.