TLA⁺ 里能表达可达性性质吗？
来源: ahelwer.ca — 2026-09-26
概述
作者读到 Hillel Wayne 说 TLA⁺ 无法表达可能性与可达性性质（「我总能关机」「用户总能改密码」），又回头重读 Lamport《A Science of Concurrent Programs》5.1 节，终于搞懂了并用更好理解的方式重讲一遍。他分两问作答：用 TLC 做可达性模型检查可以，但必须改造 TLC；而可达性性质在 TLA⁺ 语义下并不算异端——它看着像分支时间逻辑，实际是良性的。
核心要点
- <>P 表达的是「所有行为中 P 至少发生一次」，可达性要的是「对每个行为前缀，都存在某个行为使 P 发生」。
- ENABLED A 表示当前状态可以执行动作 A，[]ENABLED Next 为假就意味着系统死锁，TLC 默认会检查。
- 基本的单步可达性 [](ENABLED Next /\ P') 今天就能被 TLC 检查。
- Lamport 用上标 ⁺ 表示一个或多个动作串联，完整可达性写作 [](ENABLED [Next]_v⁺ /\ P')，TLC 目前还检查不了。
- TLC 新增了 _POSSIBLE P，只能检查从初始状态出发 P 是否有可能成立，目前仍是 beta。
- 作者确认可达性性质并没有把分支时间逻辑偷渡进线性时间逻辑。
金句
它看起来可疑地像分支时间逻辑——是异端！但结果出人意料地没问题。
👍 0
👎 0
← 返回 Lobsters 首页