技術要約：サイバー物理システムのための保守的な離散抽象化構築に関する実用的なガイド

問題提起

サイバー物理システム（CPS）は、失敗が生命や財産を脅かす可能性のある安全性が極めて重要な環境で動作します。記号的モデル検査は複雑な時相論理特性の検証に効果的な手法ですが、有限状態モデルを必要とします。しかし、現実世界のCPSは連続的な状態空間上で進化します。モデル検査を適用するために、エンジニアはこれらの連続的なダイナミクスを有限状態の抽象へと離散化しなければなりません。

核心となる課題は、**健全性（soundness）をいかに確保するかです。すなわち、抽象モデルから導出された検証結果が、具体的な（concrete）システムにも転送される必要があります。これには、抽象化が具体的な状態空間および振る舞いの保守的な過剰近似（conservative over-approximation）**であることが求められます。実務において、モデル構築者は、健全性を損なったり過度な悲観主義を招いたりする4つの落とし穴に頻繁に遭遇します。

1. 具体的な状態空間のカバー不足（Under-covering）。
2. 遷移関係の過小近似（Under-approximating）（実現可能な振る舞いの欠落）。
3. 「退化的な」振る舞いの不健全な除去（Unsound pruning）（例：認証なしでの自己ループの削除）。
4. 不適切な仕様のリフティング（Improper specification lifting）（抽象的な充足から具体的な充足への論理的含意の保持の失敗）。

これらの問題は、抽象モデルが仕様に違反しているものの、実際の具体的なシステムは仕様を満たしているという「偽の（spurious）」反例を引き起こし、検証を無意味にする原因となります。

手法

本論文は、保守的な離散抽象化を構築するための4ステップのモジュール式ワークフローを提案しています。このワークフローは「構成による保守性（conservative-by-construction）」を備えており、特定の数学的保証を通じて、各段階で健全性が維持されます。

ステップ1：状態空間の抽象化

連続的な状態空間 $X$ を、一様かつ直交する格子を用いて、有限個の抽象状態 $\hat{X}$ に分割します。量子化関数 $\psi: X \to \hat{X}$ は、具体的な状態を抽象的なセルへとマッピングします。逆写像 $\Psi(\hat{x})$ は、各抽象状態の具体的な領域（前像）を定義します。このステップにより、すべての具体的な状態および初期条件が、抽象モデルにおける代表を持つことが保証されます。

ステップ2：保守的な遷移の構築

本論文では、すべての具体的な遷移が抽象モデル内に表現されることを保証しながら、遷移関係 $\hat{f}$（どの抽象状態が次に続くかを決定すること）を計算するための、互換性のある3つの手法を提示しています。

• 軸平行境界ボックス（AABB）： 具体的なセルの像（image）の境界ボックスを計算します。このボックスと交差するすべての抽象セルが後続状態として追加されます。これは計算効率が高いですが、非線形システムに対しては過度に保守的になる可能性があります。
• ポリトープ伝搬（Polytope Propagation）： 具体的なセルの像を過剰近似するために、ポリトープ（凸包）を使用します。非線形ダイナミクスに対してAABBよりもタイトな近似が可能ですが、計算コストは高くなります。これは、高価なポリトープ交差テストを実行する前に、候補を絞り込むためのAABBカリングを採用しています。
• PAC証明を用いたサンプリング： ブラックボックス型または高度に非線形なシステムの場合、状態空間をサンプリングすることで遷移を探索します。決定論的な保証の代わりに、この手法は**おそらく正しく近似できる（Probably Approximately Correct: PAC）**保証を提供します。これは、構築された遷移関係が、高い信頼度（$1-\delta$）で、すべての「重要な」遷移（発生確率が $\ge \beta$ の遷移）を含んでいることを証明し、観測されていない遷移の「欠落した質量」を限定します。

ステップ3：退化的な振る舞いの緩和

保守的な抽象化は、しばวะとして偽の遷移（spurious transitions）（具体的なシステムでは不可能な遷移）や自己ループ（self-loops）（状態から自分自身への遷移）を導入します。これらは、特にライブネス特性の検証において、偽の否定（false negatives）を引き起こす可能性があります。

