1981 年模型檢測誕生：窮舉狀態空間的瘋狂探案#
報案人：Edmund Clarke＋E. Allen Emerson（美國）與 Jean-Pierre Queille＋Joseph Sifakis（法國）。 涉案物：一張 CTL 運算子表，以及一個叫「狀態爆炸」的怪物。
案發現場#
1980 年左右，並行系統的驗證陷入僵局。 Pnueli 給了時序邏輯，卻沒給自動判定法； Hoare 邏輯遇到交錯執行就爆炸；測試只能抽查，不能窮舉。
Clarke 與 Emerson 在哈佛／卡內基梅隆，Queille 與 Sifakis 在格勒諾布爾， 兩組人馬在 1981 年不約而同報案：既然程式是有限狀態的， 何不把「所有可達狀態」全部展開，用演算法直接檢查時序公式？
這想法在當時被視為瘋狂：狀態數隨變元指數成長， 稍大的系統就有天文數字的狀態。但兩組人都認為： 與其相信測試，不如先把小的做對，再想辦法放大。
偵查過程#
線索一：CTL 運算子表——分支時間的語言#
Clarke-Emerson 採用分支時序邏輯 CTL。公式形如路徑量詞＋時態運算子：
| CTL 公式 | 讀法 | 含義 |
|---|---|---|
| \(EX \, \phi\) | 存在下一步 \(\phi\) | 某後繼滿足 \(\phi\) |
| \(AX \, \phi\) | 一切下一步 \(\phi\) | 所有後繼皆滿足 \(\phi\) |
| \(EF \, \phi\) | 存在終將 \(\phi\) | 某條路徑未來有 \(\phi\) |
| \(AF \, \phi\) | 一切終將 \(\phi\) | 每條路徑未來皆有 \(\phi\) |
| \(EG \, \phi\) | 存在永遠 \(\phi\) | 某條路徑恆滿足 \(\phi\) |
| \(AG \, \phi\) | 一切永遠 \(\phi\) | 每條路徑恆滿足 \(\phi\) |
| \(E[\phi \, U \, \psi]\) | 存在直到 | 某條路徑 \(\phi\) 直到 \(\psi\) |
| \(A[\phi \, U \, \psi]\) | 一切直到 | 每條路徑 \(\phi\) 直到 \(\psi\) |
Queille-Sifakis 的 CESAR 系統用類似的分支邏輯，精神一致： 狀態＋轉移＋時序公式＋窮舉檢查。
例子：互斥安全性寫為 \(AG(\neg (c_1 \land c_2))\) ， 無死鎖活性寫為 \(AG \, EF \, restart\) ，飢餓自由寫為 \(AG(req \to AF \, grant)\) 。
線索二：顯式狀態演算法——標記的藝術#
早期的模型檢測是顯式的：把 Kripke 結構 \(M = (S, R, L)\) 的每個狀態都存下來， 再對公式做由內而外的標記（labelling）。
以 \(EF \, \phi\) 為例：
- 先標出一切滿足 \(\phi\) 的狀態集 \(T_0\) 。
- 反覆加入一切有後繼在已標集合中的狀態： \(T_{i+1} = T_i \cup pre(T_i)\) 。
- 求最小不動點： \(EF \, \phi = \mu Z \, . \, \phi \lor EX \, Z\) 。
- 若初態皆被標記，則 \(M \models EF \, \phi\) 。
其他運算子的不動點刻畫：
時間複雜度為 \(O(|M| \times |\phi|)\) ，對公式是線性的，對模型是線性的。 聽起來很美，直到人們算出 \(|M|\) 有多大。
線索三：狀態爆炸——怪物現身#
偵探算了一筆帳： \(n\) 個布林變元就有 \(2^n\) 個狀態， 兩個各有 \(k\) 狀態的行程交錯就有 \(k^2\) 量級， 十個小元件的乘積輕易突破百萬。
| 系統規模 | 狀態數估計 |
|---|---|
| 10 個布林變元 | \(2^{10} = 1024\) |
| 30 個布林變元 | \(2^{30} \approx 10^9\) |
| 100 個變元 | \(2^{100}\) ，天文數字 |
| 真實 CPU 管線 | 遠超顯式列舉極限 |
1981 年的原型只能處理幾千狀態。怪物「狀態爆炸」在結案報告第一頁就被點名， 成為此後三十年模型檢測史的主敵。符號方法（BDD，1992）、 偏序化簡、抽象、SAT 求解，都是為獵殺它而發明的武器。
結案報告#
1981 年，Clarke-Emerson 的〈Design and Synthesis of Synchronization Skeletons〉 與 Queille-Sifakis 的 CESAR 論文同年問世，模型檢測正式誕生。
結案意義：
- 全自動驗證：給定 \(M\) 與 \(\phi\) ，機器自動回答是／否並給反例路徑，無需人類寫證明。
- 反例即證據：驗證失敗時吐出一條違反路徑，工程師可直接除錯，這是定理證明器當時做不到的。
- 狀態爆炸立Flag：明確指出comb explosion是核心瓶頸，為 1992 年 SMV＋BDD 的逆襲鋪路。
Clarke、Emerson、Sifakis 因此同獲 2007 年圖靈獎。瘋狂的窮舉，成了最務實的驗證。
證據與工具#
- CTL 八運算子見上表，核心差異是 \(A\) （一切路徑）對 \(E\) （存在路徑）。
- 不動點三式： \(EF\) 與 \(EU\) 取最小不動點 \(\mu\) ， \(EG\) 取最大不動點 \(\nu\) 。
- 顯式演算法虛擬碼：
label(phi):
if phi 為原子命題: return {s | phi ∈ L(s)}
if phi = EX ψ: return pre(label(ψ))
if phi = EF ψ: 迭代 pre 直到不動點
if phi = EG ψ: 反向消去非 EG 區
...
- 實驗：畫 4 狀態互斥協議圖，手算 \(AG(\neg(c_1 \land c_2))\) 的標記過程， 再故意植入一個可達的雙臨界區狀態，觀察演算法如何吐出反例路徑。
- 文獻：Clarke-Emerson 1981，Queille-Sifakis 1982，Clarke 等《Model Checking》。