Value Functions for Temporal Logic: Optimal Policies and Safety Filters

技術的概要：時相論理における価値関数：最適方策と安全フィルタ

問題定義
基本的な到達、回避、および到達 - 回避問題に対するベルマン方程式は確立されているが、未割引の無限時間地平における価値最適性と方策最適性の関係は、複雑な時相論理（TL）仕様に対しては微妙なものとなる。特に、到達 - 回避問題（Until 仕様に相当）において、Q 関数を貪欲に最大化することが、価値関数自体が最適であっても、タスクの完了を無限に先送りする方策を生み出すという決定的な病理が生じる。これは、無限軌道に対する最適動作系列が本質的にマルコフ的ではないためである。最適入力は、残りの無限時間地平の仕様を満たすために、分解グラフにおける現在の価値の最大化から構成要素の価値への「切り替え」を行う必要がある。双目的問題に対する状態拡張などの既存手法は、ネストされたUntil、Globally、およびGlobally-Until仕様を含む複雑な式への一般化に苦慮している。さらに、単純な回避や到達 - 回避タスクを超えて、複雑な TL 仕様の充足を保証する安全フィルタの必要性がある。

手法
著者は、問題の非マルコフ的性質を処理するために、状態履歴に対して価値関数と Q 関数を一般化するフレームワークを提案する。この手法は、TL に対する価値関数の代数的分解に依存し、構成要素の価値関数のグラフへと展開する。

1. 非マルコフ的価値関数: 本論文は、現在の状態だけでなく状態履歴 $x_{0:t}$ に対して最適価値関数 $V^*$ および Q 関数 $Q$ を定義する。これにより、方策は時間的制約を満たすために必要な履歴を考慮できるようになる。
2. 時間拡張システムと証人時刻: Until ($U$) 仕様における先送り問題に対処するため、著者はタイマーを備えた時間拡張システムを導入する。彼らは「最適証人時刻」$\sigma^*$ を定義する。これは、軌道が最適ロバストネススコアを達成する最早の時刻である。これにより、有限時間地平の貪欲戦略（証人時刻内での Q 関数の最大化）から、残りの部分式を満たす接尾語方策へと切り替わる方策の構築が可能となる。
3. 構成的方策構築: 本論文は、TL 式の特定のフラグメント（定義 3）に対する最適方策を構築する。これには以下が含まれる：
   • 命題式。
   • Until ($p U \phi$)、Next ($X\phi$)、およびGlobally ($Gp$) 演算子。
   • Globally-Until ($G(\bigvee p_i U r_i)$)。これは Büchi 受理条件を符号化する。
   • 論理和および命題論理積。
     構築は、部分式に対する最適方策の存在（仮定 2）を前提とし、それらを再帰的に組み合わせる。Globally-Untilについては、必要な状態集合への無限回の訪問を確保するため、方策は各Until構成要素を順次訪問する。
4. 安全フィルタリング: 著者は、Q 関数が安全フィルタとして機能し得ることを示す。仕様を非負のロバストネスで満たすことができない失敗集合を定義する。最小制限介入方式が提案される。すなわち、名义方策の動作が非負の Q 値（将来の充足可能性を示す）をもたらす場合、それを許可する。そうでない場合、システムは Q 関数を最大化する動作に切り替わる。特定の仮定（例えば、有界でないUntil演算子の欠如など）の下で、このフィルタは仕様の充足を保証する。

主要な貢献

1. 価値関数の一般化: 本論文は、最適価値関数と Q 関数を状態履歴に一般化し（定義 1）、履歴に対する最適性を定義する（定義 2）。これにより、無限時間地平 TL 問題の非マルコフ的性質に対処する。
2. 構成的最適方策: 広範なクラスの TL 式（定義 3）に対して、著者は関連するロバストネス指標に対する構成的最適方策を構築する（定理 1–8）。これには、UntilおよびGlobally-Until仕様における先送り病理の処理が含まれる。
3. 最小制限安全フィルタ: 本作業は、（潜在的に非最適の）履歴に対する Q 関数が、名义方策に対する最小制限の安全フィルタをもたらすことを示す（定理 9, 10）。このフィルタは、式が特定の構造的制約を満たす限り、名义方策の先行経路を尊重しつつ仕様の充足を保証する。

結果と実証
本論文は、理論的証明と 2 つのハードウェア/ソフトウェア実証を通じて提案フレームワークを検証する：

• 2 エージェントグリッドワールド: 著者は、時間制限付き到達、安全性、および活性制約を含む複雑な仕様を伴う 4 次元の結合状態 - 動作問題を解決する。導出された最適方策（$\pi_{spec}$）がシステムを仕様を満たすように導くことを実証する。さらに、個別には結合仕様を満たさない「コーヒー」および「お茶」の名义方策に対するフィルタとして使用した場合、このフィルタは結合システムが複雑なタスクを満たすことを保証する。これに対し、標準的な「安全性のみ」のフィルタはデッドロックと失敗をもたらす。
• 単一エージェントドローン: Crazyflie ドローンを用いて、障害物のあるナビゲーションタスクにおいて方策を実証する。提案された TL フィルタは、複雑な時間的制約（特定のゾーンをループすること、壁を回避することなど）を満たしつつ、ドローンを作業場所へ導く。これに対し、フィルタリングされていない名义方策、または安全性制約のみに基づくフィルタは、ドローンが閉じ込められたり衝突したりする結果となる。

重要性
本論文は、最近の分解結果を拡張することにより、広範なクラスの TL 式の価値に対する最適方策を生成する実用的なアプローチを提供すると主張する。その主な重要性は、無限時間地平タスクにおける貪欲な Q 最大化の失敗という病理を解決し、単なる安全性だけでなく複雑なタスクの充足を保証する安全フィルタを合成するメカニズムを提供する点にある。ネストされたUntilおよびGlobally-Until仕様を含む解可能な式の範囲を拡張することで、この作業は、複雑で安全性が重要な時間的タスクにおけるハミルトン - ヤコビ到達性と強化学習の間のギャップを埋める。