查看“︁线性时序逻辑”︁的源代码

'''线性时序逻辑'''（{{lang-en|linear temporal logic}}，LTL），或称'''线性时态逻辑'''，是一种[[模态逻辑|模态]][[时态逻辑]]。其时态运算符限定于描述从一个给定的状态开始的某一条路径上的事件。<ref>[https://books.google.com/books?id=eUggAwAAQBAJ&printsec=frontcover#v=onepage&q=%22temporal%20logic%22&f=false Logic in Computer Science: Modelling and Reasoning about Systems]: page 175</ref><ref>{{Cite web |url=https://www-step.stanford.edu/tutorial/temporal-logic/temporal-logic.html |title=Linear-time Temporal Logic |access-date=2012-03-19 |archive-url=https://web.archive.org/web/20170430084134/http://www-step.stanford.edu/tutorial/temporal-logic/temporal-logic.html |archive-date=2017-04-30 |url-status=dead }}</ref><ref name=CNslides>{{cite web |author1=Li Xi |title=嵌入式系统的属性与验证 |url=https://staff.ustc.edu.cn/~llxx/embedded/slides/llxx8.pdf |website=中国科学技术大学 |page=12 |access-date=2022-08-07 |archive-date=2022-08-04 |archive-url=https://web.archive.org/web/20220804164956/http://staff.ustc.edu.cn/~llxx/embedded/slides/llxx8.pdf |dead-url=no }}</ref><ref>{{cite journal |author1=陈志远 |coauthors=黄少滨，韩丽丽 |title=现代模态逻辑在计算机科学中的应用研究 |journal=计算机科学 |date=2013 |volume=40 |issue=6A |url=https://jsjkx.com/CN/article/openArticlePDF.jsp?id=5427 |access-date=2022-08-07 |archive-date=2022-08-04 |archive-url=https://web.archive.org/web/20220804164957/https://www.jsjkx.com/CN/article/openArticlePDF.jsp?id=5427 |dead-url=no }}</ref>线性时序逻辑由[[阿米尔·伯努利]]在1977年提出。<ref>[[阿米尔·伯努利|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}}</ref>线性时序逻辑和{{link-en|计算树逻辑|Computation tree logic}}两者可以归入更广义的{{link-en|CTL*|CTL*}}中。

==语法和语义==
一个线性时序逻辑公式由以下三种要素构成：<ref>Sec. 5.1 of Christel Baier and Joost-Pieter Katoen, ''Principles of Model Checking'', MIT Press {{cite web|url=https://mitpress.mit.edu/catalog/item/default.asp?tid%3D11481%26ttype%3D2 |title=Archived copy |access-date=2011-05-17 |url-status=dead |archive-url=https://web.archive.org/web/20101204043002/http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=11481 |archive-date=2010-12-04 }}</ref><ref name=CNslides />
* 原子[[命题变量]]
* [[逻辑运算符]]：“[[逻辑非|非]]”（¬）、“[[逻辑合取|与]]”（∧）、“[[逻辑析取|或]]”（∨）、“[[实质条件|条件]]”（→）、“[[双条件]]”（↔）。
* 时态运算符：'''X'''，'''F'''，'''G'''，'''U'''，'''R'''等

时态运算符的语义如下表所示，其中 ''φ'' 和 ''ψ'' 为原子命题变量：
{| class="wikitable"
|-
!字母表示
!符号表示
!说明
![[克里普克结构|克里普克路径]]示意图
|-
| colspan="4" | [[一元運算]]:
|-
|'''X''' ''φ''
|<math>\bigcirc \varphi</math>
|ne'''X'''t（下一刻）: ''φ'' 在下一时刻为真
|[[File:Ltlnext.svg|LTL next operator]]
|-
|'''F''' ''φ''
|<math>\Diamond \varphi</math>
|'''F'''inally（最终）: ''φ'' 在以后某个时刻（最终）会真
|[[File:Ltleventually.svg|LTL eventually operator]]
|-
|'''G''' ''φ''
|<math>\Box \varphi</math>
|'''G'''lobally（总是）: 从当前时刻起， ''φ''  总是为真
|[[File:Ltlalways.svg|LTL always operator]]
|-
| colspan="4" | [[二元运算]]:
|-
|''ψ'' '''U''' ''φ''
|<math>\psi\;\mathcal{U}\,\varphi</math>
|'''U'''ntil（直到）: ''ψ'' 总是为真，直到某一时刻''φ'' 为真；该时刻可以为当前时刻或者以后某个时刻
|[[File:Ltluntil.svg|LTL until operator]]        
|-
|''ψ'' '''R''' ''φ''
|<math>\psi\;\mathcal{R}\,\varphi</math>
|'''R'''elease（释放）: ''φ'' 总是为真，直到某一时刻''ψ''和''φ'' 同时为真；如果''ψ'' 从未为真，则''φ'' 必须保持永远为真
|[[File:Ltlrelease-stop.svg|LTL release operator (which stops)]]<br>
[[File:Ltlrelease-nostop.svg|LTL release operator (which does not stop)]]
|-
|''ψ'' '''W''' ''φ''
|<math>\psi\;\mathcal{W}\,\varphi</math>
|'''W'''eak until（弱直到）:  ''ψ'' 总是为真，直到某一时刻''φ'' 为真；如果''φ'' 从未为真，则''ψ'' 必须保持永远为真
|[[File:Ltluntil.svg|LTL weak until operator (which stops)]]<br> 
[[File:Ltlweakuntil2.svg|LTL weak until operator (which does not stop)]]
|- 
|''ψ'' '''M''' ''φ''
|<math>\psi\;\mathcal{M}\,\varphi</math>
|Strong release（强释放）: ''φ'' 总是为真，直到某一时刻''ψ''和''φ'' 同时为真；该时刻可以为当前时刻或者以后某个时刻
|[[File:Ltlrelease-stop.svg|LTL strong release operator]] 
|}

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

==等价变换==
* 分配律<ref>{{cite book |author1=V.S. Alagar |coauthors=K. Periyasamy |title=Specification of Software Systems |date=2012 |publisher=Springer |isbn=1475729219 |page=186}}</ref><ref>{{cite book |author1=Fred Kroger |coauthors=Stephan Merz |title=Temporal Logic and State Systems |date=2008 |publisher=Springer |isbn=3540674012 |pages=417-418}}</ref>
{| class="wikitable"
|-
! colspan="4" | 分配律
|-
| '''X''' (φ ∨ ψ) ≡  ('''X''' φ) ∨ ('''X''' ψ)|| '''X''' (φ ∧ ψ)≡  ('''X''' φ) ∧ ('''X''' ψ)  || '''X''' (φ '''U''' ψ)≡  ('''X''' φ) '''U''' ('''X''' ψ)
|-
| '''F''' (φ ∨ ψ) ≡  ('''F''' φ) ∨ ('''F''' ψ)|| '''G''' (φ ∧ ψ)≡  ('''G''' φ) ∧ ('''G''' ψ)  || 
|-
| ρ '''U''' (φ ∨ ψ) ≡  (ρ '''U''' φ) ∨ (ρ '''U''' ψ)|| (φ ∧ ψ) '''U''' ρ ≡  (φ '''U''' ρ) ∧ (ψ '''U''' ρ)  || 
|}
* 逻辑“非”运算
{| class="wikitable"
|-
! colspan="4" | 逻辑“非”运算
|-
| '''''X''' 自[[对偶 (数学)|对偶]]'' || '''''F''' 和 '''G''' 对偶'' || '''''U''' 和 '''R''' 对偶''  || '''''W''' 和 '''M''' 对偶''
|-
| ¬'''X''' φ ≡ '''X''' ¬φ  || ¬'''F''' φ ≡ '''G''' ¬φ          || ¬ (φ '''U''' ψ) ≡ (¬φ '''R''' ¬ψ) || ¬ (φ '''W''' ψ) ≡ (¬φ '''M''' ¬ψ)
|-
|                          || ¬'''G''' φ ≡ '''F''' ¬φ          || ¬ (φ '''R''' ψ) ≡ (¬φ '''U''' ¬ψ) || ¬ (φ '''M''' ψ) ≡ (¬φ '''W''' ¬ψ)
|}
* 特殊时态属性
{| class="wikitable"
|-
! colspan="3" | 特殊时态属性
|-
| '''F''' φ ≡ '''F''' '''F''' φ || '''G''' φ ≡ '''G''' '''G''' φ || φ '''U''' ψ ≡  φ '''U''' (φ '''U''' ψ)
|-
| φ '''U''' ψ ≡  ψ ∨ ( φ ∧ '''X'''(φ '''U''' ψ) ) || φ '''W''' ψ ≡  ψ ∨ ( φ ∧ '''X'''(φ '''W''' ψ) ) || φ '''R''' ψ ≡ ψ ∧ (φ ∨ '''X'''(φ '''R''' ψ) )
|-
| '''G''' φ ≡ φ ∧ '''X'''('''G''' φ) ||'''F''' φ ≡ φ ∨ '''X'''('''F''' φ) || 
|}

==特性表达==
有两种主要特性可以使用线性时序逻辑来表达：<ref>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</ref><ref>{{cite journal |author1=Bowen Alpern |coauthors=Fred B. Schneider |title=Recognizing safety and liveness |journal=Distributed Computing |date=1987 |url=https://cs.cornell.edu/fbs/publications/RecSafeLive.pdf |access-date=2022-08-07 |archive-date=2022-07-21 |archive-url=https://web.archive.org/web/20220721181859/https://www.cs.cornell.edu/fbs/publications/RecSafeLive.pdf |dead-url=no }}</ref>
* 安全性（safety）：即某种不良性质 ''φ'' 永不出现，'''G'''&not;''&varphi;''
* 活性（liveness）<：即某种良好的性质 ''ψ'' 一直保持，'''GF'''''&psi;'' 或 '''G'''(''&varphi;'' →'''F'''''&psi;'')

==参见==
* [[克里普克结构]]
* [[时间逻辑]]

==参考文献==
{{Reflist|2}}

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