线性时序逻辑

线性时序逻辑（，LTL），或称线性时态逻辑，是一种模态时态逻辑。其时态运算符限定于描述从一个给定的状态开始的某一条路径上的事件。Logic in Computer Science: Modelling and Reasoning about Systems: page 175线性时序逻辑由阿米尔·伯努利在1977年提出。Amir Pnueli, The temporal logic of programs. Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS), 1977, 46–57. 线性时序逻辑和两者可以归入更广义的中。

语法和语义
一个线性时序逻辑公式由以下三种要素构成：Sec. 5.1 of Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press 
 原子命题变量
 逻辑运算符：“非”（¬）、“与”（∧）、“或”（∨）、“条件”（→）、“双条件”（↔）。
 时态运算符：X，F，G，U，R等

时态运算符的语义如下表所示，其中 φ 和 ψ 为原子命题变量：
字母表示符号表示说明克里普克路径示意图 一元運算:X φneXt（下一刻）: φ 在下一时刻为真LTL next operatorF φFinally（最终）: φ 在以后某个时刻（最终）会真LTL eventually operatorG φGlobally（总是）: 从当前时刻起， φ  总是为真LTL always operator 二元运算:ψ U φUntil（直到）: ψ 总是为真，直到某一时刻φ 为真；该时刻可以为当前时刻或者以后某个时刻LTL until operator        ψ R φRelease（释放）: φ 总是为真，直到某一时刻ψ和φ 同时为真；如果ψ 从未为真，则φ 必须保持永远为真LTL release operator (which stops)
LTL release operator (which does not stop)ψ W φWeak until（弱直到）:  ψ 总是为真，直到某一时刻φ 为真；如果φ 从未为真，则ψ 必须保持永远为真LTL weak until operator (which stops) 
LTL weak until operator (which does not stop)ψ M φStrong release（强释放）: φ 总是为真，直到某一时刻ψ和φ 同时为真；该时刻可以为当前时刻或者以后某个时刻LTL strong release operator 

其中，时态运算符“释放”R，“最终”F，“总是”G可分别定义为：
  R  ≡ ¬(¬ U ¬) 
F  ≡  true U   
G  ≡  false R  ≡ ¬F ¬ 
此外，时态运算符“弱直到”W和“强释放”M为对偶关系，可分别定义为：Sec. 5.1.5 "Weak Until, Release, and Positive Normal Form" of Principles of Model Checking. 
 ψ W φ ≡ (ψ U φ) ∨ G ψ ≡ ψ U (φ ∨ G ψ) ≡  φ R (φ ∨ ψ)
 ψ M φ ≡ ¬(¬ψ W ¬φ) ≡ (ψ R φ) ∧ F ψ ≡ ψ R (φ ∧ F ψ) ≡ φ U (ψ ∧ φ)

等价变换
 分配律
 分配律 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 φ)  

特性表达
有两种主要特性可以使用线性时序逻辑来表达：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
 安全性（safety）：即某种不良性质 φ 永不出现，G¬&varphi;
 活性（liveness）<：即某种良好的性质 ψ 一直保持，GFψ 或 G(&varphi; →Fψ)

参见
 克里普克结构
 时间逻辑

参考文献

Category:時間邏輯
Category:模型檢查