線性時序邏輯

線性時序邏輯（英語：linear temporal logic，LTL），或稱線性時態邏輯，是一種模態時態邏輯。其時態運算符限定於描述從一個給定的狀態開始的某一條路徑上的事件。^[1][2][3][4]線性時序邏輯由阿米爾·伯努利在1977年提出。^[5]線性時序邏輯和計算樹邏輯（英語：Computation tree logic）兩者可以歸入更廣義的CTL*（英語：CTL*）中。

語法和語義

一個線性時序邏輯公式由以下三種要素構成：^[6][3]

• 原子命題變量
• 邏輯運算符：「非」（¬）、「與」（∧）、「或」（∨）、「條件」（→）、「雙條件」（↔）。
• 時態運算符：X，F，G，U，R等

時態運算符的語義如下表所示，其中 φ 和 ψ 為原子命題變量：

字母表示	符號表示	說明	克里普克路徑示意圖
一元運算:
X φ	${\displaystyle \bigcirc \varphi }$	neXt（下一刻）: φ 在下一時刻為真
F φ	${\displaystyle \Diamond \varphi }$	Finally（最終）: φ 在以後某個時刻（最終）會真
G φ	${\displaystyle \Box \varphi }$	Globally（總是）: 從當前時刻起， φ 總是為真
二元運算:
ψ U φ	${\displaystyle \psi \;{\mathcal {U}}\,\varphi }$	Until（直到）: ψ 總是為真，直到某一時刻φ 為真；該時刻可以為當前時刻或者以後某個時刻
ψ R φ	${\displaystyle \psi \;{\mathcal {R}}\,\varphi }$	Release（釋放）: φ 總是為真，直到某一時刻ψ和φ 同時為真；如果ψ 從未為真，則φ 必須保持永遠為真
ψ W φ	${\displaystyle \psi \;{\mathcal {W}}\,\varphi }$	Weak until（弱直到）: ψ 總是為真，直到某一時刻φ 為真；如果φ 從未為真，則ψ 必須保持永遠為真
ψ M φ	${\displaystyle \psi \;{\mathcal {M}}\,\varphi }$	Strong release（強釋放）: φ 總是為真，直到某一時刻ψ和φ 同時為真；該時刻可以為當前時刻或者以後某個時刻

其中，時態運算符「釋放」R，「最終」F，「總是」G可分別定義為：

• ψ R φ ≡ ¬(¬ψ U ¬φ)
• F ψ ≡ true U ψ
• G ψ ≡ false R ψ ≡ ¬F ¬ψ

此外，時態運算符「弱直到」W和「強釋放」M為對偶關係，可分別定義為：^[7]

• ψ W φ ≡ (ψ U φ) ∨ G ψ ≡ ψ U (φ ∨ G ψ) ≡ φ R (φ ∨ ψ)
• ψ M φ ≡ ¬(¬ψ W ¬φ) ≡ (ψ R φ) ∧ F ψ ≡ ψ R (φ ∧ F ψ) ≡ φ U (ψ ∧ φ)

等價變換

• 分配律^[8][9]

分配律
X (φ ∨ ψ) ≡ (X φ) ∨ (X ψ)	X (φ ∧ ψ)≡ (X φ) ∧ (X ψ)	X (φ U ψ)≡ (X φ) U (X ψ)
F (φ ∨ ψ) ≡ (F φ) ∨ (F ψ)	G (φ ∧ ψ)≡ (G φ) ∧ (G ψ)
ρ U (φ ∨ ψ) ≡ (ρ U φ) ∨ (ρ U ψ)	(φ ∧ ψ) U ρ ≡ (φ U ρ) ∧ (ψ U ρ)

• 邏輯「非」運算

邏輯「非」運算
X 自對偶	F 和 G 對偶	U 和 R 對偶	W 和 M 對偶
¬X φ ≡ X ¬φ	¬F φ ≡ G ¬φ	¬ (φ U ψ) ≡ (¬φ R ¬ψ)	¬ (φ W ψ) ≡ (¬φ M ¬ψ)
	¬G φ ≡ F ¬φ	¬ (φ R ψ) ≡ (¬φ U ¬ψ)	¬ (φ M ψ) ≡ (¬φ W ¬ψ)

• 特殊時態屬性

特殊時態屬性
F φ ≡ F F φ	G φ ≡ G G φ	φ U ψ ≡ φ U (φ U ψ)
φ U ψ ≡ ψ ∨ ( φ ∧ X(φ U ψ) )	φ W ψ ≡ ψ ∨ ( φ ∧ X(φ W ψ) )	φ R ψ ≡ ψ ∧ (φ ∨ X(φ R ψ) )
G φ ≡ φ ∧ X(G φ)	F φ ≡ φ ∨ X(F φ)

特性表達

有兩種主要特性可以使用線性時序邏輯來表達：^[10][11]

• 安全性（safety）：即某種不良性質 φ 永不出現，G¬ϕ
• 活性（liveness）<：即某種良好的性質 ψ 一直保持，GFψ 或 G(ϕ →Fψ)

參見

• 克里普克結構
• 時間邏輯