線形時相論理

論理学において、線形時相論理または線形時間時相論理^{[1] [2]} ( LTL ) は、時間を参照する様相を持つ様相 時相論理である。 LTL では、パスの未来に関する式をエンコードすることができる。たとえば、条件は最終的に真になる、条件は別の事実が真になるまで真である、などである。これは、分岐時間と量指定子を追加で許可する、より複雑なCTL*の一部である。 LTL は命題時相論理( PTL ) と呼ばれることもある。^[3]表現力 の点では、線形時相論理 (LTL) は一階述語論理の一部である。^{[4] [5]}

LTLは1977年にアミール・プヌエリによってコンピュータプログラムの形式検証のために初めて提案されました。^[6]

LTL は、命題変数 AP、論理演算子¬ と ∨、および時間的 様相演算子 X (一部の文献ではOまたはN が使用される) とUの有限集合から構築されます。正式には、 AP上の LTL 式の集合は次のように帰納的に定義されます。

• p ∈ APの場合、p はLTL 式です。
• ψ と φ が LTL 式の場合、 δ ψ、φ ∨ ψ、X ψ、および φ U ψ は LTL 式になります。^[7]

Xは ne x tと読み、 U はuntilと読みます。これらの基本演算子の他に、LTL 式を簡潔に記述するために、基本演算子に基づいて定義された追加の論理演算子と時間演算子があります。追加の論理演算子は、 ∧、→、↔、true、およびfalseです。次に、追加の時間演算子を示します。

• Gは常に（全体的にg）
• Fは最後に
• RはリリースのR
• Wは週まで
• Mは強力な解放

LTL 式は、AP内の変数の真理値の無限シーケンスによって満たされます。これらのシーケンスは、クリプキ構造のパス上の単語(アルファベット2 ^AP上のω 単語) として見ることができます。w = a ₀、a ₁、a ₂、... をそのような ω 単語とします。w ( i ) = a _iとします。w ⁱ = a _i、a _{i +1 、... とし、これは}wの接尾辞です。正式には、単語と LTL 式の間の満足度関係 ⊨ は次のように定義されます。

• p ∈ wならばw ⊨ p (0)
• w ⊨ ¬ ψならばw ⊭ ψ
• w ⊨ φ ∨ ψ （ w ⊨ φまたはw ⊨ ψ の場合）
• w ⊨ X ψならばw ¹ ⊨ ψ（次のタイムステップではψが真でなければならない）
• w ⊨ φ U ψとなるi ≥ 0が存在し、 w ⁱ ⊨ ψであり、かつすべての 0 ≤ k < iに対してw ^k ⊨ φである ( φ はψが真になるまで真のままでなければならない)

ω 単語w がLTL 式ψ を満たすとは、 w ⊨ ψのときであるといいます。ψによって定義されるω 言語 L ( ψ )は { w | w ⊨ ψ } であり、これはψ を満たす ω 単語の集合です。 式ψ は、 w ⊨ ψとなるω 単語wが存在する場合に満たすことができます。 式ψ は、アルファベット 2 ^AP上の各 ω 単語wに対してw ⊨ ψ が成り立つ場合に有効です。

追加の論理演算子は次のように定義されます。

• φ ∧ ψ ≡ з(з φ ∨ з ψ )
• φ → ψ ≡ ¬ φ ∨ ψ
• φ ↔ ψ ≡ ( φ → ψ ) ∧ ( ψ → φ )
• 真≡ p ∨ ¬ p、ただしp ∈ AP
• 偽≡ ¬真

追加の時間演算子R、F、およびGは次のように定義されます。

• ψ R φ ≡ ¬(¬ ψ U ¬ φ ) ( φ は、 ψが真になるまで真のままです。ψが真にならない場合、φ は永遠に真のままでなければなりません。ψ rはφ を解放します。)
• F ψ ≡ 真 U ψ （最終的にψ は真になる）
• G ψ ≡ false R ψ ≡ з F з ψ ( ψ は常に true のまま)

一部の著者は、until演算子と意味論は似ているが停止条件の発生は必須ではない（releaseと同様）弱いuntil二項演算子（Wと表記）も定義している。 ^[8] UとRはどちらも弱いuntilで定義できる ため、便利な場合がある。

• ψ W φ ≡ ( ψ U φ ) ∨ G ψ ≡ ψ U ( φ ∨ G ψ ) ≡ φ R ( φ ∨ ψ )
• ψ U φ ≡ F φ ∧ ( ψ W φ )
• ψ R φ ≡ φ W ( φ ∧ ψ )

Mで表される強いリリース二項演算子は、弱い until の双対です。until 演算子と同様に定義されるため、リリース条件はどこかの時点で保持される必要があります。したがって、リリース演算子よりも強力です。

