计算树逻辑 CTL

状态公式语法 ​

CTL 公式在Kripke 结构公理库Kripke 结构Kripke structure · Kripke transition structure以状态转移和原子命题标记解释分支时间性质的状态模型。的状态上解释。除原子命题和布尔联结外，时间构造必须由路径量词 $A$ 或 $E$ 与时间算子配对：

$$EX\phi ,AX\phi ,E[\phi U\psi ],A[\phi U\psi ].$$

$E$ 表示存在一条从当前状态出发的路径，$A$ 表示所有此类路径。派生算子包括 $EF,AF,EG,AG$。

例如

$$K,s\models EX\phi$$

当且仅当存在后继 $s^{\prime }$ 满足 $\phi$；$AX\phi$ 则要求每个后继都满足。对 total Kripke 结构，每个状态至少有一个后继；非 total 模型需先声明末端语义。

路径量词与时序算子成对 ​

$EFp$ 表示存在路径最终到达 $p$ 状态，$AFp$ 表示每条路径最终都到达 $p$。$EGp$ 表示存在一条无限路径始终保持 $p$，$AGp$ 表示所有可达未来状态都保持 $p$。

CTL 不是“给一个任意 LTL 公式前加一次 A 或 E”。公式 $E(GFp)$ 在 CTL* 中合法，经典 CTL 却不合法，因为内部 $F$ 没有重新与路径量词配对。CTL 的受限语法正是其高效状态集合算法的来源之一。

写自然语言时也要保留量词作用域。$AG(EFreset)$ 表示每个可达状态都有某条恢复路径；$EF(AGstable)$ 表示存在一条有限前缀到达一个此后所有分支都稳定的状态。交换算子会改变性质。

恢复服务的分支例子 ​

状态 degraded 有两条后继：一条进入 repairing 并最终到 healthy，另一条进入 failed 自环。于是初始状态满足

$$EFhealthy,$$

因为存在成功修复路径；却不满足

$$AFhealthy,$$

因为失败分支永远到不了健康状态。

若每个可达状态都至少保留一条通向 healthy 的路径，则 $AG(EFhealthy)$ 成立。它仍不保证实际调度必然选择修复路径；那需要 $AFhealthy$ 或加入公平性后重新量化路径。

只检查状态图中“能找到 healthy”会误把存在性当全称性，这正是 CTL 用 $E/A$ 明确分开的错误。

以状态集合求值 ​

对每个子公式 $\phi$，模型检查算法计算满足状态集合 $\mathrm{Sat}(\phi )$。例如

$$\mathrm{Sat}(EX\phi )=\mathrm{Pre}(\mathrm{Sat}(\phi )).$$

$E[\phi U\psi ]$ 是单调方程

$$Z=\mathrm{Sat}(\psi )\cup (\mathrm{Sat}(\phi )\cap \mathrm{Pre}(Z))$$

的最小不动点；$EG\phi$ 则是

$$Z=\mathrm{Sat}(\phi )\cap \mathrm{Pre}(Z)$$

的最大不动点。有限状态空间中迭代至集合不再变化即可。

这些等式也解释为何 $EU$ 与 $EG$ 不能共用同一初值和收敛方向。前者从空集增长，后者从全状态集合收缩。

表达边界 ​

CTL 能表达“从每个状态存在一条继续恢复的路径”，却不能表达某些沿同一条路径反复出现的性质；LTL 能表达 $GFp$ 的全路径版本，却不直接表达混合分支选择。两者一般不可互相包含。

更强的 CTL* 允许状态公式与路径公式两层自由嵌套，但表达力增加不意味着规格更易读，也不意味着所有算法保持 CTL 的复杂度。

CTL 模型检查仍只验证给定状态图。若 Kripke 标记或转移遗漏实现行为，精确的不动点计算会精确回答错误模型的问题。

全称算子可用存在算子和否定对偶化，例如 $AX\phi \equiv \mathrm{\neg }EX\mathrm{\neg }\phi$、$AG\phi \equiv \mathrm{\neg }EF\mathrm{\neg }\phi$。until 的全称对偶不能靠交换一个字母直接得到，必须同时处理“目标永不到达且左式持续成立”的分支；实现语法归约时遗漏该无限情形会把 liveness 公式算错。

参考资料

• Edmund M. Clarke and E. Allen Emerson, “Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic,” Logic of Programs, Springer, 1981, pp. 52–71。
• E. Allen Emerson and Joseph Y. Halpern, “Decision Procedures and Expressiveness in the Temporal Logic of Branching Time,” JCSS 30(1), 1985, pp. 1–24。
• Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press, 2008, Ch. 6。