跳转到内容

线性时序逻辑

维基百科,自由的百科全书

线性时序逻辑(英語:linear temporal logic,LTL),或称线性时态逻辑,是一种模态时态逻辑。其时态运算符限定于描述从一个给定的状态开始的某一条路径上的事件。[1][2][3][4]线性时序逻辑由阿米尔·伯努利在1977年提出。[5]线性时序逻辑和计算树逻辑英语Computation tree logic两者可以归入更广义的CTL*英语CTL*中。

语法和语义

[编辑]

一个线性时序逻辑公式由以下三种要素构成:[6][3]

时态运算符的语义如下表所示,其中 φψ 为原子命题变量:

字母表示 符号表示 说明 克里普克路径示意图
一元運算:
X φ neXt(下一刻): φ 在下一时刻为真 LTL next operator
F φ Finally(最终): φ 在以后某个时刻(最终)会真 LTL eventually operator
G φ 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对偶关系,可分别定义为:[7]

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

等价变换

[编辑]
分配律
X (φ ∨ ψ) ≡ (X φ) ∨ (X ψ) X (φ ∧ ψ)≡ (X φ) ∧ (X ψ) XU ψ)≡ (X φ) U (X ψ)
F (φ ∨ ψ) ≡ (F φ) ∨ (F ψ) G (φ ∧ ψ)≡ (G φ) ∧ (G ψ)
ρ U (φ ∨ ψ) ≡ (ρ U φ) ∨ (ρ U ψ) (φ ∧ ψ) U ρ ≡ (φ U ρ) ∧ (ψ U ρ)
  • 逻辑“非”运算
逻辑“非”运算
X对偶 FG 对偶 UR 对偶 WM 对偶
¬X φ ≡ X ¬φ ¬F φ ≡ G ¬φ ¬ (φ U ψ) ≡ (¬φ R ¬ψ) ¬ (φ W ψ) ≡ (¬φ M ¬ψ)
¬G φ ≡ F ¬φ ¬ (φ R ψ) ≡ (¬φ U ¬ψ) ¬ (φ M ψ) ≡ (¬φ W ¬ψ)
  • 特殊时态属性
特殊时态属性
F φ ≡ F F φ G φ ≡ G G φ φ U ψ ≡ φ UU ψ)
φ U ψ ≡ ψ ∨ ( φ ∧ XU ψ) ) φ W ψ ≡ ψ ∨ ( φ ∧ XW ψ) ) φ R ψ ≡ ψ ∧ (φ ∨ XR ψ) )
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. ^ 3.0 3.1 Li Xi. 嵌入式系统的属性与验证 (PDF). 中国科学技术大学: 12. [2022-08-07]. (原始内容存档 (PDF)于2022-08-04). 
  4. ^ 陈志远; 黄少滨,韩丽丽. 现代模态逻辑在计算机科学中的应用研究. 计算机科学. 2013, 40 (6A) [2022-08-07]. (原始内容存档于2022-08-04). 
  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. 
  9. ^ Fred Kroger; Stephan Merz. Temporal Logic and State Systems. Springer. 2008: 417–418. ISBN 3540674012. 
  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).