• ψ M φ ≡ з(ε ψ W ε φ ) ≡ ( ψ R φ ) ∧ F ψ ≡ ψ R ( φ ∧ F ψ ) ≡ φ U ( ψ ∧ φ )

時間演算子のセマンティクスは、次のように図式的に表されます。

φ、ψ、ρ を LTL 式とします。次の表は、通常の論理演算子間の標準的な同値性を拡張する、いくつかの便利な同値性を示しています。

LTLのすべての式は否定正規形に変換することができ、ここで

• すべての否定は原子命題の前にのみ現れる。
• 他の論理演算子true、false、∧、∨ のみが出現でき、
• 時間演算子X、U、およびRのみが出現できます。

否定伝播の上記の同値性を使用して、正規形を導出することができます。この正規形により、R、true、false、および ∧ が式に出現できますが、これらは LTL の基本演算子ではありません。否定正規形への変換によって式の長さが爆発的に増加しないことに注意してください。この正規形は、LTL 式から Büchi オートマトンへの変換に役立ちます。

LTLは、順序FO[<]のモナド一階述語論理と同等であることが示されており、これはKampの定理として知られる結果である^{[9] 。あるいは、}スターフリー言語と同等であることが示される。^[10]

計算木論理（CTL）と線形時相論理（LTL）はどちらもCTL*のサブセットですが、比較することはできません。たとえば、

• CTL の式では、LTL 式F ( G p)によって定義される言語を定義できません。
• LTL の式では、CTL 式AG ( p → ( EX q ∧ EX ¬q) ) または AG ( EF (p))によって定義される言語を定義できません。

LTL式に対するモデル検査と充足可能性はPSPACE完全問題である。LTL合成とLTL勝利条件に対するゲームの検証問題は2EXPTIME完全である。^[11]

オートマトン理論的線形時相論理モデル検査

LTL 式は、システムが従うべき制約、仕様、またはプロセスを表現するのによく使用されます。モデル検査の分野は、システムが特定の仕様を満たしているかどうかを正式に検証することを目的としています。オートマトン理論的モデル検査の場合、対象のシステムと仕様の両方が別々の有限状態マシン、つまりオートマトンとして表現され、比較されて、システムが指定されたプロパティを持つことが保証されているかどうかが評価されます。コンピューター サイエンスでは、このタイプのモデル検査は、アルゴリズムが正しく構造化されていることを検証するためによく使用されます。

無限システム実行で LTL 仕様をチェックするための一般的な手法は、モデルと同等のBüchi オートマトン(モデルである場合に正確に ω ワードを受け入れる) と、プロパティの否定と同等の別の Büchi オートマトン (否定されたプロパティを満たす ω ワードを受け入れる) を取得することです ( Büchi オートマトンに対する線形時相論理を参照)。この場合、2 つのオートマトンが受け入れる ω ワードのセットに重複がある場合、モデルが目的のプロパティに違反する動作を受け入れることを意味します。重複がない場合、モデルによって受け入れられるプロパティ違反の動作はありません。正式には、2 つの非決定性 Büchi オートマトンが交差するのは、モデルが指定されたプロパティを満たす場合のみです。^[12]

形式検証における重要な特性の表現

線形時相論理を使用して表現できるプロパティには、主に2つのタイプがあります。安全性プロパティは通常、悪いことが決して起こらないこと（G ¬ ϕ）を示しますが、活性プロパティは良いことが起こり続けること（GF ψまたはG（ϕ → F ψ））を示します。^[13]たとえば、安全性プロパティでは、自律型ローバーが崖を決して乗り越えないこと、またはソフトウェア製品が間違ったパスワードでのログイン成功を決して許可しないことが要求される場合があります。活性プロパティでは、ローバーが常にデータサンプルを収集し続けること、またはソフトウェア製品がテレメトリデータを繰り返し送信することが要求される場合があります。

より一般的には、安全性プロパティとは、すべての反例が有限の接頭辞を持ち、それが無限パスに拡張されても依然として反例であるようなプロパティです。一方、活性プロパティの場合、すべての有限パスは、式を満たす無限パスに拡張できます。

仕様言語

線形時相論理の応用例の 1 つは、嗜好に基づく計画を目的とした計画ドメイン定義言語での嗜好の指定です。^[要出典]

パラメトリック線形時相論理は、LTLをuntil-modality上の変数で拡張する。^[14]

ウィキメディア・コモンズには、線形時相論理に関連するメディアがあります。

• アクション言語
• メトリック時相論理
• 安全性と活性特性

• LTLのプレゼンテーション
• 線形時間時相論理とビュッヒオートマトン
• ボルツァーノ自由大学のアレサンドロ・アルターレ教授の LTL 授業スライド
• LTL から Buchi への変換アルゴリズムの系譜、モデル チェック用ライブラリ Spot の Web サイトより。