计算树逻辑 CTL | Codeboy's Blog

形式陈述

状态公式语法

作为一种时序逻辑，CTL 公式在Kripke 结构的状态上解释。除原子命题和布尔联结外，时间构造必须由路径量词 $A$ 或 $E$ 与时间算子配对：

EX\varphi, AX\varphi, E[\varphi U\psi],\ A[\varphi U\psi].

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

例如

K,s\models EX\varphi

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

路径量词与时序算子成对

$EF\,p$ 表示存在路径最终到达 $p$ 状态， $AF\,p$ 表示每条路径最终都到达 $p$ 。 $EG\,p$ 表示存在一条无限路径始终保持 $p$ ， $AG\,p$ 表示所有可达未来状态都保持 $p$ 。

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

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

直觉

恢复服务的分支例子

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

EF\,healthy,

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

AF\,healthy,

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

若每个可达状态都至少保留一条通向 healthy 的路径，则 $AG(EF\,healthy)$ 成立。它仍不保证实际执行必然修复；要得到该结论，模型本身必须满足 $AF\,healthy$ 。在上面的 failed 自环路径中，修复动作进入 sink 后已不再使能，所以普通弱公平或强公平都不会排除这条路径；公平性不能笼统地当作 liveness 修补器。

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

例子与边界

以状态集合求值

对每个子公式 $\varphi$ ，模型检查算法计算满足状态集合 $\operatorname{Sat}(\varphi)$ 。取四状态结构

R=\{s_0\to s_1,s_0\to s_2,s_1\to s_3, s_2\to s_2,s_3\to s_3\},

且只有 $s_3$ 标记 $p$ 。对方程 $Z=\{s_3\}\cup Pre(Z)$ 从空集开始迭代：

Z_0=\varnothing,\quad Z_1=\{s_3\},\quad Z_2=\{s_3,s_1\},\quad Z_3=\{s_3,s_1,s_0\},\quad Z_4=Z_3.

因此 $\operatorname{Sat}(EFp)=\{s_0,s_1,s_3\}$ ；自环状态 $s_2$ 永远到不了 $p$ 。同一图上 $s_0\not\models AFp$ ，因为路径 $s_0s_2s_2\cdots$ 是反例。

一般地，

\operatorname{Sat}(EX\varphi)= \operatorname{Pre}(\operatorname{Sat}(\varphi)),

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

Z=\operatorname{Sat}(\psi)\cup (\operatorname{Sat}(\varphi)\cap\operatorname{Pre}(Z))

的最小不动点。 $EG\varphi$ 是

Z=\operatorname{Sat}(\varphi)\cap\operatorname{Pre}(Z)

的最大不动点。有限状态空间中， $EU$ 从空集增长、 $EG$ 从全状态集合收缩，至集合不再变化。单调性保证迭代选择相应最小/最大解；互换初值会得到错误的不动点。

推论与应用

表达边界

系统级 LTL 性质 $A(GF\,p)$ 不是区分 LTL 与 CTL 的例子；在 total Kripke 结构上，它等价于 CTL 公式 $AG(AF\,p)$ 。前者要求每条路径从任意位置往后都还能遇到 $p$ ，后者要求每个可达状态的所有延续最终遇到 $p$ ；给任一可达前缀接上任一延续，便可互相得到这两个量词条件。

真正的 LTL-not-CTL 例子是 $A(FG\,p)$ ：每条路径可以有各自的稳定位置，此后只沿该路径永久满足 $p$ 。看似接近的 CTL 公式 $AF(AG\,p)$ 更强，因为内层 $A$ 会在到达状态处重新量化所有分支。举例说，带 $p$ 的状态 $s$ 有自环，也可转到一次不满足 $p$ 的状态 $t$ ，随后进入永久满足 $p$ 的 sink；每条路径至多经过一次 $t$ ，所以 $A(FG\,p)$ 成立，但路径 $s^\omega$ 永远没有到达 $AG\,p$ 状态，因为在 $s$ 仍可另选通向 $t$ 的分支。CTL 一般没有与 $A(FG\,p)$ 等价的公式。

反过来，CTL 的 $AG(EF\,p)$ 允许在每个可达状态重新选择一条可能不同的未来去寻找 $p$ ，依赖 LTL 单条 trace 不保留的分支结构，因此一般没有等价 LTL 公式。一个方向保留同一路径上的稳定后缀，另一个方向在状态处重新分支，说明 CTL 与 LTL 一般不可互相包含。

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

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

全称算子可用存在算子和否定对偶化，例如 $AX\varphi\equiv\neg EX\neg\varphi$ 、 $AG\varphi\equiv\neg EF\neg\varphi$ 。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。

形式陈述 ​

状态公式语法 ​

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

恢复服务的分支例子 ​

以状态集合求值 ​