介绍

在前面我们已经介绍了线性属性，为了方便地去描述这个线性属性，我们又介绍了线性时序逻辑，本节要介绍一种新的逻辑计算树逻辑（CTL），那么问题来了，既然我们已经有了一种逻辑，为啥还要介绍一种新的？因为这种逻辑可以描述LTL不能描述的部分。

如果用文氏图来表示的话就是：

CTL能够表达某些LTL不能表达的，LTL也能表达某些CLT不能表达的，但是它们也存在能够共同表达的部分，有没有逻辑能够包括LTL和CTL呢？有，那就是CTL*，它不仅包含了LTL和CTL可以表达的，也可以表达LTL和CTL不能表达的，当然它也需要更多的计算，表意能力比CTL*还强的称为 model μ − c a l c u l u s \text{model }\mu-calculus model μ−calculus，这玩意儿不在这里讨论。

让我们先来回想一下LTL之所以称为线性的，是因为时间的定性概念是基于路径的，并且被视为线性的：在每个时刻只有唯一的一个可能的后继状态，因此每个时刻都有一个唯一的可能的未来。从技术上讲，这是基于以下事实：LTL公式的解释是根据路径（即状态序列）定义的。

但是路径本身可能存在着分支，例如在一个TS系统中，一个状态也许有着多个后继状态，从这个角度来看这种解释是基于状态分支的。我们想到，某些时候在一个状态的所有可能计算都满足某个条件，或者有些时候一个状态的部分可能计算满足某个条件，为了表述这些个性质，我们加入 ∀ \forall ∀和 ∃ \exist ∃符号。

LTL描述的从某个状态开始所有的路径情况，例如 s ⊨ □ ( x ≤ 20 ) s\vDash\Box(x\le 20) s⊨□(x≤20)，它表示对于从s开始的所有路径都满足 x ≤ 20 x\le 20 x≤20

而CTL描述的是从某个状态开始的所有或部分路径情况
例如 s ⊨ ∀ □ ( x ≤ 20 ) s\vDash\forall\Box(x\le 20) s⊨∀□(x≤20),它表示对于从s开始的所有路径都满足 x ≤ 20 x\le 20 x≤20
而 s ⊨ ∃ □ ( x ≤ 20 ) s\vDash\exist\Box(x\le 20) s⊨∃□(x≤20)表示对于从s开始的某些路径满足 x ≤ 20 x\le 20 x≤20

计算树

一个TS的计算树，就是将TS从初始状态出发，可能的路径展开成为一棵树

例如，现在我们有一个TS系统

将它从s0出发可能的路径展开，这样就成为了一棵计算树

线性时间和分支时间的对比

方面	linear time	branching time
行为behavior	path-based:trace(s)	state-based:computation tree of s
时间逻辑temporal logic	LTL path formulas	CTL state formulas
模型检测	PSPACE-complete O( s i z e ( T S ) ⋅ 2 ∣ ϕ ∣ size(TS)·2^{\mid\phi\mid} size(TS)⋅2∣ϕ∣)	PTIME O( s i z e ( T S ) ⋅ ∣ ϕ ∣ size(TS)·\mid\phi\mid size(TS)⋅∣ϕ∣)
公平性	可以直接表示	需要额外的技术

CTL的语法

CTL在状态上的公式
Φ ::= true | a | Φ 1 ∧ Φ 2 | ¬ Φ | ∀ φ | ∃ φ \Phi\text{::= true | a | }\Phi_{1}\wedge\Phi_{2}\text{ | }\lnot\Phi\text{ | }\forall φ\text{ | } \existφ Φ::= true | a | Φ1∧Φ2 | ¬Φ | ∀φ | ∃φ

前面的true，a这种都和LTL差不多，主要到状态上的公式有一个φ，这个就是下面的路径上的公式，它代表了从树的根结点开始的路径

CTL在路径上的公式
φ::= | ◯ Φ | Φ 1 U Φ 2 \text{φ::= }\text{ | }\bigcirc\Phi\text{ | } \Phi_{1} U \Phi_{2} φ::= | ◯Φ | Φ1UΦ2

