18 hours ago
- 作者引入了线性时态逻辑中的时态算子A（总是）和E（最终）来表达系统属性，涵盖安全性和活性。
- 第三类属性P（可能性）询问模型中某事是否可能发生，即使不能保证；这包括可达性属性。
- 组合算子可得到如A(P(x))（总是可能）和A(x => P(y))（从任何x为真的状态，y是可能的）等表达式，这些无法仅用A和E表示。
- P的主要用途是作为规范的正确性检查：验证像'重试'这样的状态是否实际可达，以避免活性属性的平凡满足。
- Alloy和TLA+等工具本身不支持P；简单可达性可通过检查A(!x)的反例来模拟，但像A(P(x))这样的组合算子更难验证。
- 作者指出一个鸡生蛋蛋生鸡的问题：由于工具无法验证可能性属性，实践者不习惯在系统设计中注意到它们。