線形時相論理
線形時相論理（せんけいじそうろんり、Linear Temporal Logic、LTL）とは、時間に関する様相を持つ様相時相論理である。LTLでは、ある条件が最終的に真となるとか、別の事実が真になるまでその条件は真であるとかいった将来の出来事について論理式で表すことができる。
文法
LTL では変項 [math]p_1, p_2, ...[/math] や一般的な論理作用素 [math]\neg,\or,\and,\rightarrow[/math] の他に以下の時相様相作用素を使用する:
- N （next）
- G （globally）
- F （in the future）
- U （until）
- R （release）
最初の3つの作用素は単項演算である。従って、[math]\phi[/math] が整論理式であれば、N [math]\phi[/math] も整論理式である。最後の2つの作用素は二項演算である。従って、[math]\phi[/math] と [math]\psi[/math] が整論理式であれば、[math]\phi[/math] U [math]\psi[/math] も整論理式である。
意味論
LTLの論理式の評価は経路上の位置における逐次的な真理値として評価される。LTLの論理式はその経路上の位置 0 において真であるときのみ真である。様相作用素の意味論は以下のように与えられる。
| 文字表記 | 記号表記 | 説明 | ダイアグラム |
|---|---|---|---|
| 単項演算 | |||
| N [math]\phi[/math] | [math]\circ \phi[/math] | Next: [math]\phi[/math] は次の状態で真である。（X と表記することもある） | LTL N 作用素 |
| G [math]\phi[/math] | [math]\Box \phi[/math] | Globally: [math]\phi[/math] は今後常に真である。 | LTL G 作用素 |
| F [math]\phi[/math] | [math]\Diamond \phi[/math] | Finally: [math]\phi[/math] は将来のいずれかの時点で真となる。 | LTL F 作用素 |
| 二項演算 | |||
| [math]\psi[/math] U [math]\phi[/math] | [math]\psi\mathcal{U}\phi[/math] | Until: [math]\phi[/math] は現在または将来の時点で真であり、かつ [math]\psi[/math] はその時点まで真である。その時点以降 [math]\psi[/math] は真になるとは限らない。 | LTL U 作用素 |
| [math]\psi[/math] R [math]\phi[/math] | [math]\psi\mathcal{R}\phi[/math] | Release: [math]\psi[/math] が真となる時点まで [math]\phi[/math] は真であり続ける（その後は真ではない）。また、[math]\psi[/math] が真となることがない場合は、[math]\phi[/math] は真のままである。 | 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* の一部である。
LTLは、後者（successor、ペアノの公理参照）と「小なり」の関係についての一階述語論理 FO[S,<] と等価である。また、クリーネスターのない正規表現や loop complexity が 0 であるような決定性有限オートマトンも LTL と等価である。
関連項目
- 有限状態検証における時相論理
- 計算木論理 (CTL)
- CTL*
- インターバル時相論理 (ITL)