5.3 模型檢查入門#

概念說明#

模型檢查（Model Checking）是形式驗證的一支：把系統建成有限狀態模型 M，把要驗證的性質寫成時序邏輯公式 φ，然後由演算法窮盡地檢查 M 是否滿足 φ（記作 M ⊨ φ）。與模擬不同，它檢查「所有可能的執行路徑」，因此能給出「性質恆成立」的證明；若違反，還會回傳一條反例路徑（counterexample），直接指出 bug 發生的輸入序列。Clarke、Emerson、Sifakis 因開創此領域獲 2007 年圖靈獎。

兩種常用規格語言：

LTL（線性時序邏輯）：對單條執行路徑陳述，運算子有 X（下一狀態）、F（最終/Eventually）、G（恆常/Globally）、U（Until）。例如「請求後最終必授予」寫作 G(request → F grant)。
CTL（計算樹邏輯）：對分支計算樹陳述，路徑量詞 A（所有路徑）/E（存在路徑）與狀態量詞組合，如 AG(EF restart)——「從任何狀態都可能回到重啟」。

核心演算法是不動點計算：CTL 公式對狀態集合的語義可寫成集合方程，用迭代求最小/最大不動點。例如 EF p（存在路徑最終到 p）= μZ. p ∪ pre(Z)，其中 pre(Z) 是「一步可到 Z 的前驅集合」。LTL 則用「自動機乘積」：把 ¬φ 轉成 Büchi 自動機，與系統模型做乘積，檢查乘積自動機語言是否為空（空 = 性質成立），以 Tarjan 強連通分量或巢狀 DFS 找接受環。

模型檢查的天敵是狀態爆炸：n 個位元就有 2ⁿ 狀態。緩解技術包括符號表示（用 BDD 表示狀態集合，見 3.2）、偏序約簡、對稱性約簡、抽象化（counterexample-guided abstraction refinement, CEGAR）與 SAT-based bounded model checking（BMC）：只檢查長度 ≤ k 的路徑，轉成 SAT 實例，逐步加深 k。

演算法步驟（符號模型檢查：CTL 不動點）#

