技術要約：離散時間動的システムにおける Co-Büchi バリア証明書

問題定義

本論文は、離散時間動的システムに対して $\omega$-正則特性（特に、特定の状態集合（または領域）への訪問が有限回のみであることを証明する必要があるもの）を検証するという課題に取り組んでいる。従来の安全性検証は、システムが「決して」安全でない集合に進入しないことを保証するものである。しかし、多くの時相論理特性（Universal Co-Büchi オートマトンによって指定されるものや、Büchi オートマトンの補集合など）は、システムが受理状態を無限回訪問しないことを示す必要がある。

既存のアプローチには大きな限界がある：

1. 状態トリプレット・アプローチ： 従来のメソッド（Wongpiromsarn et al. など）は、バリア証明書を用いて状態トリプレットを「切断」することでオートマトンのパスを遮断する。これは有限語オートマトンや co-safe 言語には効果的であるが、一般的な無限語オートマトンに対しては保守的であり、合計の訪問回数が有限であっても、トレースが受理状態に2回を超えて到達するシステムを検証できない場合がある。
2. 有界合成の限界： 有界合成は、状態の訪問回数を制限することで LTL 仕様を安全性問題に変換するが、標準的な手法はオートマトンの展開（unfolding）を必要としたり、インクリメンタルな保証を欠く複雑な積構成を扱う必要があったりする。
3. 複雑性： 連続空間における従来のモデル検査は次元の呪いに苦しむ。また、既存の時相論理のためのバリア証明書手法は、特定のテンプレートに依存しているか、あるいは必要性の保証を欠いていることが多い。

核心となる問題は、完全な積システムやオートマトンの無限の展開を明示的に構築することなく、システムのトレースが特定の領域を限定された回数しか訪問しないことを証明する、関数的な過近似（証明書）を開発することである。

メソドロジー

著者らは、Co-Büchi バリア証明書 (CBBC) を提案している。これは、古典的なバリア証明書の一般化である。そのメソドロジーは、以下の概念的および計算的ステップに基づいている。

1. 概念的枠組み：有界訪問としての安全性

核となる洞察は、「領域への訪問が有限回である」ことは直接的な安全性特性ではないが、システムにカウンタを付加することで、それを安全性問題へと変換できるということである。

• 拡張システム： 元のシステム $S$ は、システムがターゲット領域 $X_{VF}$ に入るたびにインクリメントされるカウンタ $\ell$ を付加することで、概念的に拡張システム $S'$ へと変換される。
• 安全性の還元： $X_{VF}$ への訪問が有限回であることを証明することは、拡張システム $S'$ がカウンタが固定された境界 $k$ を超える状態に決して到達しないことを証明することと同等である。これにより、この問題は拡張された状態空間における標準的な安全性検証問題へと変換される。

2. CBBC の定義

Co-Büchi バリア証明書は、カウンタが $k$ を超えないことを保証する特定の条件を満たす関数 $B: X \times [0..k] \to \mathbb{R}$ である。

• 初期条件： すべての初期状態に対して $B(x, 0) \le 0$ である。
• 不安全条件： すべてのターゲット領域内の状態に対して $B(x, k) > 0$ である（これは、カウンタが $k$ の状態で領域に到達することが「不安全」であることを示す）。
• 帰納的ステップ：
  • システムが $X_{VF}$ にいない場合、$B$ の値は非増加でなければならない（カウンタは維持される）。
  • システムが $X_{VF}$ にいる場合、次のステップ（カウンタが増加した状態）での $B$ の値は、現在のステップに対して非増加でなければならない。

論文では、このような関数の存在が、システムが領域を最大 $k$ 回訪問するという条件に対して、オラクル仮定の下で十分かつ必要であることを証明している。

3. オートマタ理論的検証

Universal Co-Büchi オートマトン $A_{c,k}$ によって指定される特性を検証するために：

• システム $S$ はオートマトンと同期され、積システムを形成する。
• CBBC の「不安全」領域は、オートマトンが受理状態にある積状態として定義される。
• 検証アルゴリズムは、境界 $k$ を持つ CBBC を探索する。もし見つかれば、システムはその特性を満たす。見つからなければ、$k$ をインクリメントし、探索を繰り返す。これはインクリメンタルな検証アプローチを提供する。

