技術的概要：信号時相論理仕様を有する確率的非線形システムのためのフィードバック運動計画

問題定式化

本論文は、信号時相論理（STL）仕様に制約された連続時間確率的非線形システムに対するフィードバック運動計画の課題に取り組む。空間的境界のみを符号化する古典的な安全集合制約とは異なり、STL は、「A を B より前に訪問する」といったシーケンシング、デッドライン、永続性などの複雑な時空間要件の指定を可能にする。

核心的な難しさは、モデル化されていないダイナミクスと外部擾乱の存在にある。これらは、センサーまたはアクチュエータノイズなどの無界な確率ノイズとしてモデル化される。このような設定では、最悪ケースのロバスト制御手法は過度に保守的となる。逆に、既存の確率的アプローチは、連続時間非線形システムへのスケーラビリティに欠けるか、厳密な保証を欠いていることが多い。具体的な問題は、確率制約付き STL 軌道最適化として定式化される：確率軌道 $X_t$ が STL 式 $\phi$ を高い確率（例：$1-\delta \geq 99.99\%$）で満たすことを保証しつつ、コスト関数を最小化する制御方策 $u$ を見出すことである。

主要な課題は、STL の論理的および時間的構造を同時に満たしつつ、数えきれない時間点にわたる軌道レベルの確率制約を課すことの非実用性にある。

手法

著者らは、扱いにくい確率問題を、制約を厳密化した**決定論的 STL 軌道最適化（STLTO）**問題に変換する体系的な枠組みを提案する。手法は 3 つの主要な構成要素からなる：

1. 述語侵食戦略

核心的な考え方は、ランダム性と論理を分離することである。著者らは、元の STL 述語を「侵食」（厳密化）して決定論的な代理問題を生成する述語侵食戦略を導入する。

• メカニズム： 確率軌道 $X_t$ と関連する名义的な決定論的軌道 $x_t$ との間の偏差を束縛するために、**確率到達チューブ（PRT）**が構築される。
• 変換： 名义的な軌道が「侵食された」STL 式 $\tilde{\phi}$ を満たす場合（ここで各述語集合 $C$ は $C \ominus E_t$ に置き換えられ、$E_t$ はチューブの断面である）、確率軌道は確率 $1-\delta$ 以上で元の式 $\phi$ を満たすことが保証される。
• 結果： これにより、確率制約付き問題は、既存の数値ツールで解ける標準的な決定論的最適化問題（8）に変換される。

2. 収束理論に基づく PRT 構築

PRT を tight（過度な保守性を避ける）に保つために、著者らは収束理論を活用する。

• フィードバック設計： 閉ループシステムを強く収束するようにするフィードバック追跡制御器が設計される。これにより、名义的な軌道からの確率的偏差が発散しないことが保証される。
• tight な境界： 新しい**アフィン・マルチンゲール（AM）と平均モーメント生成関数（AMGF）**を用いて、PRT に対する軌道レベルの境界 $r_{\delta,t}$ が導出される。
• 重要な洞察： 導出された境界は $O(\sqrt{\log(T/\delta)})$ としてスケーリングし、これは伊藤確率システムに対して可能な限り tight な依存関係である。これは、時間または離散化ステップに線形にスケーリングすることが多い、和の境界（union bounds）に依存する手法よりもはるかに保守性が低い。

3. フィードバック運動計画パイプライン

この枠組みは、2 段階の合成プロセスで動作する：

1. オフライン計画： 決定論的代理問題（8）を解き、名义的な軌道 $(x^*, u^*)$ とフィードフォワード制御を得る。
2. オンライン実行： 複合制御則 $u_t = u^*_t + K_t(X_t; x^*_t, u^*_t)$ を適用する。ここで $K_t$ は、名义的な計画の周りで確率システムを安定化する追跡制御器（例：時間可変 LQR または時間可変制御収束計量）である。

