技術要約：ハイブリッドシステムの特性に対する実行時強制

問題提起

自律システムおよびサイバー物理システム（CPS）は、不確実で動的な環境下で動作するため、従来の設計時検証（形式検証、シミュレーション）だけでは安全性を保証するには不十分な場合が多い。実行時検証（Runtime Verification: RV）は、実行中に特性違反を検出することはできるが、それは受動的なものであり、違反を防止するものではない。実行時強制（Runtime Enforcement: RE）は、システムの振る舞いを修正するために能動的に介入することで、この問題に対処する。しかし、既存のREフレームワークは、複雑なリアクティブシステムに適用する場合、以下のような重大な制限に直面する：

1. 離散的ダイナミクス対連続的ダイナミクス： ほとんどのフレームワークは、非時刻型または離散時間仕様（例：離散型タイムオートマトン）に依存している。これらは、複雑な連続ダイナミクスを示すシステムに対しては不適切である。なぜなら、それらは密な時間の進化をモデル化できず、離散的なサンプリングポイントの間で介入することができないからである。
2. 介入の粒度： 既存のアプローチは、離散的な時刻におけるイベントの遅延や抑制に限定されることが多い。これらは、任意の時刻にイベントを挿入したり、連続時間のモニタリングを行ったりする能力を欠いており、連続的な状態軌道における安全性を維持するために不可欠な機能が不足している。
3. リアクティブシステムの制約： 多くの強制メカニズム（例：実行の停止や長いバッファリング）は、ライブネスを維持し厳格なタイミング制約を満たす必要があるリアクティブシステムにおいては、実現不可能である。

対処すべき核心的な問題は、ハイブリッドオートマトン（HA）として指定された安全特性を扱うことができ、連続時間のモニタリングと、プロアクティブで微細な修正介入（抑制、遅延、挿入）を可能にする実行時強制フレームワークの欠如である。

メソドロジー

本論文では、安全要件を**安全ハイブリッドオートマトン（Safety HA）**を用いてモデル化する実行時強制フレームワークを提案する。この形式手法は、離散的な実行ステップ（遷移ガード経由）と、連続的なダイナミクス（微分方程式および状態不変量経由）の両方を捉える。

コアコンポーネント

1. 安全ハイブリッドオートマトン (S): 特性 $\phi$ は、一意の非受理的な「シンク（Sink/トラップ）」ロケーションを持つHAとして定式化される。安全不変量（例：最小距離）が違反されるたびに、シンクへの遷移が発生する。その他のすべてのロケーションは受理状態である。
2. 強制関数 ($E_\phi$): 強制器は、監視対象システム（System under Monitor: SuM）と環境の間のレイヤーとして機能する。これは、離散的な同期ポイント（クロックティック、$ptick$ と表記）において、入力イベントのストリームと環境状態を受け取る。
3. 修正アクション： 強制器は、以下の手法を用いて修正された出力ストリームを合成する：
   • 抑制 (Suppressing): 不安全なイベントを破棄し、前の状態を維持するために「スタッター（stutter）」イベントを出力する。
   • 遅延 (Delaying): ガード条件が満たされるまで、イベントを後方に延期する。
   • 挿入 (Inserting): 直近の不変量違反を防ぐために、任意の時刻（$ptick$ の間であっても）に新しいイベントをプロアクティブに挿入する。
4. オンラインアルゴリズム： 強制アルゴリズムは、同期的なリアクティブループ内で動作する：
   • 初期化： 現在の環境状態に基づいてHAを初期化する。
   • 時間の経過： アルゴリズムは、次のイベントまたは $ptick$ までの時間間隔におけるシステム状態の連続的な進化をシミュレートする。
   • 不変量チェック： 現在のロケーションの不変量内に連続的な軌道が留まっているかを検証する。
   • 決定ロジック：
     • 不変量が保持されており、かつ入力イベントに対するガードが満たされている場合、そのイベントを通過させる。
     • 不変量は保持されているが、ガードが満たされていない場合、そのイベントは抑制（遅延）される。
     • 不変量が違反された場合、アルゴリズムは延期されたアクションが有効であるかを確認し、存在しない場合は、次の $ptick$ までにシステムを安全な状態へ導くために、有効な遷移（enabled transitions）から新しいアクションを合成・挿入する。

