线性时序逻辑

线性时序逻辑（英语：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 (帮助)