技術要約：ベクトルの区間を用いた記号的モデル検査

1. 問題提起

モデル検査は、ソフトウェアやハードウェアシステムが仕様に従っていることを保証するための、堅牢な形式検証技術である。しかし、これは状態爆発問題、すなわちシステムの規模とともに可能な状態数と遷移数が指数関数的に増加するという問題によって、深刻に阻害されている。この課題は、単一の構成を検証するのではなく、計算樹論理（CTL）式を満たすすべての状態を特定することを目的とするグローバル・モデル検査において特に顕著である。

決定グラフ（DD）、抽象化、部分順序削減などの既存の手法は、この問題を軽減するが、モデルがより高度になるにつれて限界に直面する。具体的には、標準的な区間ベースのアプローチ（例：区間決定グラフ）は、ベクトルの集合を区間のベクトルとしてエンコードする。本論文は、ペトリネットに対しては、ベクトルの区間ではなく、ベクトルの一般化された区間（ベクトルの区間）を用いてマーキングの集合をエンコードする方が、より効果的なアプローチであると主張している。この区別は極めて重要である。なぜなら、ベクトル空間はしばしば非全順序の半順序を伴うため、単純な区間の定義では不十分だからである。

2. 手法

著者らは、ペトリネットのマーキングの集合をエンコードするために、**記号的ベクトル集合（Symbolic Vector Sets: SVS）**と呼ばれる新しい記号的構造を提案している。この手法は、以下の3つの柱に基づいている。

2.1. 記号的ベクトルと集合

記号的ベクトルは、$(a, b)$ というペアとして定義される。ここで、$a$ と $b$ はベクトルの集合（マーキング）である。

• 包含 ($a$): マクロキング $q$ が記号的ベクトルに含まれるとは、$q$ が $a$ に含まれるすべてのベクトルを含む（非厳密な部分順序 $\subseteq_f$ の下で）ことを指す。
• 除外 ($b$): マクロキング $q$ が記号的ベクトルに含まれないとは、$q$ が $b$ のいかなるベクトルも含まないことを指す。
• 一般化: これは自然数の区間 $[a, b]$ （$a \le x \le b$）をベクトルへと一般化したものである。ベクトルは必ずしも比較可能ではないため、この構造には単一の境界ではなく、下限の集合 ($a$) と上限の集合 ($b$) が必要となる。

記号的ベクトル集合は、これらの記号的ベクトルの集合であり、それらの基礎となるマーキングの集合の和集合を表す。

2.2. 標準形と演算

効率性を確保し冗長性を回避するために、著者らは記号的ベクトルおよび集合に対する**標準形（Canonical Form）**を定義している。主な特性は以下の通りである：

• 一意性: すべてのマーキングの集合は、正確に一つの標準的な表現を持つ。
• 準同型演算: 論文では、個々のマーキングにデコードすることなく、記号的構造上で直接作用する準同型演算（和集合、積集合、差集合、否定）を定義している。
• 結合可能性と共有可能性: 標準性を維持するために、著者らは、2つの記号的ベクトルがいつ結合可能か、あるいは「共有可能な」成分が存在するかを判断するための関係を導入している。これには、非全順序における曖昧さを解決するための辞書式全順序が含まれ、重複する制約を決定論的に扱うことを保証する。

2.3. ペトリネット上のCTLモデル検査

このフレームワークは、有限容量を持つペトリネットにこれらの構造を適用する。

• 前置演算 (Pre-Operation): グローバル・モデル検査の核心は、前置マーキングを計算する pre 演算である。著者らは、遷移の可逆性と容量制約を処理しながら、記号的ベクトル集合上で動作する記号的 pre 演算を定義している。
• 不動点評価: CTL式（例：$EF, EG, EU$）は、記号的ベクトル集合上の不動点計算（最小不動点および最大不動点）を用いて評価される。式の充足は、結果としての記号的ベクトル集合にマーキングが含まれるかどうかをチェックすることによって決定される。

2.4. 最適化

