计算树逻辑

计算树逻辑（Computation Tree Logic，CTL）是一种分支时间逻辑。一个状态可能因不同输入或调度选择而有多个后继；从当前状态把所有后续运行展开，就得到计算树。CTL公式在状态上求值，既能约束所有可能的未来，也能要求某一种未来存在。

常见语义使用带命题标记的克里普克结构：状态表示系统配置，边表示允许的一步转移，标记说明哪些命题成立。通常假定每个状态至少有一个后继，因此路径可以无限延伸；需要表示终止状态时，可明确约定自循环等处理。性质是否成立取决于这个模型，而非仅取决于公式文字。

参考：[2]

A表示所有从当前状态出发的路径，E表示至少一条这样的路径。X表示下一步，F表示最终某一步，G表示始终，U表示直到。CTL要求时序算子与路径量词配对，形成AX、EX、AF、EF、AG、EG以及A[p U q]、E[p U q]等状态公式，再用布尔联结词组合。

例如EX p只要求一个直接后继满足p，AX p要求全部直接后继满足p。A[p U q]要求每条路径终会出现q，且此前各状态满足p；“直到”在这里还包含q最终发生的要求。F、G通常从当前状态算起，不能一律理解为严格排除当前时刻的将来。

参考：[1]

设r表示设备已经恢复。EF r表示存在一条运行能到达恢复状态；AF r表示每条运行最终都会恢复。如果设备可选择重启成功，也可无限留在故障循环中，前一句可以为真，后一句却为假。这一区别在描述容错系统时非常关键。

AG EF r进一步要求：在每个可达状态，仍至少保留一条通向恢复的道路。它没有承诺实际调度会走这条路。还有一个容易混淆的例子：EF p与EF q同时成立，两个存在量词可以分别由不同路径见证，不能据此声称同一条运行会先后经历p和q。

参考：[1] [2]

模型检查把系统模型与性质公式一起输入工具，判断指定初始状态是否满足要求。对于AG safe之类的不变式，能找到通向不安全状态的路径就足以反驳；但包含复杂量词嵌套的性质，应按公式结构解释证据，不能把所有诊断都简化成同一种轨迹。

线性时序逻辑LTL首先描述单条运行上的时间关系，CTL则能在状态中反复选择路径量词。两者的表达能力一般不可互相包含，不能只在LTL每个时序算子前机械加A就得到等价CTL公式。CTL*允许更自由地组合状态公式和路径公式，包含这两类逻辑；选择哪种语言应由待表达的性质决定。

参考：[1] [2]