線形時相論理（せんけいじそうろんり、Linear Temporal Logic、LTL）とは、時間に関する様相を持つ様相時相論理である。LTLでは、ある条件が最終的に真となるとか、別の事実が真になるまでその条件は真であるとかいった将来の出来事について論理式で表すことができる。LTL では変項 formula_1 や一般的な論理作用素 formula_2 の他に以下の時相様相作用素を使用する:最初の3つの作用素は単項演算である。従って、formula_3 が整論理式であれば、N formula_3 も整論理式である。最後の2つの作用素は二項演算である。従って、formula_3 と formula_6 が整論理式であれば、formula_3 U formula_6 も整論理式である。LTLの論理式の評価は経路上の位置における逐次的な真理値として評価される。LTLの論理式はその経路上の位置 0 において真であるときのみ真である。様相作用素の意味論は以下のように与えられる。以下の恒等式が成り立つことから、作用素の種類を減らすことができる:線形時相論理で表現できる重要な特性として次の2種類がある。安全性特性は「何か悪いことが決して起こらない」ことを意味する（Gformula_13formula_3）。活性特性は「何か良いことがいずれ起きる」ことを意味する（Fformula_6）。安全性特性とは、有限な期間での反例を無限の時系列に拡張しても反例であるような状態である。一方活性特性は、有限な期間での反例を無限の時系列に拡張したとき、それが反例でなくなる（その論理式が真となる）状態である。線形時相論理(LTL) は CTL* の一部である。LTLは、後者（successor、ペアノの公理参照）と「小なり」の関係についての一階述語論理 FO[S,<] と等価である。また、クリーネスターのない正規表現や loop complexity が 0 であるような決定性有限オートマトンも LTL と等価である。

出典:wikipedia