同样，这里的 Φ \Phi Φ表示的是状态上的公式， ◯ Φ \bigcirc\Phi ◯Φ就表示从根结点出发的下一个状态。

根据这两个定义，我们可以注意到符号 ◯ \bigcirc ◯和 U U U的前面一定会带有 ∀ \forall ∀或者 ∃ \exist ∃

CTL公式的一些例子

两进程互斥问题中的安全性： ∀ □ ( ¬ c r i t 1 ∨ c r i t 2 ) \forall\Box(\lnot crit_{1}\vee crit_{2}) ∀□(¬crit1∨crit2)
每个请求最终都会被应答： ∀ □ ( r e q u e s t → ∀ ◊ r e s p o n s e ) \forall\Box(request\rightarrow\forall\Diamond response) ∀□(request→∀◊response)
红绿灯，黄灯后面一定是红灯亮： ∀ □ ( y e l l o w → ∀ ◯ r e d ) \forall\Box(yellow\rightarrow\forall\bigcirc red) ∀□(yellow→∀◯red)
重置可能性： ∀ □ ∃ ◊ s t a r t \forall\Box\exist\Diamond start ∀□∃◊start
无条件公平性： ∀ □ ∀ ◊ c r i t 1 ∧ ∀ □ ∀ ◊ c r i t 2 \forall\Box\forall\Diamond crit_{1}\wedge\forall\Box\forall\Diamond crit_{2} ∀□∀◊crit1∧∀□∀◊crit2

CTL的语义

CTL状态公式的语义

s ⊨ t r u e s\vDash true s⊨true
s ⊨ a s\vDash a s⊨a当且仅当 a ∈ L ( s ) a∈L_(s) a∈L(s)
s ⊨ φ 1 ∧ φ 2 s\vDash φ_{1}\wedge φ_{2} s⊨φ1∧φ2当且仅当 s ⊨ φ 1 s\vDash φ_{1} s⊨φ1 and s ⊨ φ 2 s\vDash φ_{2} s⊨φ2
s ⊨ ¬ φ s\vDash \lnotφ s⊨¬φ 当且仅当 s ⊭ φ s\nvDash φ s⊭φ
s ⊨ ∃ φ s\vDash \existφ s⊨∃φ 当且仅当 π ⊨ ϕ \pi\vDash\phi π⊨ϕ对于某些从s开始的路径成立
s ⊨ ∀ φ s\vDash \forallφ s⊨∀φ 当且仅当 π ⊨ ϕ \pi\vDash\phi π⊨ϕ对于所有从s开始的路径成立

CTL路径公式的语义

π ⊨ ◯ ϕ 当且仅当 π [ 1 ] = ϕ \pi\vDash\bigcirc\phi当且仅当\pi[1]=\phi π⊨◯ϕ当且仅当π[1]=ϕ
π ⊨ ϕ 1 U ϕ 2 当且仅当存在 j ≥ 0 使得 s j ⊨ ϕ 2 且对于 0 ≤ k < j , π [ k ] ⊨ ϕ 1 \pi\vDash\phi_{1} U\phi_{2}当且仅当存在j\ge0使得s_{j}\vDash\phi_{2}且对于0\le k\lt j,\pi[k]\vDash\phi_{1} π⊨ϕ1Uϕ2当且仅当存在j≥0使得sj⊨ϕ2且对于0≤k<j,π[k]⊨ϕ1

CTL在TS上的语义

对于一个CTL公式 ϕ \phi ϕ，它的可满足集合(satisfaction set) S a t ( ϕ ) Sat(\phi) Sat(ϕ)定义为:
S a t ( ϕ ) = { s ∈ S ∣ s ⊨ ϕ } Sat(\phi)=\{s\in S | s\vDash \phi\} Sat(ϕ)={s∈S∣s⊨ϕ}

说白了就是一些满足CTL公式 ϕ \phi ϕ的状态的集合