形式的制約

強制器は、以下の4つの制約を満たすように定義される：

• 健全性 (Soundness): 出力シーケンスは常に安全特性 $\phi$ を満たさなければならない。
• 即時性 (Instantaneity): 強制器は入力に対して即座に反応しなければならず、プロアクティブにイベントを挿入することができる。
• 単調性 (Monotonicity): 拡張された入力シーケンスに対する出力は、その接頭辞に対する出力の継続でなければならない。
• 透明性 (Transparency): 強制器は最小限の介入を行う。システムの振る舞いが安全である場合、強制器は恒等関数として機能する。

主要な貢献

1. 新しいフレームワーク： ハイブリッドオートマトン仕様に基づく、連続時間モニタリングと修正介入を可能にする、リアクティブCPSのための実行時強制フレームワーク。
2. 形式的定義： 安全ハイブリッドオートマトンを介して指定された安全特性のための実行時強制問題の形式的定義であり、REを非時刻型および離散時間形式を超えて拡張する。
3. 強制可能性の条件： すべての非違反状態から、有効な遷移を介して受理状態に到達可能であるという、強制可能性（enforceability）に関する条件の確立。
4. オンラインアルゴリズム： イベントの抑制、遅延、および挿入を行いながら、システムのタイミング制約を遵守して安全な実行トレースを合成できるアルゴリズム。
5. ケーススタディ： 適応型クルーズコントロール（ACC）システムへの詳細な適用であり、故障した可能性のあるコントローラの出力を安全なトレースへと合成できることを示す。

結果と評価

提案されたフレームワークは、主要なコントローラが故障していると仮定し、最小安全距離の制約（$d > 10$ メートル）に違反する可能性のあるコマンドを発行する可能性がある、適応型クルーズコントロール（ACC）のシナリオを用いて評価された。

• シナリオ： システムは、加速度（$a$）、速度（$v$）、および相対距離（$d$）を含む変数を監視した。コントローラは、介入がなければ衝突（距離 $< 10$m）に至る一連のイベント（加速、クルーズなど）を生成した。
• 強制の結果： 強制器は、不安全なイベントストリームを正常に遮断した。不安全な加速コマンドを抑制し、他のコマンドを遅延させ、安全不変量を維持するために精密な時刻（例：$t \approx 10.67$）に減速コマンドを挿入した。
• パフォーマンス：
  • レイテンシ： イベントあたりの平均応答時間は 4.67ミリ秒 であった。
  • オーバーヘッド： フレームワークによる計算オーバーヘッドは無視できる程度であり、標準的なハードウェア（Intel Core i5, 8GB RAM）上で全トレースを15.098秒で処理した。
  • 結論： 結果は、厳格なタイミング制約を違反することなく、高頻度のリアクティブ環境で効果的に動作できる本フレームワークの能力を裏付けている。

意義と主張

本論文の主な意義は、離散時間強制と、サイバー物理システムの連続的な性質との間のギャップを埋めることにあると主張されている。ハイブリッドオートマトンを利用することで、本フレームワークは以下を実現する：

• 離散型タイムオートマトン（DTA）のアプローチに欠けている、密な時間のモニタリング（離散的なサンプリングポイント間でのモニタリング）を可能にする。
• 離散的なティックに限定されることなく、任意の時刻にプロアクティブな介入（イベントの挿入）を可能にする。
• システム挙動に対するより細かい制御を提供し、安全要件への連続的な遵守を保証する。

著者らは、彼らの知る限り、表現力豊かなHA仕様をサポートし、リアクティブシステムに適した既存の強制フレームワークは存在しないと述べている。彼らは、本研究を、受動的な検証を超え、不確実な環境で作動する自律システムのための、より強力な安全性保証への一歩として位置づけている。

本論文は、現在の手法が安全特性（接頭辞閉じた仕様）および決定可能なハイブリッドオートマトンのサブクラスに限定されていることを認め、その範囲について控えめな姿勢を保っている。今後の課題として、ライブネス特性、非線形ダイナミクス、確率的な不確実性、および分散マルチエージェントシステムへの対応が挙げられている。