技術的概要：iSMC – 対話的証明を備えた BDD ベースの記号モデルチェッカー

1. 問題定義

モデルチェッキングは、ハードウェアおよびソフトウェアシステムの正しさを検証するための基本的な技術である。しかし、モデルチェッカー自体の信頼性を保証することは、重要な課題である。従来の証明パラダイムは、非対話型プロトコルに依存している：証明者（モデルチェッカー）が証明書（例えば、充足割り当てや解決証明）を生成し、検証者がそれを独立して検証する。

本論文は、このアプローチにおける根本的な理論的限界を特定している：一般的な CTL モデルチェッキングを含む多くの問題において、証明書はインスタンスのサイズに対して最悪の場合、指数関数的な長さを持つ可能性がある。その結果、検証者はそれらを検証するために指数時間が必要となり、$NP = coNP$ でない限り、大規模システムに対する証明プロセスは非現実的となる。

著者らは、対話的証明を提案する。これは、証明者と検証者が多ラウンドのプロトコルに従事する対話証明システム（IP）に基づくパラダイムである。検証者は適応的に質問を行うことで、背後にある計算が複雑であっても、多項式時間で高い確率で誤りを検出できる。PSPACE 問題（CTL モデルチェッキングなど）に対する対話的証明は理論的に確立されている（Shamir の $IP=PSPACE$）が、バイナリ決定図（BDD）を用いた記号モデルチェッキングに対してこれを実用的にすることは、依然として未解決の課題であった。

2. 手法

本論文は、正義（justice）要件を伴う CTL モデルチェッキングに対して対話的証明を実装した、初の自己証明型モデルチェッカーiSMCを提示する。このシステムは、3 つの中核モジュールに基づいて構築されている。

2.1 アーキテクチャ

• ソルバー: CTL 仕様を満たす到達可能状態の集合を計算する、記号的 BDD ベースのモデルチェッカー。これはフラット化されたブールモデル（SMV 形式）で動作し、clic BDD ライブラリを使用する。
• 証明者: ソルバーと同じマシン上で実行される。モデルチェッキングインスタンスを実行し、計算中に生成された BDD ライブラリ呼び出しとアサーションのシーケンスからなる実行トレースを生成する。
• 検証者: 限られたリソースを持つクライアント上で実行可能な軽量モジュール。モデルチェッキングアルゴリズムを再実行するのではなく、証明者と対話型プロトコルに従事して実行トレースを検証する。

2.2 TraceCert プロトコル

中核的な革新は、Couillard ら [11] の QBF 証明に関する研究から適応された対話証明プロトコルTraceCertである。

1. トレースから回路へ: 実行トレースは**汎用ブール回路（GBC）**に変換される。トレース内の各命令はゲートとなり、アサーション（例えば、「状態集合 $C_1$ は $C_0$ と等価ではない」）は等価性主張となる。
2. 算術化: ブール関数は、有限体 $\mathbb{F}_p$ 上の多変数多項式として符号化される。これにより、検証者は回路全体をトラバースするのではなく、ランダムな点で多項式を評価することで計算の性質を検証できる。
3. 次数削減: 多項式が低次数を持つことを保証し（多項式時間検証に必要）、プロトコルは次数削減ゲート（$\delta_x$）を導入する。これは、ブール入力における関数の値を変えずに指数を 1 に削減する。
4. 対話ラウンド: プロトコルは回路をトラバースしながらラウンドごとに進行する。証明者はゲートの値を主張し、検証者はそのゲートへの入力に対するランダムな割り当てで証明者に挑戦する。証明者は主張と整合する多項式を提供しなければならない。証明者が嘘をついた場合、検出される確率は Schwartz-Zippel 補題によって制限される。

2.3 先行研究に対する主要な技術的改善

著者らは、QBF に焦点を当てた [11] の技術を、CTL モデルチェッキングの特定のニーズに対応するように拡張し、3 つの主要なボトルネックに対処した。