如果我们说一个TS满足CTL公式 ϕ \phi ϕ,那么当且仅当公式 ϕ \phi ϕ在所有的初始状态上成立，用公式表示为：
T S ⊨ ϕ 当且仅当 S 0 ⊆ S a t ( ϕ ) 当且仅当 ∀ s 0 ∈ S 0 . s 0 ⊨ ϕ TS\vDash\phi\text{ 当且仅当 }S_{0}\subseteq Sat(\phi) \text{ 当且仅当 }\forall s_{0}\in S_{0}.s_{0}\vDash\phi TS⊨ϕ 当且仅当 S0⊆Sat(ϕ) 当且仅当 ∀s0∈S0.s0⊨ϕ

上面的 S 0 S_{0} S0就是初始状态的集合

来看点实际的例子

从左往右看

存在某些路径，使得这些路径最终出现red
存在某些路径满足整条路径都red总是成立
存在某些路径，使得 y e l l o w U r e d yellowUred yellowUred成立
对于所有的路径来说，最终都会出现red
对于所有的路径来说，red总是成立
对于所有的路径来说，都满足 y e l l o w U r e d yellowUred yellowUred

CTL等价的定义

如果CTL公式 ϕ \phi ϕ和 ψ \psi ψ是等价的（表示为 ϕ ≡ ψ \phi\equiv\psi ϕ≡ψ），那么当且仅当在TS上 S a t ( ϕ ) ≡ S a t ( ψ ) Sat(\phi)\equiv Sat(\psi) Sat(ϕ)≡Sat(ψ)

用公式可以表示为：
ϕ ≡ ψ 当且仅当 T S ⊨ ϕ ⇔ T S ⊨ ψ 当且仅当 S a t ( ϕ ) = S a t ( ψ ) \phi\equiv\psi \\ 当且仅当 TS\vDash\phi \Leftrightarrow TS\vDash\psi \\ 当且仅当 Sat(\phi)=Sat(\psi) ϕ≡ψ当且仅当TS⊨ϕ⇔TS⊨ψ当且仅当Sat(ϕ)=Sat(ψ)

我们可以看到CTL和LTL等价的概念是完全不一样的，LTL的等价是指两个公式表示的无限字的集合相同，而CTL的等价指的是两个公式的可满足集相同

例如我们有

¬ ¬ ϕ ≡ ϕ \lnot\lnot\phi\equiv\phi ¬¬ϕ≡ϕ
¬ ( ϕ ∧ ψ ) ≡ ¬ ϕ ∨ ¬ ψ \lnot(\phi\wedge\psi)\equiv\lnot\phi\vee\lnot\psi ¬(ϕ∧ψ)≡¬ϕ∨¬ψ
¬ ∀ ◯ ϕ ≡ ∃ ◯ ¬ ϕ \lnot\forall\bigcirc\phi\equiv\exist\bigcirc\lnot\phi ¬∀◯ϕ≡∃◯¬ϕ

CTL公式的性质

分配律
∀ □ ( ϕ ∧ ψ ) ≡ ∀ □ ϕ ∧ ∀ □ ψ ∃ ◊ ( ϕ ∨ ψ ) ≡ ∃ ◊ ϕ ∨ ∃ ◊ ψ \forall\Box(\phi\wedge\psi)\equiv\forall\Box\phi\wedge\forall\Box\psi \\ \exist\Diamond(\phi \vee\psi)\equiv \exist\Diamond\phi\vee\exist\Diamond\psi ∀□(ϕ∧ψ)≡∀□ϕ∧∀□ψ∃◊(ϕ∨ψ)≡∃◊ϕ∨∃◊ψ

