線性時序邏輯

線性時序邏輯（英語：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ψ)

參見

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

參考文獻

1. Logic in Computer Science: Modelling and Reasoning about Systems: page 175
2. Linear-time Temporal Logic. [2012-03-19]. （原始內容存檔於2017-04-30）.
3. Li Xi. 嵌入式系统的属性与验证 (PDF). 中國科學技術大學: 12. [2022-08-07]. （原始內容存檔 (PDF)於2022-08-04）.
4. 陳志遠; 黃少濱，韓麗麗. 现代模态逻辑在计算机科学中的应用研究. 計算機科學. 2013, 40 (6A) [2022-08-07]. （原始內容存檔於2022-08-04）. 引文使用過時參數coauthors (幫助)
5. Amir Pnueli, The temporal logic of programs. Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS), 1977, 46–57. doi:10.1109/SFCS.1977.32
6. Sec. 5.1 of Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press Archived copy. [2011-05-17]. （原始內容存檔於2010-12-04）.
7. Sec. 5.1.5 "Weak Until, Release, and Positive Normal Form" of Principles of Model Checking.
8. V.S. Alagar; K. Periyasamy. Specification of Software Systems. Springer. 2012: 186. ISBN 1475729219. 引文使用過時參數coauthors (幫助)
9. Fred Kroger; Stephan Merz. Temporal Logic and State Systems. Springer. 2008: 417–418. ISBN 3540674012. 引文使用過時參數coauthors (幫助)
10. Bowen Alpern, Fred B. Schneider, Defining Liveness, Information Processing Letters, Volume 21, Issue 4, 1985, Pages 181-185, ISSN 0020-0190, https://doi.org/10.1016/0020-0190(85)90056-0
11. Bowen Alpern; Fred B. Schneider. Recognizing safety and liveness (PDF). Distributed Computing. 1987 [2022-08-07]. （原始內容存檔 (PDF)於2022-07-21）. 引文使用過時參數coauthors (幫助)