Bounded Model Checkingとは何か｜探索範囲を有限に固定する

Bounded Model Checking（BMC／有界モデル検査）とは、未来を無限に調べるのではなく、先の k ステップまでに区切って、『まずい状態にたどり着く道があるか』を調べる手法である。全部の未来について安全だ、とは言わない。区切った範囲の内側だけを見る。

もともと何に使われたか

BMCが適用されるシーンは、ハードウェアやプロトコル、組込みソフトの形式検証である。設計が「起きてはならない状態」へ到達し得るかを、有限深さ k で検査する。

系譜として、Armin Biere（アルミン・ビーレ）、Alessandro Cimatti（アレッサンドロ・チマッティ）、Edmund M. Clarke（エドムンド・M・クラーク、1945–2020）、Yunshan Zhu（ユンシャン・ジュ）らの有界モデル検査（1990年代末）がある。遷移関係を深さ k まで展開し、反例探索を SAT（Boolean Satisfiability Problem／ブール充足可能性問題）へ落とす流れが、実務のSATソルバと接続した。

従来のモデル検査は、状態空間をなるべく広く覆って性質を証明しようとした。状態数が爆発すると、証明も反例探索も止まる。BMCは方針を変える。無限の安全証明を一旦諦め、深さ k までのバグ（反例）を先に見つける。k 内に反例があれば設計の欠陥として直す。無ければ「少なくとも深さ k までは見つからなかった」と記録し、必要なら k を上げて次ラウンドを開く。

調べ方は次である。いまの状態、次への移り方、起きてほしくない状態を条件として書き、その条件をすべて同時に満たす答えがあるかを問う。変数には真か偽（1か0）を入れ、一つでも満たす入れ方があれば「ある（SAT）」、どう入れても無理なら「無い（UNSAT）」。

例題：エレベータ制御のバグを深さ k で探す

コンピュテーションでの典型は、組込み制御や回路の安全条件を、短い手順のバグとして見つけることである。ここではエレベータの制御を、ドア・走行・階ボタンの変数3つだけで追う。

各ステップで、次の0/1を持つ。

破ってはならない性質（違反 B）は一つだけ置く。

• 違反 B：D=1 かつ M=1（ドアが開いたまま動く）

設計者が意図した遷移は次である。

1. 停止中（M=0）だけドアを開けられる
2. ドアが閉じたあとだけ発車できる（D=0 のときだけ M を1にできる）
3. 階ボタン R=1 なら、停止してドアを開ける方向へ進む

バグ入りの実装では、「ドア閉完了の確認」を飛ばして発車できる、とする。BMCの問いを Bound k=3 で置く。

初期は D=0, M=0, R=0。3ステップ以内に、D=1 かつ M=1 へ到達する入力列があるか。

マトリックスを作ると、次の反例経路が出る。

BMCが返すのは「深さ3以内に反例がある（SAT）」と、上のような0/1の列である。設計者はステップ3の遷移条件を直し、「D=1 のときは M を立てられない」をreject条件としてコードへ戻す。

同じ問いで k=1 なら、開始から1ステップでは D=M=1 に届かないので UNSAT になりやすい。深さによって見えるバグが違う。全期間の安全証明ではない。

回路でも同じ型である。たとえば req（要求）と ack（応答）の握手回路で、「ack=1 なのに req=0」を違反 B と置き、深さ k まで展開してSATに落とす。チップ設計や自動車のECU検証でBMCが使われるときの骨格は、この「短い手順の反例探し」である。

上の表は、手順を追えるように変数を3つに絞った例である。実機の制御では、センサー、タイマ、割り込み、複数のかごなどが加わり、調べる状態の組合せが急に増える。未来をどこまでも調べ尽くすのは現実的でない。そこで先に「何ステップ先まで見るか」を Bound k として決め、その範囲に違反へ至る道があるかだけをSATで調べる。

BMCが解く問い

BMCは次を同時に満たす割当を探す。

