计算树逻辑

线性时序逻辑LTL是基于路径的，因此是被视为线性的。在LTL中考虑从同一状态开始计算时，很容易碎全部计算同时陈述性质，但难以对部分计算陈述性质。
我们接下来介绍的计算树逻辑将基于时间的分支概念，用无限有向树来描述系统性质。这将允许我们表示开始与一个状态的某些或全部计算的性质，因而允许使用路径存在量词\(\exists\)和全称量词\(\forall\).

计算树逻辑(Computation Tree Logic, CTL)
CTL语法： 原子命题集合AP上的CTL状态公式\[\Phi := true|a|\Phi_1\land\Phi_2|\lnot \Phi|\exists\varphi|\forall\varphi\]其中\(a\in AP, \varphi\)是路径公式：\[\varphi := \bigcirc \Phi|\Phi_1\bigcup\Phi_2,\]\(\Phi\)是状态公式。

状态公式表达状态的性质，而路径公式表达状态的一个无限序列的性质。在路径公式前添加路径量词就可以转化为状态公式。可以类似LTL那样利用true和false派生出\(\Diamond,\Box\).
\(\exists\Diamond\Phi\)表示"可能成立"，\(\forall\Diamond\Phi\)表示"必然成立"，\(\exists\Box\Phi\)表示"可能总是，"\(\forall\Box\Phi\)表示"不变"。\(\forall\Box\forall\Diamond\Phi\)表示在所有路径上无线经常为真。
如果迁移系统TS的每个初始状态\(s_0\)满足状态公式\(\Phi\)，称TS满足\(\Phi\)(\(TS\vDash\Phi\)).

LTL与CTL的表达力对比
定理1. CTL转化为等价LTL公式的准则：令\(\Phi\)是CTL公式，消去其中所有路径量词得到LTL公式\(\varphi\). 则\(\Phi\equiv\varphi\)或不存在LTL公式等价于\(\Phi\).
定理2. 存在这样的LTL公式，使不存在CTL公式与之等价。例：\(\Diamond\Box a\).
也存在这样的CTL公式，使不存在LTL公式与之等价。例：\(\forall\Box\exists\Diamond a\).

CTL模型检验
基本算法：
(1) 递归计算满足公式\(\Phi\)的所有状态的集合\(Sat(\Phi)\).
(2) \(TS\vDash\Phi\)当且仅当\(I\subseteq Sat(\Phi)\).
\(Sat(\Phi)\)的递归计算可以理解为对CTL公式自下而上的遍历，节点表示子式，叶节点为true或原子命题。所有内部节点用一个运算符标记。
叶节点的满足集可以直接由标签函数得到。

    所属分类：Formal Methods     发表于2022-02-14