扩展律
∀ ( ϕ U ψ ) ≡ ψ ∨ ( ϕ ∧ ∀ ◯ ∀ ( ϕ U ψ ) ) ∀ ◊ ϕ ≡ ϕ ∨ ∀ ◯ ∀ ◊ ϕ ∀ □ ϕ ≡ ϕ ∧ ∀ ◯ ∀ □ ϕ ∃ ( ϕ U ψ ) ≡ ψ ∨ ( ϕ ∧ ∃ ◯ ∃ ( ϕ U ψ ) ) ∃ ◊ ϕ ≡ ϕ ∨ ∃ ◯ ∃ ◊ ϕ ∃ □ ϕ ≡ ϕ ∧ ∃ ◯ ∃ □ ϕ \forall(\phi U\psi)\equiv\psi\vee(\phi\wedge\forall\bigcirc\forall(\phi U\psi)) \\ \forall\Diamond\phi\equiv\phi\vee\forall\bigcirc\forall\Diamond\phi \\ \forall\Box\phi\equiv\phi\wedge\forall\bigcirc\forall\Box\phi \\ \exist(\phi U\psi)\equiv\psi\vee(\phi\wedge\exist\bigcirc\exist(\phi U\psi)) \\ \exist\Diamond\phi\equiv\phi\vee\exist\bigcirc\exist\Diamond\phi \\ \exist\Box\phi\equiv\phi\wedge\exist\bigcirc\exist\Box\phi ∀(ϕUψ)≡ψ∨(ϕ∧∀◯∀(ϕUψ))∀◊ϕ≡ϕ∨∀◯∀◊ϕ∀□ϕ≡ϕ∧∀◯∀□ϕ∃(ϕUψ)≡ψ∨(ϕ∧∃◯∃(ϕUψ))∃◊ϕ≡ϕ∨∃◯∃◊ϕ∃□ϕ≡ϕ∧∃◯∃□ϕ

写给学生看的系统分析与验证笔记（十五）——计算树逻辑(Computation tree logic,CTL)相关推荐

写给学生看的系统分析与验证笔记（七）——线性时间属性（Linear-Time Properties）
目录路径和状态图(Paths and State Graph) 状态图路径迹(trace) 刻画线性时间属性(LT Properties) 刻画基于信号量互斥系统的属性刻画无饥饿(starva ...
写给学生看的系统分析与验证笔记（九）——验证正则安全性(verifying regular safety properties)
目录正则安全性验证正则安全性总结之前我们将系统建模为了抽象的模型,并且刻画了相应的性质,现在终于到了模型检测最后一步--验证(verification) 如果我们将真实的系统建模为了TS,并且 ...
《The Non-Designer's Design Book(写给大家看的设计书)》--笔记整理
The Non-Designer's Design Book(写给大家看的设计书)-笔记整理这是一本实用性书籍,阐述了设计中的四大原则:亲密性.对齐.重复和对比,并介绍了如何运用颜色.字体,以及针对 ...
颠覆绿之韵传销谣言！看草根企业逆袭激荡十五载
颠覆绿之韵传销谣言!看草根企业逆袭传奇激荡十五载,17年底,人民日报海外版曾整版刊文评绿之韵助推中国大健康产业发展,文中浓墨重彩地提到了绿之韵创立十五年来坚持履行企业责任与担当.毋庸置疑的是,因为绿之 ...
【系统分析与验证笔记】Transition System模型知识点
本章目录项目到模型的转换原因本章基本词汇解释基本动作的转移公式:S→αS′S\overset{\alpha }{\rightarrow}S'S→αS′ 标签函数(Label function): ...
【系统分析与验证笔记】线性时间（Linear-Time，简称LT）
线性时间行为(Linear-Time Behavior) 路径和状态图 TSTSTS的状态图记作G(TS)G(TS)G(TS),是顶点V=SV = SV=S和边E={(s,s′∈S×S∣s′∈Post ...
写给大家看的设计书阅读笔记1——设计的四大基本原则
设计的四大基本原则概述有一些基本的设计原则,每一个优秀的设计中都应用了这些原则.我们在观察评价一个设计作品时,也要从这几条基本原则去考虑. 亲密性 Proximity 彼此相关的项应当靠近,归组在一 ...
代码要写成别人看不懂的样子（二十六）
本篇文章参考书籍<JavaScript设计模式>–张容铭文章目录前言 MVC 模式实现传说数据模型层视图层控制器层测试完去干饭总个小结附录前言嗨!各位乡绅,上一节 ...
【神经网络】学习笔记十五——训练集，验证集和测试集
以前一直知道神经网络划分数据集时要分为训练集,测试集和验证集,但不知道并且一般以6:2:2的比例划分,到头来不知道这三者各是啥,以及他们的作用是什么.本片文档解释一下三者的作用. 重点在于验证集和测试 ...

写给学生看的系统分析与验证笔记（十五）——计算树逻辑(Computation tree logic,CTL)

目录

介绍

计算树