(Translated by https://www.hiragana.jp/)
线性时序逻辑 - 维基百科，自由的百科全书 跳とべ转到内容ないよう

线性时序逻辑

维基百科ひゃっか，自由じゆう的てき百科ひゃっか全ぜん书

线性时序逻辑（英語えいご：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 (ψぷさい ∧ φふぁい)

等とう价变换

[编辑]
  • 分配ぶんぱい律りつ[8][9]
分配ぶんぱい律りつ
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. ^ 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）. 
检索自じ“https://zh.wikipedia.org/w/index.php?title=线性时序逻辑&oldid=74934477”