CTL*

形式陈述 ​

两层语法 ​

CTL* 明确区分状态公式 $\phi$ 与路径公式 $\psi$。一种核心语法是

$$\phi ::=p\mid \mathrm{\neg }\phi \mid (\phi \wedge \phi )\mid E\psi ,$$$$\psi ::=\phi \mid \mathrm{\neg }\psi \mid (\psi \wedge \psi )\mid X\psi \mid (\psi U\psi ),$$

其中 $p$ 是原子命题，$A\psi$ 可定义为 $\mathrm{\neg }E\mathrm{\neg }\psi$。状态公式在 Kripke 状态上判断，路径公式在从该状态出发的完整路径及其当前位置上判断。

满足关系的关键接口为

$$K,s\models E\psi ⟺\mathrm{\exists }\pi \in Paths(s),K,\pi ,0\models \psi .$$

路径公式中嵌入状态公式时，在当前路径状态求值。两层不能合并成一个未标类型的公式集合，否则 $E$ 的量化对象和 $X$ 的推进对象会混淆。

LTL 与 CTL 的嵌入 ​

LTL公理库线性时序逻辑 LTLLinear temporal logic · LTL · Propositional temporal logic在单条无限状态序列上解释 next、until 及其派生算子，并以全路径量词规定系统满足关系。 公式本身是 CTL* 路径公式。系统满足 LTL 的默认全路径语义，可写成 CTL* 状态公式 $A\psi$。

CTL公理库计算树逻辑 CTLComputation tree logic · CTL · Branching-time temporal logic将路径量词 A/E 与时间算子成对组合，在 Kripke 状态上表达分支未来性质。 要求每个时间算子紧跟路径量词，例如 $EX\phi$、$A[\phi U\psi ]$。这些都是合法 CTL* 公式，但 CTL* 还允许

$$E(GFp),A(FGq),E(Gp\wedge Fq),$$

即在一次路径选择后组合多个时间义务。

公式 $EGFp$ 表示存在一条路径让 $p$ 无限多次出现。它不能改写成 CTL 的 $EG(EFp)$：后者允许在路径上每个状态重新选择一条可能不同的未来去到 $p$，不要求同一条路径反复到达。

直觉

同一路径责任的例子 ​

取三个 total 状态 $s,t,d$，转移为

$$s\to s,s\to t,t\to d,d\to d,$$

且只有状态 $t$ 满足命题 $p$。选择路径 $s^{\omega }$ 时，每个位置的状态 $s$ 都满足 $EFp$，因为仍可另选边 $s\to t$。因此

$$K,s\models EG(EFp).$$

但 $K,s⊭E(GFp)$：一直留在 $s$ 的路径从不见 $p$；一旦选择 $s\to t$，命题只在 $t$ 处出现一次，随后永远停在 $d$。这三个状态直接展示“沿外层路径每一步重新寻找某条成功未来”不等于“同一条已选路径无限多次成功”。

有限深度展开看不见“无限多次”的失败；必须分析循环结构或完整无限路径，才能核对 $GF$ 的责任。

例子与边界

量词对偶与作用域 ​

路径量词满足

$$A\psi \equiv \mathrm{\neg }E\mathrm{\neg }\psi ,$$

时间算子仍有 until/release、eventually/globally 的对偶。否定正常化必须同时穿过路径量词与时间算子，例如

$$\mathrm{\neg }A(Fp)\equiv E(G\mathrm{\neg }p).$$

括号不可省略到改变作用域。$AF(p\vee q)$ 要求每条路径最终到达 $p$ 或 $q$；$AFp\vee AFq$ 则要求系统整体满足其中一个统一目标，通常更强。

多个路径量词嵌套时，内层从当前路径位置的状态重新量化所有未来，而不是继续沿外层已选路径。这个“回到状态再分支”的语义是 CTL* 与纯线性逻辑的核心差别。

推论与应用

表达力与验证代价 ​

CTL* 严格包含 CTL 和 LTL 的状态性质表达，但更强表达力不等于更好的规格。许多工程需求用较小片段已经清楚，复杂量词交替会增加阅读和反例解释难度。

有限 Kripke 结构上的 CTL* 模型检查可判定，但对公式的最坏复杂度显著高于 CTL 的直接状态集合迭代。常见路线把路径子公式转为自动机或使用 alternating automata，公式转换会产生指数级结构。

表达能力也不提供定量时间、概率或数据不变量。若路径需要“5 秒内”或“概率至少 0.99”，必须扩展模型和逻辑，而不是用更多 $A/E$ 嵌套模拟。

CTL* 的反例形状也随量词交替变化。反驳全称路径公式往往一条路径足够，反驳“每个状态存在某条恢复路径”却可能需要展示一个状态及其所有候选未来为何失败。工具若始终只输出线性 trace，可能只能给局部提示而非完整可检查证书；规格作者应预先确认诊断形式能否承载所用量词结构。

参考资料

• 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。
• E. Allen Emerson and Chin-Laung Lei, “Efficient Model Checking in Fragments of the Propositional Mu-Calculus,” LICS, 1986, pp. 267–278。
• Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press, 2008, §§5.8, 6.6。