线性时序逻辑

线性时序逻辑（，LTL），或称线性时态逻辑，是一种模态时态逻辑。其时态运算符限定于描述从一个给定的状态开始的某一条路径上的事件。线性时序逻辑由阿米尔·伯努利在1977年提出。线性时序逻辑和两者可以归入更广义的中。

语法和语义
一个线性时序逻辑公式由以下三种要素构成：

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

等价变换

• 分配律

• 逻辑“非”运算

• 特殊时态属性

特性表达
有两种主要特性可以使用线性时序逻辑来表达：

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

参见

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

参考文献