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的表达能力，他们只是可以等价地写为不带过去算子地公式

标签：Fq,路径,笔记,算子,CTL,alpha,数理逻辑,LTL
来源： https://blog.csdn.net/qq_37400312/article/details/113176621