What TLA+ can and can't check
9 hours ago
- TLA+ 对于验证并发系统的安全性和活性属性很有用，但它有局限性。
- 安全性属性（如不变式和动作属性）检查“坏事永远不会发生”。
- 活性属性（如 '[]<>P' 和 '<>[]P'）确保“最终会有好事发生”，例如终止或恢复。
- TLA+ 无法表达需要多步骤、浮点运算、实时或可达性的属性。
- TLA+ 无法检查存在性属性（例如，“存在一个行为使得P为真”）或超属性（例如，比较两个行为）。
- 超属性包括安全性和统计属性，例如“节能模式比正常模式使用更少的能量”。
- 一些局限性可以通过辅助变量、自组合或其他工具来绕过，但这些是复杂的技巧且有缺点。
- TLA+ 擅长许多常见的不变式和活性属性，但无法表达所有内容，因此它不是人工智能或软件正确性的银弹。