fbpx
维基百科

线性时序逻辑

四月 08, 2024

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

语法和语义 编辑

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

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

字母表示 符号表示 说明 克里普克路径示意图
一元運算:
X φ   neXt（下一刻）: φ 在下一时刻为真  
F φ   Finally（最终）: φ 在以后某个时刻（最终）会真  
G φ   Globally（总是）: 从当前时刻起， φ 总是为真  
二元运算:
ψ U φ   Until（直到）: ψ 总是为真，直到某一时刻φ 为真；该时刻可以为当前时刻或者以后某个时刻  
ψ R φ   Release（释放）: φ 总是为真，直到某一时刻ψ和φ 同时为真；如果ψ 从未为真，则φ 必须保持永远为真  

 

ψ W φ   Weak until（弱直到）: ψ 总是为真，直到某一时刻φ 为真；如果φ 从未为真，则ψ 必须保持永远为真  

 

ψ M φ   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 (ψ ∧ φ)

等价变换 编辑

分配律
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. ^ . [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 . [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）. 

四月 08, 2024
线性时序逻辑, 英語, linear, temporal, logic, 或称线性时态逻辑, 是一种模态时态逻辑, 其时态运算符限定于描述从一个给定的状态开始的某一条路径上的事件, 由阿米尔, 伯努利在1977年提出, 和计算树逻辑, 英语, computation, tree, logic, 两者可以归入更广义的ctl, 英语, 目录, 语法和语义, 等价变换, 特性表达, 参见, 参考文献语法和语义, 编辑一个公式由以下三种要素构成, 原子命题变量, 逻辑运算符, 条件, 双条件, 时态运算符, r等时态运算符. 线性时序逻辑 英語 linear temporal logic LTL 或称线性时态逻辑 是一种模态时态逻辑 其时态运算符限定于描述从一个给定的状态开始的某一条路径上的事件 1 2 3 4 线性时序逻辑由阿米尔 伯努利在1977年提出 5 线性时序逻辑和计算树逻辑 英语 Computation tree logic 两者可以归入更广义的CTL 英语 CTL 中 目录 1 语法和语义 2 等价变换 3 特性表达 4 参见 5 参考文献语法和语义 编辑一个线性时序逻辑公式由以下三种要素构成 6 3 原子命题变量 逻辑运算符 非 与 或 条件 双条件 时态运算符 X F G U R等时态运算符的语义如下表所示 其中 f 和 ps 为原子命题变量 字母表示 符号表示 说明 克里普克路径示意图一元運算 X f f displaystyle bigcirc varphi nbsp neXt 下一刻 f 在下一时刻为真 nbsp F f f displaystyle Diamond varphi nbsp Finally 最终 f 在以后某个时刻 最终 会真 nbsp G f f displaystyle Box varphi nbsp Globally 总是 从当前时刻起 f 总是为真 nbsp 二元运算 ps U f psUf displaystyle psi mathcal U varphi nbsp Until 直到 ps 总是为真 直到某一时刻f 为真 该时刻可以为当前时刻或者以后某个时刻 nbsp ps R f psRf displaystyle psi mathcal R varphi nbsp Release 释放 f 总是为真 直到某一时刻ps和f 同时为真 如果ps 从未为真 则f 必须保持永远为真 nbsp nbsp ps W f psWf displaystyle psi mathcal W varphi nbsp Weak until 弱直到 ps 总是为真 直到某一时刻f 为真 如果f 从未为真 则ps 必须保持永远为真 nbsp nbsp ps M f psMf displaystyle psi mathcal M varphi nbsp Strong release 强释放 f 总是为真 直到某一时刻ps和f 同时为真 该时刻可以为当前时刻或者以后某个时刻 nbsp 其中 时态运算符 释放 R 最终 F 总是 G可分别定义为 ps R f ps U f F ps true U ps G ps false R ps F ps此外 时态运算符 弱直到 W和 强释放 M为对偶关系 可分别定义为 7 ps W f ps U f G ps ps U f G ps f R f ps ps M f ps W f ps R f F ps ps R f F ps f U ps f 等价变换 编辑分配律 8 9 分配律X f ps X f X ps X f ps X f X ps X f U ps X f U X ps F f ps F f F ps G f ps G f G ps r U f ps r U f r U ps f ps U r f U r ps U r 逻辑 非 运算逻辑 非 运算X 自对偶 F 和 G 对偶 U 和 R 对偶 W 和 M 对偶 X f X f F f G f f U ps f R ps f W ps f M ps G f F f f R ps f U ps f M ps f W ps 特殊时态属性特殊时态属性F f F F f G f G G f f U ps f U f U ps f U ps ps f X f U ps f W ps ps f X f W ps f R ps ps f X f R ps G f f X G f F f f X F f 特性表达 编辑有两种主要特性可以使用线性时序逻辑来表达 10 11 安全性 safety 即某种不良性质 f 永不出现 G ϕ 活性 liveness lt 即某种良好的性质 ps 一直保持 GFps 或 G ϕ Fps 参见 编辑克里普克结构 时间逻辑参考文献 编辑 Logic in Computer Science Modelling and Reasoning about Systems page 175 Linear time Temporal Logic 2012 03 19 原始内容存档于2017 04 30 3 0 3 1 Li Xi 嵌入式系统的属性与验证 PDF 中国科学技术大学 12 2022 08 07 原始内容存档 PDF 于2022 08 04 陈志远 黄少滨 韩丽丽 现代模态逻辑在计算机科学中的应用研究 计算机科学 2013 40 6A 2022 08 07 原始内容存档于2022 08 04 引文使用过时参数coauthors 帮助 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 Sec 5 1 of Christel Baier and Joost Pieter Katoen Principles of Model Checking MIT Press Archived copy 2011 05 17 原始内容存档于2010 12 04 Sec 5 1 5 Weak Until Release and Positive Normal Form of Principles of Model Checking V S Alagar K Periyasamy Specification of Software Systems Springer 2012 186 ISBN 1475729219 引文使用过时参数coauthors 帮助 Fred Kroger Stephan Merz Temporal Logic and State Systems Springer 2008 417 418 ISBN 3540674012 引文使用过时参数coauthors 帮助 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 Bowen Alpern Fred B Schneider Recognizing safety and liveness PDF Distributed Computing 1987 2022 08 07 原始内容存档 PDF 于2022 07 21 引文使用过时参数coauthors 帮助 取自 https zh wikipedia org w index php title 线性时序逻辑 amp oldid 74934477, 维基百科，wiki，书籍，书籍，图书馆，

文章

，阅读，下载，免费，免费下载，mp3，视频，mp4，3gp， jpg，jpeg，gif，png，图片，音乐，歌曲，电影，书籍，游戏，游戏。