Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+

技術要約：有限トレース技術を用いた無限トレース目的関数

問題提起
線形時相論理（LTL）は、リアクティブ合成からマルコフ決定過程におけるプランニングに至るまで、AIにおける時相目的を規定するための標準的な言語である。しかし、LTLに基づく問題を解くには、伝統的にLTL式を無限語上の非決定性オートマトンへと変換し、その後に決定化（determinization）する必要がある。この決定化のステップは、理論的にも実用的にも極めて困難であり、スケーラビリティに対する大きな障壁となっている。近年のLTL合成の進展では、数式を決定的なコンポーネントへと分解するために、Manna-Pnueliの安全性・進行（safety-progress）階層に基づく正規形を利用しているが、LTLから決定性オートマトンへの変換は二重指数関数的となる。

並行して、LTLf（有限トレース上のLTL）は、決定性有限オートマトン（DFA）への効率的な変換が可能であることから注目を集めている。LTLf+は、接頭辞（prefix）を量化することでLTLfを無限トレースへと拡張するために最近導入されたものであり、Manna-Pnueli階層のクラスと一致する。LTLf+はLTLと同じ表現能力を持つが、一般的なLTLからLTLf+への構成的な変換はこれまで欠落しており、これがDFAベースの技術（最小化など）を標準的なLTL仕様に適用することを制限していた。

手法
本論文は、任意のLTL式からLTLf+への、正規化されていることを前提とした線形時間での構成的な変換を提示する。手法は主に以下の3つの段階で進行する：

1. $\Delta_2$ 正規形への正規化：
   著者らは、任意のLTL式を$\Delta_2$（リアクティビティ）正規形へと変換するために、純粋な数式書き換えシステム（Esparza, Rubio, and Sickert 2024に基づく）を利用する。この形式は、各項が特定の「極限挙動（limit-behavior）」$(M, N)$を表す項の選言へと数式を分解する。各項は以下で構成される：

   • 単純化された$\Sigma_2$ボディ式（$\phi[M, N]$）。
   • 再帰のための$\Pi_2$チェック（$\bigwedge GF(\psi[N]_\mu)$）。
   • 持続のための$\Sigma_2$チェック（$\bigwedge FG(\psi[M]_\nu)$）。
     この正規化は、元の式のサイズに対して単一指数関数的である。

2. 極限挙動ブロックの変換：
   論文では、極限挙動のチェックをLTLf+のリーフ式へと変換するための特定の変換を定義している：

   • 再帰（$\Pi_2$）： $GF(\sigma_1)$（ここで$\sigma_1 \in \Sigma_1$）という形式の式は、$\forall\exists(F(\text{tight}(\text{finX}(\sigma_1))))$へと変換される。著者らは、式の充足が接頭辞の終端に結び付けられるように、chop演算子を用いた「タイトな補完（tight completion）」の概念を導入し、無限の接頭辞上での偽の充足を防いでいる。
   • 持続（$\Sigma_2$）： $FG(\pi_1)$（ここで$\pi_1 \in \Pi_1$）という形式の式は、$\exists\forall(G(\neg\text{tight}(\neg\text{finX}(\pi_1))))$へと変換される。
   • 有限の再解釈： 著者らは、finXおよびtight演算子を定義し、文脈（安全性 vs 共安全性フラグメント）に基づいた強・弱のNext演算子の区別を含む、有限トレース上のLTL演算子の再解釈を行う。

3. $\Sigma_2$ ボディの変換：
   正規化された式の主要なボディ（$\phi[M, N]$）に対し、著者らは、固定された極限挙動 $(M, N)$ の下では、すべての安全性リーフ（G式）がいずれ永久に成立するという事実を利用する。これらの安全性リーフを投影（ttで置き換え）することで、ボディ式は実質的に$\Sigma_1$（共安全性）式へと簡約される。著者らは、特定の極限挙動を示すトレースにおいて、ボディが「収束的（convergent）」であることを証明している。すなわち、その無限トレース上での充足は、すべての（十分大きな）接頭辞における有限再解釈の充足と等価である。これにより、ボディは存在・全称量化子を用いて $\exists\forall(\text{finX}(\phi[M, N]))$ と変換することが可能になる。

主な貢献

• 構成的な変換： 本論文は、一般的なLTLからLTLf+への初の構成的な変換を提供し、Aminofら（2025）の存在論的な結果と実用的なアルゴリズムとの間の溝を埋めるものである。
• 線形変換計算量： 正規化されたLTL形式からLTLf+への変換は、正規化された式のサイズに対して線形である。
• 複雑性の保存： この変換パイプライン（LTL $\to$ 正規形 $\to$ LTLf+ $\to$ DFA）が、元のLTLのサイズに対して二重指数関数的であることを示している。これは、最新の直接的なLTL-to-automaton変換と比較して、追加の指数的増大を導入しないことを意味する。
• DFA技術の有効化： この変換により、元々LTLで定式化された問題に対して、DFAベースの技術（オートマトンの最小化など）を適用することが可能になる。これは、非決定性Büchiオートマトンの最小化がPSPACE完全であるのに対し、DFAは効率的に最小化できるため重要である。

結果
著者らは、任意のLTL式 $\phi$ と無限トレース $w$ について、$w \models_{inf} \phi$ であることと $w \models_{inf} \text{Translation}(\phi)$ であることが同値であることを証明している。得られるLTLf+式は、元の部分式の有限トレース上の再解釈に対して、接頭辞量化子（$\forall, \exists, \forall\exists, \exists\forall$）を適用したブール結合である。変換された式の長さは $2^{O(|\phi|)}$ で抑えられ、これは中間的な $\Delta_2$ 正規形のサイズと一致する。

意義
本論文は、任意のLTL仕様に対する実用的な中間言語としてLTLf+を確立する。LTLをLTLf+に変換することで、有限トレース論理のために開発された効率的なDFAベースの技術のエコシステムを、無限トレースの問題へと拡張できる。これには以下が含まれる：

• リアクティブ合成： 有限ホライゾン仕様に限定されていた能力を拡張し、DFA最小化を利用して合成を高速化することを可能にする。
• プランニングと学習： LTL目的関数が使用されるマルコフ決定過程、確率的プランニング、および強化学習への技術の適用範囲を広げる。

著者らは、特定の義務（obligations）のようなフラグメントについては、正規化やタイトな補完をスキップできる最適化を含め、SPOTライブラリ上でこの変換を実装したと述べている。本研究は、LTLf+を単なる理論的な拡張としてではなく、AIにおけるLTLベースの推論のスケーラビリティを向上させるための、実行可能なエンジニアリング経路として位置づけている。