時序邏輯之線性時序邏輯（LTL）和分支時序邏輯（CTL）對比及典型示例

在模型檢測工具NuSMV中，時序邏輯是用來描述系統性質（或形式規約）的形式化語言，包括兩類，一類是線性時序邏輯（Linear-time Temporal Logic, LTL）,另一類是分支時序邏輯（也稱計算樹邏輯，Computing Tree Logic, CTL），二者主要的差別在于采取不同的方式對Kripke結構所對應的計算樹分支進行展開。

線性時序邏輯

定義

時态運算符限定于描述從一個給定的狀态開始的某條路徑上的事件。

特點

• 将時間模組化成狀态序列，無限延伸到未來，該狀态序列稱為計算路徑（簡稱“路徑”），隐含了整個系統是按着一個路徑向前發展演化的，隐含使用全稱量詞，不适用存在量詞（與CTL不同）
• 使用訓示未來的連接配接詞（時間操作符），隻表達一條路徑上的不确定性，而CTL表達多個路徑

構成

• 項（terms）：p表示原子命題
• 經典布爾操作
  • ¬(not), v(or), ∧(and)
  • →(imply, if-then): p->q, 如果p發生則會出現q
• 基本時态操作（Basic temporal operators）
  • ☐(G, always), ◇(F, eventually), ○(X, next), U(strong unit)
  • Gp - p holds globally in the future.
  • Fp - p holds sometime（不确定性！）in the future.
  • Xp - p holds next time.
  • pUq - p holds until q holds.

語義

<>p ：p在以後某個時刻會真

[]p ：從目前時刻起，p總是為真

Xp ：p在下一個時刻為真

示例

以紅綠燈為例（gr:green ye:yellow re:red）

性質1：信号燈按照“紅、黃、綠、紅、黃、綠…”的順序變化

對應的LTL：[] ( (grUye) v (yeUre) v (reUgr) )

性質2：信号燈不能在同一時間出現兩種以上的顔色

對應的LTL： [] ( ¬(gr∧ye) ∧ ¬(ye∧re) ∧ ¬(re∧gr) ∧ (gr v ye v re) )

分支時序邏輯

定義

時态運算符限定于從一個給定的狀态開始的所有可能路徑上。

構成

CTL由路徑量詞和時态算子構成。

路徑量詞：

• A（“for all computation paths”，全稱量詞，将來全部路徑）
• E（“exist some computation path” ，存在量詞，存在一條将來路徑）

時态算子：

• X（next：下一個狀态）
• F（future：某個未來的狀态）
• G（globally：所有的未來狀态）

• U（until：路徑上存在某個狀态滿足性質q，而且它之前的每

  個狀态都滿足性質p）

• R（release：路徑上從第一個狀态開始，都要滿足性質q，直

  到某個狀态滿足性質p）

常見表達：

• AX p：在所有未來路徑上，公式在下一個狀态為真
• AF p：在所有未來路徑上，公式在某個狀态必然為真

  

• AG p：在所有未來路徑上，公式都永遠為真

  

• A (p U q)：在所有未來路徑都存在：公式p一直為真，直到公式q為真
• EX p：存在一條未來路徑，下一狀态公式為真
• EF p：存在一條未來路徑，公式在某個狀态一定為真

  

• EG p：存在一條未來路徑，公式永為真

  

• E (p U q)：存在一條未來路徑，公式p一直為真，直到公式q為真

示例

以程序通路共享資料為例，假設有兩個程序proc1和proc2，當進入“critical”狀态表示正在通路共享資料，“entering”狀态表示程序請求通路共享資料，當任務排程允許通路後進入“critical”狀态通路共享資料。

性質1：不存在程序1和程序2同時進入“critical”狀态

對應的CTL：AG ! (proc1.state = critical & proc2.state = critical)

性質2：如果程序1處于“entering”狀态（即請求進入“critical”狀态），那麼最終程序1都會進入“critical”狀态

對應的CTL：AG (proc1.state = entering -> AF proc1.state = critical)

參考資料

1. 嵌入式系統的屬性與驗證
2. NuSMV 2.6 Tutorial