• 飽和 (Saturation): 不動点計算における中間解が不必要に大きくなる「ピーク効果」に対処するため、著者らは飽和戦略を実装している。これには、容量境界を反復し、後続のステップを計算するために以前の結果を活用することが含まれ、中間的な記号的ベクトルの数を大幅に削減する。
• クラスタリング: 論文では、到達可能性のための最適化として、小さなベクトルを結合するクラスタリングについても言及しているが、これは将来の形式的な記述のための概念として留められている。

3. 主な貢献

1. 新しいエンコーディング: ペトリネットのマーキングにおける非全順序を扱うために特別に設計された、区間をベクトルへと一般化した構造である記号的ベクトル集合の導入。
2. 形式的な標準化: 一意性の証明を含む、記号的ベクトルおよび集合のための厳密な標準形の定義、および標準性を保持する準同型演算（和集合、積集合、差集合、否定）の開発。
3. グローバル・モデル検査フレームワーク: これらの記号的構造を用いてペトリネット上のCTL式を評価するための完全な形式体系（記号的 pre 演算の定義を含む）。
4. 飽和アルゴリズム: 不動点反復中の計算ピークを緩和するために、記号的ベクトル集合の文脈に飽和原理を適応させたもの。
5. 実装 (SVSKit): 理論を実装したSwiftライブラリであり、Model Checking Contest (MCC) 2022のベンチマークを用いてテストされている。

4. 結果

著者らは、MCC 2022の例、特に**サーカディアン・クロック（Circadian Clock）**モデルを用いて、SVSKitツールによるアプローチを評価した。

• 飽和によるスケーラビリティ: サーカディアン・クロック・モデル（14プレイス、16トランジション）を用いた実験により、飽和が極めて重要であることが示された。飽和なしでは、計算時間はプレイス容量とともに指数関数的に増加した（容量6で5時間を超えた）。飽和を用いると、容量2以上に対して計算時間は一定（約3.2秒）に保たれ、記号的ベクトルの数も安定した。
• 大規模な状態空間の処理: 本ツールは、容量 $N=100,000$ までのケースを正常に処理し、約 $10^{84}$ 個のマーキングをわずか26個の記号的ベクトルとしてエンコードした。
• ベンチマーク性能: MCC 2022のCTLファイアビリティ（fireability）カテゴリにおいて、既存のツール（GreatSPN, ITS-Tools, Tapaal）は、60分間の制限時間内にすべての16個のクエリに回答できなかった（Tapaalは9/16を回答）。SVSKitのアプローチは、16個すべてのクエリを約30分で解決した。
• 限界: 著者らは、現在の実装が標準化演算の最悪計算量（$O(n!)$）に起因するスケーラビリティの課題に直面していることを認めている。効率性はこれらの演算の実装に大きく依存しており、ベンチマークにおけるツールは、これらの制約により比較的小さなペトリネットに限定されていた。

5. 意義と主張

本論文は、「ベクトルの区間」から「ベクトルの区間（intervals of vectors）」への移行により、既存の記号的モデル検査技術に対する有望な代替案を提示していると主張している。

• 理論的貢献: ベクトルの集合を半順序の下で操作するための形式的な代数的枠組みを提供し、これまで停滞していた（30年前の「述語構造」を参照）文献の空白を埋めるものである。
• 実用的な実行可能性: 実験結果は、このアプローチが明示的な列挙よりも大規模または無限の状態空間をより効率的に処理でき、特に容量が大きい特定のグローバル・モデル検査タスクにおいて、現在のツールを上回る可能性があることを示唆している。
• 今後の方向性: 著者らは控えめに、現在の実装には最適化（特に標準化演算）が必要であると述べている。また、今後の課題として、ローカル・モデル検査への拡張、モデルをペトリネット以外へ広げること、および本手法を決定グラフと統合すること（両者は直交しており、ハイブリッド化による恩恵を受けられる可能性がある）を挙げている。

結論として、現在の実装には限界があるものの、理論的基盤と初期の実験結果は、記号的ベクトル集合がグローバル・モデル検査に対して持つ潜在能力を裏付けている。