1. 初期状態 I(s₀) が成立する
2. 各ステップで遷移関係 T(sᵢ, sᵢ₊₁) が成立する
3. どこかの深さ i ≤ k で違反条件 B(sᵢ) が成立する

SATソルバ（充足可能性を解くプログラム）の出力は、次のように読む。

UNSATは「いま置いた境界の内側では見つからなかった」という情報である。BMCの価値は無限探索の代替ではなく、探索範囲を有限に固定して検証可能にすることにある。

なぜ有限境界が必要か

回路や並行プロセスの状態空間は、ビット幅とプロセス数の積で容易に爆発する。全状態を列挙して最適に近い検証を続けることは、多くの場合現実的でない。

BMCが返すのは、目的関数の最適値ではない。有限の探索境界を置き、充足条件へ至る道があるかを先に見える化する。反例が見つかれば直す。見つからなければ k を上げるか、別の性質へ移る。プロセスの完全性を証明するのではなく、おおよそのプロセスに重大な欠陥がないことを検証する。

経営へ応用するなら

先に「破れば棄却する条件（reject）」と「どこまで見るか（Bound k）」を宣言し、その内側で破綻経路を探す。

違反条件 B の例は次である。

• 現金残高が下限を下回る
• 法令・安全基準を破る
• 品質の必須条件を満たさない
• 顧客への約束と在庫の不一致

BMCは、これらの違反が Bound 内に到達する経路があるかを問う。経路が見つかれば、どの決定の列が原因かを追跡できる。見つからなければ、少なくともその Bound 内では違反経路が無い。

FMEA（Failure Mode and Effects Analysis／故障モード影響解析）と構造が近い。故障モードを違反条件 B として定義し、直近の k ステップで下限を下回るかを検査する。k 内に反例が無いことは全期間の安全証明ではない。有限境界付きの耐故障設計である。

SATソルバ実行の位置づけ

BMC単体では、反例の有無しか分からない。実務では次の手続と接続する。

1. BMCで Bound を固定する
2. 候補を実行し、破れば棄却する条件（reject）との Conflict を記録する
3. CDCL（Conflict-Driven Clause Learning／衝突駆動型節学習。失敗を再訪禁止の短い条件へ変換する手続）で Conflict を学習節へ変換する
4. reject条件を守り、充足条件が受入閾値へ達したら停止する

この停止は系全体の終了ではない。局所探索ラウンドの終了である。上限までに達しなければ、そのラウンドをUNSATまたは未決として閉じ、性質・制約・Boundのどれを変更するかを外部主体が決める。

reject条件と充足条件を分けてからBoundを置く

BMCの前に、破れば棄却する条件と、足りれば採用する条件を分ける。

「99%なら常に十分」という普遍閾値は存在しない。何をrejectとし、どの重みと充足水準で止めるかを外部主体が宣言する。Boundだけを先に決めてreject条件を曖昧にすると、SAT/UNSATの解釈が崩れる。

よくある誤解

実行チェックリスト

1. Bound k を計算開始前に固定したか
2. 初期状態、遷移、違反条件を明示したか
3. reject条件と充足条件を分けたか
4. SAT/UNSATの読み方を事前に合意したか
5. Bound変更時に新しいラウンドとして記録したか
6. 局所探索の停止条件を採用・UNSAT・未決・再起動のいずれかで閉じられるか

BMCの有効性は、「すべてをチェックすれば安全になる」ではなく、「最低限をチェックすれば大局的には問題がない」下界の特定である。有限資源を前提にして求める結果を出すために、検証可能な有限境界を置き、その内側で反例を探し、見つからなければ境界付きの知見として次のプロセスで枝切りして探索範囲を削減することも手順の一つである。もともと回路とプロトコルのバグ探しのために生まれた手続を、事業の充足条件の到達検査に活用すると役に立つ。

『P vs NP経営』の詳細はこちら https://link.amazon/B04IEdYsn