本章目錄
- CTL和LTL的差別：
- CTL*、CTL、LTL的關系：
- CTL*公式
- LTL中的過去算子
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是不滿足的
【面向計算機的數理邏輯/軟體理論基礎筆記】CTL*CTL和LTL的差別：CTL*、CTL、LTL的關系：CTL*公式LTL中的過去算子
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*CTL和LTL的差別：CTL*、CTL、LTL的關系：CTL*公式LTL中的過去算子 - 在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 Y Y表示昨天，與 X X X對立
- S S S表示自從，與 U U U對立
- O O O表示i曾經，與 F F F對立
- H H H表示曆史地，與 G G G對立
- 例如：“隻要q出現，那麼過去已經有某一個p出現過了”可以表示為 G ( q → O p ) G(q \to Op) G(q→Op)
- NuSMVz支援LTL中的過去算子，但不支援CTL中的過去算子（例如AX，ES等）
- 過去算子并不能增加LTL的表達能力，他們隻是可以等價地寫為不帶過去算子地公式