1. 効率的な名前変更と等価性: 元のプロトコル（CPCertify）は、等価性と名前変更ゲートを非効率的に処理していた（それぞれ $O(n^2)$ および $O(n^k)$）。TraceCert はこれらのラウンドをそれぞれ $O(1)$ および $O(n)$ に最適化する。
2. ガベージコレクションとの互換性: 標準的な BDD ライブラリは、グローバル計算キャッシュとガベージコレクションを使用する。従来のアプローチでは、証明者がすべての中間 BDD を保存する必要があり、ガベージコレクションを妨げていた。著者らは、証明者が過去の挑戦を悪意を持って記憶しない限り、健全性を損なうことなく中間結果（オラクルとして機能）を破棄できる、プロトコルのボトムアップ変種であるTraceCertRevを導入する。
3. グローバル計算キャッシュ: 従来の実装（blic）は、キャッシュと互換性のない方法で拡張 BDD（eBDD）を操作していたため、グローバルキャッシュを使用できなかった。著者らは、リンクフィールドを使用してノードのバージョン管理を行う新しい不変な eBDD 表現を導入し、グローバルユニークテーブルの使用を可能にし、パフォーマンスを大幅に向上させた。

3. 主要な貢献

1. iSMC システム: 正義要件を伴う任意の CTL 特性に対する対話的証明を備えた、初の自己証明型モデルチェッカーの実装。
2. TraceCert プロトコル: モデルチェッキングトレースで一般的に変数名変更や等価性アサーションを効率的に処理する新しい対話証明プロトコル。特定のゲートラウンドの複雑さを削減する。
3. 最適化された eBDD 実装: グローバル計算キャッシュとガベージコレクションの使用を可能にする新しいアルゴリズム（ApplyEBDD）とデータ構造。以前の blic ライブラリの非効率性を克服する。
4. TraceCertRev: 証明中にガベージコレクションを可能にするプロトコル変種。メモリが制約となる大規模モデルチェッキングにおいて、システムを実用的にする。

4. 実験結果

著者らは、HWMCC'25 のライブネストラックから 53 のベンチマークを用いて iSMC を評価した。

• ソルバーのパフォーマンス: 成熟したツール NuSMV と比較して、iSMC のソルバーは平均して5.84 倍遅い。著者らは、これを主に現在のプロトタイプにおける関係積（BDD 最適化）のサポート欠如に起因すると特定している。なぜなら、それらを対話的に証明することは依然として未解決の問題だからである。
• 証明者のオーバーヘッド: 証明者はソルバーの時間 $S$ に対して $O(S)$ の時間で実行される。定数係数は約2.00であり、証明のオーバーヘッドは解決時間の約 2 倍であることを意味する。
• 検証者の効率性: 検証者は非常に効率的である。証明者に 15 分のタイムアウトを設定した場合、検証者の実行時間は3.6 秒を超えることはなく（証明者に対する平均 33.4 倍の高速化）、検証者の実行時間は計算時間ではなく、実行トレースの長さに対して線形にスケーリングする。
• 最適化の影響: 改善（TraceCert、clic ライブラリ、グローバルキャッシュ）により、CPCertify と blic を使用したベースライン実装と比較して、実行時間が平均2.26 倍高速化し、メモリ使用量が16.12 倍削減された。

5. 意義と主張

本論文は、iSMC がモデルチェッキングに対する実用的な対話的証明への重要な一歩であると主張している。

• 信頼できないサーバーへの信頼: このシステムは、リソースが限られたクライアントが、強力だが信頼できないサーバーにモデルチェッキングを委任できるシナリオを可能にする。サーバー（ソルバー＋証明者）が重い計算を実行し、クライアント（検証者）が多項式時間で高い確率で結果を証明する。
• 多項式検証: 一般的な CTL 特性に対して指数時間を必要とする非対話型証明方法とは異なり、iSMC の検証者は変数の数とトレースの長さに対して多項式時間で実行される。
• スケーラビリティ: 著者らは、最適化により、対話的証明のオーバーヘッドは管理可能であり、メモリフットプリントが大幅に削減されることを実証した。これにより、非自明なベンチマークに対してこのアプローチが実行可能となった。

著者らは謙虚であり、iSMC は最初のプロトタイプであると指摘している。ソルバーは、関係積などの最適化が欠如しているため、NuSMV などの最先端ツールよりも現在遅く、また現在の実装は CTL を対象としているが、基盤となるフレームワークは理論的には完全なモダリティ $\mu$ 計算論へ拡張可能であると認めている。