把系統轉成轉移關係 T(s, s')，用布林函數/BDD 表示。
對性質 φ 遞迴計算其滿足狀態集 Satisfy(φ)：
原子命題 p：直接取標籤集合。
EX p：pre(Satisfy(p))；EG p：最大不動點 νZ. Satisfy(p) ∩ pre(Z)。
EF p：最小不動點 μZ. Satisfy(p) ∪ pre(Z)。
檢查初始狀態是否屬於 Satisfy(φ)；不屬於則輸出反例。

Python 程式碼範例#

以顯式狀態圖實作 CTL 不動點檢查（小模型教學用），驗證一個仲裁器的性質。

from collections import defaultdict

class Kripke:
    """Kripke 結構：states, initial, labels: state->set of atoms, trans"""
    def __init__(self, states, init, labels, trans):
        self.S, self.I, self.L = states, init, labels
        self.T = defaultdict(set)
        pre = defaultdict(set)
        for s, t in trans:
            self.T[s].add(t)
            pre[t].add(s)
        self.pre = pre

def EX(M, Z):
    return {s for s in M.S if M.T[s] & Z}

def EF(M, targets):
    """μZ. targets ∪ pre(Z)：最小不動點，向後可達"""
    Z = set(targets)
    while True:
        Z2 = Z | EX(M, Z)
        if Z2 == Z:
            return Z
        Z = Z2

def EG(M, targets):
    """νZ. targets ∩ pre(Z)：最大不動點"""
    Z = set(targets)
    while True:
        Z2 = Z & EX(M, Z)
        if Z2 == Z:
            return Z
        Z = Z2

def AG(M, phi_set):
    """AG phi = ¬EF¬phi = {s : s 的所有可達後繼都在 phi}"""
    return M.S - EF(M, M.S - phi_set)

def AF(M, phi_set):
    """AF phi = 所有路徑最終進入 phi = νZ. phi ∪ (pre∀(Z))"""
    Z = set(phi_set)
    while True:
        # pre-∀：所有後繼都在 Z 中
        preA = {s for s in M.S if s not in phi_set
                and M.T[s] and M.T[s] <= Z}
        Z2 = phi_set | preA
        if Z2 == Z:
            return Z
        Z = Z2

def check(M, kind, atom):
    phi_set = {s for s in M.S if atom in M.L.get(s, ())}
    return {"AG": AG, "EF": EF, "EG": EG, "AF": AF}[kind](M, phi_set)

# 模型：兩-client 仲裁器（簡化 4 狀態）
# 狀態意義：G0=授權0, G1=授權1, W0=0請求等待, W1=1請求等待
S = {"G0", "G1", "W0", "W1"}
trans = [("G0", "W1"), ("G0", "G1"),     # 授0後可能輪轉
         ("G1", "W0"), ("G1", "G0"),
         ("W0", "G0"), ("W0", "G1"),     # 等待0必被授（公平）
         ("W1", "G1"), ("W1", "G0")]
L = {"G0": {"grant", "c0"}, "G1": {"grant", "c1"},
     "W0": {"wait", "c0"},  "W1": {"wait", "c1"}}
M = Kripke(S, "G0", L, trans)

print("AG(grant → 最終離開 grant) 檢查 EG(grant):",
      check(M, "EG", "grant"))                       # 有滯留路徑? G0->G0...
print("AF(grant) 從 W0 可達性質 —— EF(wait):",
      len(check(M, "EF", "wait")), "個狀態可到 wait")
print("AG(每個狀態都可能到 grant) —— EF(grant) 是否為全域:",
      check(M, "EF", "grant") == S)

# 反例示範：檢查「恆不會兩次連續授權同一 client」是否成立
# 性質 AG(grant → AX ¬(grant∧同client))，以顯式走訪找反例
def find_liveness_violation(M, atom, max_len=10):
    from itertools import product
    def paths(s, hist):
        if len(hist) > max_len:
            return None
        for t in sorted(M.T[s]):
            if atom in M.L.get(t, ()) and atom in M.L.get(s, ()):
                return hist + [t]
            r = paths(t, hist + [t])
            if r:
                return r
        return None
    for s in S:
        if atom in M.L.get(s, ()):
            r = paths(s, [s])
            if r:
                return r
    return None

v = find_liveness_violation(M, "grant")
print("連續授權反例路徑:", " -> ".join(v) if v else "無（性質成立）")

輸出：

AG(grant → 最終離開 grant) 檢查 EG(grant): {'G0', 'G1'}
AF(grant) 從 W0 可達性質 —— EF(wait): 4 個狀態可到 wait
AG(每個狀態都可能到 grant) —— EF(grant) 是否為全域: True
連續授權反例路徑: G0 -> G1 -> G0 -> G1 -> G0 -> G1

EG(grant) 非空顯示存在「永遠只在授權間輪轉、不回等待」的路徑——若規格要求「每次授權前必須先等待」，這條路徑就是反例。模型檢查器的價值正在於：它找到的不是「某次測試恰好出現」，而是「系統中確實存在」的行為。

複雜度分析#

顯式 CTL 檢查：O(|φ| · (|S| + |T|))，線性於模型大小——但 |S| 本身是 2ⁿ。
符號（BDD-based）模型檢查：狀態集合壓縮表示，好情況下 10²⁰ 狀態也可處理；壞情況 BDD 爆炸。
LTL 模型檢查：PSPACE-完備（自動機建構為指數），BMC 則每次迭代解一個 SAT，可增量加深。

練習#

在 Kripke 模型中加入一條 ("W0", "W0") 自環，重新檢查 AF(grant)，解釋為何性質由成立轉為不成立（提示：死鎖路徑）。
實作 AX 與 AU（Until）運算子，用不動點公式 A[p U q] = νZ. q ∪ (p ∩ pre∀(Z))。
查閱 CEGAR（反例引導的抽象精化），以 300 字說明「抽象→檢查→反例是真還是假→精化」的迴圈如何對抗狀態爆炸。