• 偽の遷移： **反例誘導型抽象化洗練（Counterexample-Guided Abstraction Refinement: CEGAR）**によって対処します。抽象モデルで反例の軌跡が見つかった場合、アルゴリズムはその軌跡を具体的なダイナミクスに対して検証します。その軌跡が偽である場合（到達可能集合が空になる場合）、状態空間を細分化（分割）して、その偽の遷移を排除します。
• 自己ループ： **認証付き自己ループ消去（Certified Self-Loop Erasure）**によって対処します。自己ループは、すべての具体的な軌跡が有限ステップ（$K$）以内にそのセルから脱出することが証明できる場合にのみ削除されます。これは、到達可能集合の伝搬の反復、またはPAC保証を用いたサンプリング戦略によって検証されます。

ステップ4：LTL仕様の健全なリフティング

具体的な空間上で定義された線形時相論理（LTL）の仕様 $\phi$ を、抽象的な仕様 $\hat{\phi}$ へとリフトする必要があります。本論文では、may-must意味論を採用しています。

• Must述語： ある原子命題が抽象状態において成立するのは、そのセル内のすべての具体的な状態において成立する場合のみです。
• May述語： ある原子命題が、そのセル内の少なくとも一つの具体的な状態において成立する場合に成立します。
  リフティング演算子 $\rho$ は、$\hat{s} \models \hat{\phi} \implies s \models \phi$ を保証するように、原子命題を「must」へ強化するか、あるいは論理構造に応じて「may」へと弱めることで、$\phi$ を $\hat{\phi}$ へと変換します。

主な貢献

1. 実用的なワークフロー： 状態分割、遷移構築、退化的な振る舞いの緩和、および仕様のリフティングを、単一の健全なフレームワークへと統合した、統一された4ステップのパイプラインを提供します。
2. 互換性のあるサブルーチン： 本手法は、遷移構築（AABB、ポリトープ、サンプリング）および退化的な振る舞いの除去（CEGAR、認証付き消去）に対する複数のアプローチをサポートしており、ユーザーが計算コストと抽象化のタイトさのバランスを選択できるようにしています。
3. サンプリングのためのPAC保証： 解析的な過剰近似が困難なシステムに対して、厳密な確率的被覆証明（Good-Turing推定量およびMcAllester-Schapire境界を介して）を提供する、データ駆動型のアプローチを導入しています。
4. 退化性の体系的な処理： 認証付き消去とCEGARを通じて、偽の自己ループや遷移の除去に明示的に対処し、保守的な抽象化に特有の悲観主義を防止します。

実験結果

著者らは、合成線形システム、Mountain Carベンチマーク（非線形、学習済みポリシー）、およびAutonomous Unicycle（Dubinsモデル）の3つのケーススタディでパイプラインを評価しました。

• 遷移構築： サンプリングベースの手法は、特に非線形システムにおいて、AABBおよびポリトープ手法と比較して、より疎な遷移関係、より少ない自己ループ、およびより低い後続状態数の変動を実現しました。これにより、検証における真陽性率（TPR）の向上が見られました。
• 自己ループ消去： 自己ループの除去は、検証結果を大幅に改善しました。Unicycleのケースでは、消去後にTPRは約0.19から約0.63に上昇しました。Mountain Carのケースでは、TPRは約0.83から0.93に向上しました。
• CEGAR： CEGARはモデルサイズと構築時間を大幅に増加させましたが、自己ループの割合（SLP）を一貫して減少させました。Mountain Carシステムに対して顕著なTPRの向上をもたらしましたが、Unicycleにおいては、ターゲットを絞った消去なしでは排除困難な些細な反例に起因する高いSLPがあったため、影響は限定的でした。
• 粒度： 状態空間の粒度を細かくするほど、一貫してTPRが高まり、モデルサイズと検証精度のトレードオフが確認されました。

意義

本論文は、CPSの抽象化を構築するエンジニアや研究者のための実用的なガイドとしての意義を主張しています。以下の点を通じて、理論的な抽象化技術と実用的な実装との間の溝を埋めています。

• 誤った検証（不健全な検証）を招く一般的なエラーを防ぐ、**構成による健全性（sound-by-construction）**を備えたワークフローを提供すること。
• システムの複雑さや利用可能な計算リソースに基づいて、決定論的手法（AABB/ポリトープ）と確率的手法（サンプリング）を選択できるモジュール式のツールを提供すること。
• 退化的な振る舞い（偽の遷移や自己ループ）の緩和が、単なる最適化ではなく、特にライブネス特性において意味のある検証結果を得るための不可欠なステップであることを実証したこと。

著者らは、記号的モデル検査は強力であるが、その有用性は抽象化の質に完全に依存すると結論付けています。このワークフローは、悲観主義と計算可能性のバランスを取りながら、その品質を達成するための厳格で適応可能なフレームワークを提供します。