CTL和LTL的区别：
- CLT明确允许对路径使用量词，比LTL有更强的表达能力
- 但CTL不允许像LTL那样，通过用公式描述来选择一个路径范围，在这方面LTL更有表达能力。
- 比如：“对所有这样的路径，沿该路径有p的话，也有q”，用LTL表示为 F p → F q Fp \to Fq Fp→Fq
- 但由于收到所有
F
F
F必须伴随着一个
A
A
A或
E
E
E使用的约束，用CTL写成
F
p
→
F
q
Fp \to Fq
Fp→Fq是不可能的
- 如果CTL写成 A F p → A F q AFp \to AFq AFp→AFq，则表示为“如果沿着所有路径有p，那么沿着所有路径也有q"；
- 如果CTL写成 A G ( p → A F q ) AG(p \to AF q) AG(p→AFq)，则表示为“所有路径延伸到 p p p最终会遇到 q q q”，与 F p → F q Fp \to Fq Fp→Fq的意义还是不相同。
- 说明LTL公式
F
G
p
FGp
FGp和CTL公式
A
F
A
G
p
AFAGp
AFAGp不等价的范例：
下图的模型中， F G p FGp FGp是满足的， A F A G p AFAGp AFAGp是不满足的
LTL公式 X F p XFp XFp、LTL公式 F X p FXp FXp、CTL公式 A X A F p AXAFp AXAFp是等价的，但不与CTL公式 A F A X p AFAXp AFAXp等价
CTL*、CTL、LTL的关系：
- CTL*公式将LTL和CTL的表达能力结合，并去除了CTL对每个时态算子（X，U，F，G）必须与唯一路径量词（A，E）伴随使用的约束而得到的一种逻辑。
- 表达能力之间的关系
- 在CTL中但不在LTL中： ψ 1 = d e f A G E F p \psi_1 \overset{def}{ = } AGEFp ψ1=defAGEFp，表示无论到哪里，我们总可以到达一个使p为真的状态，例如在协议中寻找死锁。
- 在LTL中但不在CTL中： ψ 3 = d e f A [ G F p → F q ] \psi_3 \overset{def}{ = } A[GFp \to Fq] ψ3=defA[GFp→Fq]，表示如果沿该路径有无限多p，则q出现一次。
- 在LTL中和CTL中： ψ 2 = d e f A G [ p → A F q ] \psi_2 \overset{def}{ = } AG[p \to AFq] ψ2=defAG[p→AFq]在CTL中，或者 G ( p → F q ) G(p \to Fq) G(p→Fq)在LTL中，表示任何p最终都跟着一个q
- 在CTL*中，但不在CTL和LTL中： ψ 4 = d e f E [ G F p ] \psi_4 \overset{def}{ = } E[GFp] ψ4=defE[GFp]，表示存在一条有限多p的路径
- 在
CTL*公式
状态公式，用状态来赋值：
ϕ
:
:
=
⊤
∣
p
∣
(
¬
ϕ
)
∣
(
ϕ
∧
ϕ
)
∣
A
[
α
]
∣
E
(
α
)
\phi :: = \top | p | (\neg \phi) | (\phi \wedge \phi) | A[\alpha] |E (\alpha)
ϕ::=⊤∣p∣(¬ϕ)∣(ϕ∧ϕ)∣A[α]∣E(α)
路径公式，沿着路径赋值：
α
:
:
=
ϕ
∣
(
¬
α
)
∣
(
α
∧
α
)
∣
(
α
U
α
)
∣
(
G
α
)
∣
(
F
α
)
∣
(
X
α
)
\alpha :: = \phi | (\neg \alpha) | (\alpha \wedge \alpha ) | (\alpha U \alpha)|(G \alpha) | (F \alpha) | (X \alpha)
α::=ϕ∣(¬α)∣(α∧α)∣(αUα)∣(Gα)∣(Fα)∣(Xα)
范例：
- A [ ( p U r ) ∨ ( q U r ) ] A[(p U r) \vee (q U r)] A[(pUr)∨(qUr)]
- A [ X p ∨ X X p ] A[X p \vee XX p] A[Xp∨XXp]
- E [ G F p ] E [GFp] E[GFp]
LTL中的过去算子
- LTL中的时态算子 X , U , F X,U,F X,U,F等都是参考未来的算子，有时我们可能需要一个参考过去的算子，我们称之为过去算子。
- 过去算子：
- Y表示昨天，与X对立
- S表示自从，与U对立
- O表示i曾经，与F对立
- H表示历史地，与G对立
- 例如：“只要q出现，那么过去已经有某一个p出现过了”可以表示为 G ( q → O p ) G(q \to Op) G(q→Op)
- NuSMVz支持LTL中的过去算子，但不支持CTL中的过去算子（例如AX，ES等）
- 过去算子并不能增加LTL的表达能力，他们只是可以等价地写为不带过去算子地公式