线性时序逻辑

线性时序逻辑（英語：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ψ)

参见

• 克里普克结构
• 时间逻辑