1992 SMV 符號模型檢測：百萬狀態的無聲審訊#

案件編號：1992-SMV。報案人：Clarke、Emerson 的模型檢測學派。案情：顯式狀態列舉至多數千狀態就爆炸，真正的硬體卻有百萬狀態。破案者：Burch、Clarke、McMillan。

案發現場#

1981 年，Clarke 與 Emerson、Sifakis 各自提出了模型檢測（Model Checking）：把程式看成 Kripke 結構，把規格寫成時序邏輯，讓機器窮舉所有狀態，自動回答「系統是否滿足規格」。

理想很美，現實很冷。顯式列舉的模型檢查器只能處理約 \(10^3\) 到 \(10^4\) 個狀態。一個 20 個布林變數的電路就有 \(2^{20}\) 個狀態，約一百萬；真正的處理器管線、匯流排仲裁器，狀態數輕易超過 \(10^{10}\) 。工程師稱之為「狀態爆炸」。

1980 年代末的 Intel 與 IBM 驗證團隊深受其苦。模擬（simulation）只能測到你想到的向量，沒測到的角落就藏著 Pentium 級別的 bug。形式驗證若不能突破規模，就只能留在論文裡。

案發現場留下三件證物：

一張 Kripke 結構圖，節點多到無法畫下。
一本 CTL 手冊，滿是 \(EX\) 、 \(EG\) 、 \(EU\) 算子。
一句抱怨：「我們不是缺邏輯，我們是缺表示法。」

偵探登場：卡內基梅隆的 Burch、Clarke，與博士生 McMillan。他們盯上的不是新邏輯，而是新的「證物袋」—— OBDD。

偵查過程（含數學式/表格/理論）#

線索一：BDD 把布林函數壓成有向無環圖#

Bryant 在 1986 年證明：給定變數序，有序二元決策圖（OBDD）在化簡後是典範表示。兩個等價的布林函數，對應同一張圖；等價檢查變成指標比較。

一個集合 \(S\) 的特徵函數 \(\chi_S\) 、一個轉移關係 \(R\) ，都可以寫成布林函數，再壓成 BDD。百萬狀態的集合，有時只需數百個 BDD 節點。

表示法	表示對象	規模	操作
顯式列舉	單個狀態	\(O(\\|S\\|)\) 節點	DFS/BFS
符號表示	狀態集合 \(\chi_S\)	\(O(BDD 節點數)\)	邏輯運算
符號轉移	關係 \(R(x,x')\)	\(O(BDD 節點數)\)	存在量化

關鍵 BDD 操作都是多項式或實務高效：交集是 \(And\) ，聯集是 \(Or\) ，求補是 \(Not\) ，求後繼是存在量化加變數替換。

線索二：CTL 符號不動點演算法#

McMillan 的洞見是：CTL 模型檢測可以全部翻譯成集合操作，不必看見單個狀態。

設 Kripke 結構為 \(M = (S, R, L)\) ， \(S\) 為狀態集， \(R\) 為轉移關係， \(L\) 為標記函數。CTL 公式 \(\phi\) 的滿足集記為 \([\![\phi]\!]\) 。

\[ [\![EX \, \phi]\!] = Pre([\![\phi]\!]) \]

\[ Pre(X) = \{ s \mid \exists s' : R(s,s') \land s' \in X \} \]

\[ [\![EG \, \phi]\!] = \nu Z . ([\![\phi]\!] \cap Pre(Z)) \]

\[ [\![E[\phi_1 U \phi_2]]\!] = \mu Z . ([\![\phi_2]\!] \cup ([\![\phi_1]\!] \cap Pre(Z))) \]

其中 \(\nu\) 為最大不動點， \(\mu\) 為最小不動點。偵查筆記：在 BDD 上， \(Pre\) 就是一次「關係乘積加存在量化」：

\[ Pre(X)(x) = \exists x' : R(x,x') \land X(x') \]

從千到百萬的飛躍就藏在這裡：每次迭代操作的不是狀態，而是整片狀態集合的 BDD。10 次迭代就可能掃過 \(2^{20}\) 個狀態。

線索三：SMV 語言與 1992 年的引爆點#

McMillan 在 1992 年博士論文與 SMV 系統中，把上述理論變成可用的語言。SMV 允許以模組、分層、同步/非同步組合描述硬體，規格直接寫 CTL。

偵查重點整理：

Burch、Clarke、McMillan 1990 年論文先證明符號 CTL 可行。
McMillan 1992 年 SMV 把變數序啟發式、模型劃分、快取計算全部工程化。
驗證規模從約 \(10^3\) 跳到 \(10^6\) 甚至 \(10^{20}\) （視 BDD 壓縮率而定）。
同期 McMillan 亦提出符號 LTL 與插值方向，為後來 BMC 鋪路。

表格：SMV 前後對比。

年代	工具	方法	可處理狀態數
1982	EMC	顯式 CTL	約 \(10^3\)
1987	Cospan	語言包含	約 \(10^4\)
1992	SMV	BDD 符號 CTL	\(10^6\) 以上
1999	Cadence SMV	BDD + 組合抽象	工業級電路

結案報告#

案件告破。SMV 證明：狀態爆炸不是死刑，只是表示法選錯了。BDD 讓集合運算一次處理百萬狀態，CTL 不動點讓規格檢查變成純符號計算。

遺產有三：

Intel、IBM、Motorola 紛紛採用符號模型檢測，驗證快取一致性協定、匯流排仲裁、浮點除法器。Pentium FDIV 事件之後，Intel 更把形式驗證列為標準流程。
SMV 分化出 NuSMV、Cadence SMV，成為教學與工業界標準教材。
當 BDD 遇到乘法器等難例而爆炸時，學界轉向 SAT-based BMC 與 CEGAR，但「符號化」思想從未離開。

從因果鏈看，1981 模型檢測是報案，1992 SMV 是第一次大規模破案，1999 TLA+ 與 TLC、2001 Chaff、2008 Z3 都是它的共犯與繼承者。

證據與工具#

證據 A：CTL 符號演算法骨架（虛擬碼）。

function CheckEG(phi):
    Z := AllStates
    loop:
        Z' := Sat(phi) ∩ Pre(Z)
        if Z' == Z: return Z
        Z := Z'

證據 B：BDD 變數序的教訓。好的變數序讓 BDD 只有 \(O(n)\) 節點，壞的變數序讓同一函數爆成 \(O(2^n)\) 。SMV 使用者第一課就是：相關的現態與次態變數要交錯排列。

證據 C：SMV 範例（互斥協定片段）。

MODULE main
VAR
  turn : boolean;
  p0 : process cell(0);
  p1 : process cell(1);
SPEC AG !(p0.st = crit & p1.st = crit)

證據 D：延伸閱讀。Burch、Clarke、McMillan 1990 年〈Symbolic Model Checking: \(10^{20}\) States and Beyond〉；McMillan 1993 年專書《Symbolic Model Checking》；Bryant 1986 年 OBDD 論文。