4. 計算的アプローチ

論文では、CBBC を計算するための 2 つの手法を提示している。

1. 和の平方 (SOS) アプローチ： システムのダイナミクスと状態集合が半代数的（多項式不等式で定義される）であることを前提とする。バリア証明書の探索は、半正定値計画問題 (SDP) として定式化される。その複雑性は、状態空間の次元に対して多項式時間であり（固定された多項式次数テンプレートを想定）、境界 $k$ に対して線形である。
2. SMT ベースのアプローチ (CEGIS)： 反例誘導型帰納的合成 (Counterexample-Guided Inductive Synthesis) を使用する。状態空間から点をサンプリングし、CBBC の制約を線形実算術上の SMT クエリとしてエンコードし、有効な関数が見つかるかタイムアウトが発生するまで、反例を用いて候補となる証明書を反復的に洗練させる。

主な貢献

1. 新しい証明書の定義： カウンタ変数を証明書関数に直接組み込むことで、「有限回の訪問」特性を扱うために古典的なバリア証明書を一般化した、Co-Büchi バリア証明書 (CBBC) の導入。
2. 理論的保証： CBBC が有界訪問特性を検証するための十分条件であるだけでなく、必要条件でもあることを確立した。これは、既存の多くの時相検証手法よりも強い主張である。
3. 状態トリプレット・アプローチの一般化： 著者らは、CBBC アプローチが「状態トリプレット」アプローチを包含することを実証した。状態トリプレット法で検証可能なシステムは CBBC でも検証可能であることを構成的な証明によって示しているが、その逆は必ずしも真ではない（CBBC はトリプレット法では検証できないシステムも検証できる）。
4. インクリメンタルな検証戦略： 提案されたメソドロジーは、境界 $k$ に関するインクリメンタルな探索を可能にする。アルゴリズムは $k=0$ から開始し、証明書が見つからない場合にのみ $k$ を増加させることで、計算コストと検証能力の間の実用的なトレードオフを提供する。
5. 計算フレームワーク： SOS ベース（多項式システム用）および SMT ベース（一般的なシステム用）の両方のアルゴリズムによる、これらの証明書の合成。

結果とケーススタディ

論文は、以下の 3 つのケーススタディを通じて、このアプローチを検証している。

1. 室温モデル (状態トリプレットの失敗)： オートマトンのエッジ上にラベルが重複しているために（具体的には、繰り返されるラベルでパスを遮断できないため）、状態トリプレット・アプローチが失敗するシステム。CBBC アプローチは $k=4$ の証明書を正常に見つけ出し、以前の手法では決定不能であった箇所において、特性が保持されることを証明した。
2. 2D Van der Pol オシレータ： UCA に対して検証された非線形システム。SOS アプローチを用いることで、次数 6 の CBBC が $k=3$ で約 5 分で発見され、受理状態への訪問が最大 3 回であることを証明した。
3. 3D Kuramoto オシレータ： 三角関数ダイナミクス（テイラー展開により近似）を持つ高次元システム。次数 4 の CBBC が $k=2$ で約 20 分で発見され、特定の領域への有限回の訪問を検証した。

重要性と主張

本論文は、CBBC が離散時間動的システムにおける $\omega$-正則特性を検証するための、堅牢で抽象化フリーなフレームワークを提供すると主張している。その重要性は以下にある：

• 保守性の克服： 一般的な無限語オートマトンに対して、しばしば保守的すぎる「状態トリプレット」アプローチの限界に対処している。
• スケーラビリティ： 複雑な積オートマトンの明示的な構築を避け、関数的な過近似に依存することで、次元の呪いを緩和し、状態次元に対して多項式時間でスケールする。
• 必要性： 多くのヒューリスティックな手法とは異なり、本論文はこれらの証明書が「必要」であることを主張しており、システムが特性を満たすならば、理論的に CBBC が存在することを示唆している。

著者らは、CBBC は検証には効果的であるが、非決定性を扱う困難さや実現可能性問題における決定性オートマトンの必要性から、合成（コントローラ設計）への適用は依然として困難であると述べている。これらを今後の研究課題として、重み付き、確率的、およびタイミング付きオートマトンへの拡張とともに挙げている。