線形時相論理のソースを表示

'''線形時相論理'''（せんけいじそうろんり、Linear Temporal Logic、'''LTL'''）とは、時間に関する様相を持つ[[様相論理学|様相]][[時相論理]]である。LTLでは、ある条件が最終的に真となるとか、別の事実が真になるまでその条件は真であるとかいった将来の出来事について論理式で表すことができる。

==文法==
LTL では変項 <math>p_1, p_2, ...</math> や一般的な[[論理演算|論理作用素]] <math>\neg,\lor,\land,\rightarrow</math> の他に以下の時相[[様相作用素]]を使用する:

*'''N''' （next）
*'''G''' （'''g'''lobally）
*'''F''' （in the '''f'''uture）
*'''U''' （until）
*'''R''' （release）

最初の3つの作用素は単項演算である。従って、<math>\phi</math> が[[well-formed formula|論理式]]であれば、'''N''' <math>\phi</math> も論理式である。最後の2つの作用素は二項演算である。従って、<math>\phi</math> と <math>\psi</math> が論理式であれば、<math>\phi</math> '''U''' <math>\psi</math> も論理式である。

==意味論==
LTLの論理式の評価は経路上の位置における逐次的な真理値として評価される。LTLの論理式はその経路上の位置 0 において真であるときのみ真である。様相作用素の意味論は以下のように与えられる。

{| class="wikitable"
|-
! style="word-break: keep-all" | 文字表記
! style="word-break: keep-all" | 記号表記
! style="word-break: keep-all" | 説明
! style="word-break: keep-all" | ダイアグラム
|-
| colspan="4" style="text-align: center" | [[単項演算]]
|-
| style="white-space:nowrap; text-align: center" | '''N''' <math>\phi</math>
| style="text-align: center" | <math>\circ \phi</math>
|'''N'''ext: <math>\phi</math> は次の状態で真である。（'''X''' と表記することもある）
|[[Image:Ltlnext.png|LTL N 作用素]]
|-
| style="white-space:nowrap; text-align: center" | '''G''' <math>\phi</math>
| style="text-align: center" | <math>\Box \phi</math>
|'''G'''lobally: <math>\phi</math> は今後常に真である。
|[[Image:Ltlalways.png|LTL G 作用素]]
|-
| style="white-space:nowrap; text-align: center" | '''F''' <math>\phi</math>
| style="text-align: center" | <math>\Diamond \phi</math>
|'''F'''inally: <math>\phi</math> は将来のいずれかの時点で真となる。
|[[Image:Ltlevently.png|LTL F 作用素]]
|-
| colspan="4" style="text-align: center" | [[二項演算]]
|-
| style="white-space:nowrap; text-align: center" | <math>\psi</math> '''U''' <math>\phi</math>
| style="text-align: center" | <math>\psi\mathcal{U}\phi</math>
|'''U'''ntil: <math>\phi</math> は現在または将来の時点で真であり、かつ <math>\psi</math> はその時点まで真である。その時点以降 <math>\psi</math> は真になるとは限らない。
|[[Image:Ltluntil.png|LTL U 作用素]]
|-
| style="white-space:nowrap; text-align: center" | <math>\psi</math> '''R''' <math>\phi</math>
| style="text-align: center" | <math>\psi\mathcal{R}\phi</math>
|'''R'''elease: <math>\psi</math> が真となる時点まで <math>\phi</math> は真であり続ける（その後は真になるとは限らない）。また、<math>\psi</math> が真となることがない場合は、<math>\phi</math> は真のままである。
|[[Image:Ltlrelease1.png|LTL R 作用素（停止する場合）]]<br />
[[Image:Ltlrelease2.png|LTL R 作用素（停止しない場合）]]
|}

以下の恒等式が成り立つことから、作用素の種類を減らすことができる:
*'''F''' <math>\phi</math> = '''true''' '''U''' <math>\phi</math>
*'''G''' <math>\phi</math> = '''false''' '''R''' <math>\phi</math> = <math>\neg</math> '''F''' <math>\neg</math><math>\phi</math>
*<math>\psi</math> '''R''' <math>\phi</math> = <math>\neg</math>(<math>\neg</math><math>\psi</math> '''U''' <math>\neg</math><math>\phi</math>)

==重要な特性==
線形時相論理で表現できる重要な特性として次の2種類がある。安全性特性は「何か悪いことが決して起こらない」ことを意味する（'''G'''<math>\neg</math><math>\phi</math>）。活性特性は「何か良いことがいずれ起きる」ことを意味する（'''F'''<math>\psi</math>）。安全性特性とは、有限な期間での[[反例]]を無限の時系列に拡張しても反例であるような状態である。一方活性特性は、有限な期間での反例を無限の時系列に拡張したとき、それが反例でなくなる（その論理式が真となる）状態である。

==他の論理との関係==
線形時相論理(LTL) は [[CTL*]] ([[:en:CTL*|英語版]]) の一部である。

LTLは、後者（successor、[[ペアノの公理]]参照）と「小なり」の関係についての[[一階述語論理]] FO[S,<] と等価である。また、[[クリーネ閉包|クリーネスター]]のない[[正規表現]]や loop complexity が 0 であるような[[決定性有限オートマトン]]も LTL と等価である。

==関連項目==
* [[有限状態検証における時相論理]]
* [[計算木論理]] (CTL)
* [[CTL*]] ([[:en:CTL*|英語版]])
* [[インターバル時相論理]] (ITL)
<!-- * [[Büchi automaton]] -->

==外部リンク==

* [http://www.dcs.qmul.ac.uk/~pm/SaR/2004ltl.pdf A presentation of LTL]
* [http://www.cmi.ac.in/~madhavan/papers/isical97.html Linear-Time Temporal Logic and Büchi Automata]

{{DEFAULTSORT:せんけいしそうろんり}}
[[Category:数理論理学]]
[[Category:論理学]]
[[Category:時相論理]]
[[Category:数学に関する記事]]