• 結合： 本論文は、チューブサイズに依存する計画ホライズンと、チューブサイズを決定する制御器合成との間の結合を、反復アルゴリズムまたは軌道に依存しない TVCCM 合成を用いた非結合設計を通じて扱う。

主要な貢献

本論文は、以下の具体的な貢献を行う：

1. 連続時間 STL 侵食： 一般の連続時間非線形システムに適用可能な、PRT に基づく述語の侵食によって確率制約付き STL 軌道最適化問題を決定論的なものに変換する体系的な戦略。
2. 厳密な確率的保証： 既存の離散時間または線形だけの手法の限界を克服し、確率システムに対して厳密な確率的保証（例：$\geq 99.99\%$ の充足）を提供する、フィードバック制御合成のための完全なパイプライン。
3. tight な PRT 境界： 収束理論とマルチンゲールに基づく分析を用いた、連続時間における和の境界の保守性を回避する、tight な軌道レベルの PRT 境界の開発。
4. 実証的検証： 4 つのロボティックベンチマーク（ダブルインテグレータ、ダブインズカー、PVTOL、クアッドロター）における広範なシミュレーションと、四足歩行ロボットにおける実世界実験を通じた、枠組みのスケーラビリティと有効性の実証。

結果

提案された枠組みは、4 つのシミュレーションベンチマークと実世界の四足歩行ロボット（Unitree Go1）で評価された。

• シミュレーション性能：

  • 本手法は、すべての 4 つのベンチマーク（ダブルインテグレータ、ダブインズカー、PVTOL、3D クアッドロター）において、10,000 回の確率ロールアウトで100% の STL 仕様充足を達成した。
  • ベースライン： 「非ロバスト」な決定論的計画や「縮小ホライズン MPC（SHMPC）」を含む競合手法は、有意に低い充足率（0.2% から 77.6% の範囲）を示し、確率システムに対して決定論的計画のみでは不十分であることを示した。
  • 保守性： 離散時間のベースライン（DPRT および STLCD）との比較により、提案された連続時間手法の方が保守性が低いことが示された。具体的には、提案手法における侵食半径は離散化ステップサイズ $N$ に依存せず、リスクレベル $\delta$ に対して（$\sqrt{\log(1/\delta)}$ として）より緩やかにスケーリングするのに対し、離散時間の和の境界は線形にスケーリングする。

• 実世界実験：

  • 本枠組みは、高レベルのユニサイクル抽象化を用いて Unitree Go1 四足歩行ロボットに展開された。
  • 2 つの異なるナビゲーションタスク（到達・回避と通過・前）における50 回のハードウェア実行において、ロボットは状態推定ノイズ、作動ノイズ、モデルの不一致にもかかわらず、すべての試行でタスクを正常に完了し、STL 仕様を満たした。

意義と主張

著者らは、この研究が、連続時間非線形システムに対する不確実性下での信頼性の高い高レベル時相論理計画を可能にすることで、ロボティクスの自律性における重要なギャップを埋めると主張する。

• 保守性の克服： 本論文は、既存の確率的手法は、和の境界に起因して過度に保守的であるか、近似に起因して形式的な保証を欠いていると論じる。提案された PRT ベースの侵食戦略は、厳密でありながら保守性の低い代替案を提供する。
• スケーラビリティ： 確率問題を決定論的な問題に還元することで、本手法は既存の数値最適化ソルバー（SNOPT、MOSEK など）を活用し、複雑な非線形ダイナミクスにもスケーラブルにする。
• 実用性： 実世界の四足歩行ロボットへの成功した展開は、理論的枠組みが、完全なシステムモデルを必要とすることなく、ハイブリッドダイナミクスや衝突イベントを含む実世界の不確実性を処理するのに十分な頑健性を持っていることを示している。

本研究は、確率的設定における信頼性の高い STL 充足のために、述語侵食とフィードバック制御による確率制約の明示的な処理が必要であり、不確実な環境における信頼性の高い自律性への体系的な道筋を提供すると結論づけている。