線形時相論理

LTL では変項 ${\displaystyle p_{1},p_{2},...}$ や一般的な論理作用素 ${\displaystyle \neg ,\lor ,\land ,\rightarrow }$ の他に以下の時相様相作用素を使用する:

• N （next）
• G （globally）
• F （in the future）
• U （until）
• R （release）

最初の3つの作用素は単項演算である。従って、${\displaystyle \phi }$ が論理式であれば、N ${\displaystyle \phi }$ も論理式である。最後の2つの作用素は二項演算である。従って、${\displaystyle \phi }$ と ${\displaystyle \psi }$ が論理式であれば、${\displaystyle \phi }$ U ${\displaystyle \psi }$ も論理式である。

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

さらに見る ...

文字表記	記号表記	説明	ダイアグラム
単項演算
N ${\displaystyle \phi }$	${\displaystyle \circ \phi }$	Next: ${\displaystyle \phi }$ は次の状態で真である。（X と表記することもある）
G ${\displaystyle \phi }$	${\displaystyle \Box \phi }$	Globally: ${\displaystyle \phi }$ は今後常に真である。
F ${\displaystyle \phi }$	${\displaystyle \Diamond \phi }$	Finally: ${\displaystyle \phi }$ は将来のいずれかの時点で真となる。
二項演算
${\displaystyle \psi }$ U ${\displaystyle \phi }$	${\displaystyle \psi {\mathcal {U}}\phi }$	Until: ${\displaystyle \phi }$ は現在または将来の時点で真であり、かつ ${\displaystyle \psi }$ はその時点まで真である。その時点以降 ${\displaystyle \psi }$ は真になるとは限らない。
${\displaystyle \psi }$ R ${\displaystyle \phi }$	${\displaystyle \psi {\mathcal {R}}\phi }$	Release: ${\displaystyle \psi }$ が真となる時点まで ${\displaystyle \phi }$ は真であり続ける（その後は真になるとは限らない）。また、${\displaystyle \psi }$ が真となることがない場合は、${\displaystyle \phi }$ は真のままである。

閉じる

以下の恒等式が成り立つことから、作用素の種類を減らすことができる:

• F ${\displaystyle \phi }$ = true U ${\displaystyle \phi }$
• G ${\displaystyle \phi }$ = false R ${\displaystyle \phi }$ = ${\displaystyle \neg }$ F ${\displaystyle \neg }$${\displaystyle \phi }$
• ${\displaystyle \psi }$ R ${\displaystyle \phi }$ = ${\displaystyle \neg }$(${\displaystyle \neg }$${\displaystyle \psi }$ U ${\displaystyle \neg }$${\displaystyle \phi }$)

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

線形時相論理(LTL) は CTL* (英語版) の一部である。

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

• 有限状態検証における時相論理
• 計算木論理 (CTL)
• CTL* (英語版)
• インターバル時相論理 (ITL)

• A presentation of LTL
• Linear-Time Temporal Logic and Büchi Automata