自動機、邏輯與模型檢驗

有限自動機的兩張臉

回到最早的第一階梯，一台 DFA 不過是個卑微的小裝置——一道閘門，或一台只記得自己當前狀態的販賣機。你曾用兩個狀態、每讀到一個 a 就翻轉一次，設計出辨認「偶數個 a 符號」的那台。它感覺像個玩具。整個這一階梯講的，正是那個玩具出人意料的「來世」：同一台自動機，骨子裡其實是一條寫在某套邏輯裡的句子，也是一份用來檢查系統是否「行為正確」的食譜。正是這兩種讀法，使自動機成為「驗證」背後那台沉默的主力——而驗證正是本篇最終要加冕的主題。

先看邏輯這張臉。一台 DFA 恰好接受某個正規語言中的字串；把那個語言想成是「所有滿足某種性質的字串」之集合。現在回想數學階梯裡那套帶量詞的邏輯。有一條乾淨而深刻的定理——大約於 1960 年由 Büchi、Elgot 與 Trakhtenbrot 所證——說正規語言恰恰就是你能在一套特定的字串邏輯（稱為單子二階邏輯）中寫出的那些性質。一個字串不過是一條由位置構成、貼了標籤的小小直線；這套邏輯讓你能說出諸如「存在位置 x 與 y，x 在 y 之前，且該處字母為 a」這樣的話，並且不只能對單一位置、還能對整個位置集合做量化。每一條這樣的句子都圈出一個正規語言，而每一個正規語言也都由某條這樣的句子圈出。

永遠運行的自動機：Büchi 自動機

這裡有個關卡，逼出了一個新想法。你至今遇見的每一台自動機，讀的都是一個有限字串，然後停在某個狀態。但我們最想驗證的東西卻永不停止：一套作業系統、一份網路協定、一台紅綠燈控制器、一具心臟節律器。它們的行為是一段無限的步驟序列——所謂的 omega 字（omega-word），一道永無盡頭的符號流，像「請求、等待、授予、請求、等待、授予……」這樣永遠下去。一台尋常的 DFA 無法裁判這種東西，因為沒有一個「最後的符號」可以讓你在那裡問「我們此刻在接受狀態嗎？」我們需要一台自動機，它對永不終止的運行有一個合情合理的接受概念。

解方是 Büchi 自動機，由 Julius Büchi 於 1962 年發明。在結構上，它看起來與一台 NFA 一模一樣——有狀態、一個起始狀態、轉移 delta(q, a) = ...，以及一組接受狀態。改變的只有接受規則，而它改變的方式近乎詩意。一段對無限輸入的運行會走過一個無限的狀態序列；Büchi 自動機接受這段運行，若它無窮多次經過某個接受狀態——也就是說，這段運行永遠一再回到某個接受狀態，無論你往多遠處看都是如此。「一次又一次、永遠地造訪那塊綠色地帶」，正是你用來表達活性（liveness）性質的方式，例如「每個請求終將被授予」。

BUCHI automaton for "a holds INFINITELY OFTEN"   (alphabet {a, b})

       loop on b                          loop on a
        +-----+                            +-----+
        |     v          a                 |     v
        |   ( q0 )  ------------->  (( q1 ))      |
        |     ^                        |   ^      |
        +-----+                        +---+------+
                                          b   (b sends q1 back to q0)

     q0   : have-NOT-just-seen-a    (NOT an accept state)
   (( q1)): just-saw-an-a           (accept state, drawn doubled)

   accept a run  <=>  it is in q1 infinitely often
                 <=>  the letter a appears infinitely often.

   stream  a b a b a b a b ...  -> visits q1 over and over   -> ACCEPT
   stream  a a a b b b b b ...  -> after the b's, stuck in q0 -> REJECT
           (only finitely many a's: q1 visited only finitely often)

一台兩狀態的 Büchi 自動機，恰好接受那些含有「無窮多個 a 字母」的無限串流。雙圈狀態 q1 是接受狀態；當一段運行永遠不斷回到 q1 時，它就被接受。「a b a b ...」一直在碰 q1；「a a a b b b ...」只碰了有限次，所以被拒絕。

兩個誠實的提醒，因為無限字打破了一些你信賴已久的習慣。第一：對於有限字串，確定型與非確定型有限自動機是等價的——早期階梯那道子集建構法能把任何 NFA 變成一台 DFA。但對於無限字，這份等價失效了：確定型 Büchi 自動機嚴格地比非確定型弱，要找回完整的力量需要更豐富的接受條件（Muller、Rabin、Streett、parity）。所以你曾倚靠的一條舒適定理，並沒能挺過向 omega 字的這一跳。第二：這裡的非確定性仍是那同一個數學裝置，不是隨機、也不是實體的猜測——一台 Büchi 自動機接受，若某段運行無窮多次造訪那塊綠色地帶，正是「只要任一分支成功」的規則，只不過拉長到了一段永無盡頭的運行上。

一套關於時間的邏輯，以及模型檢驗的迴圈

要驗證，你得先說清楚你想要什麼——而非正式的中文（「這系統絕不會死結」）對機器而言太滑溜了。標準答案是時序邏輯：在尋常邏輯之上加幾個新算子，它們談的是時間而非日期。最常用的口味是線性時序邏輯（LTL），它沿著一段運行的無限未來加入這些算子：G p 表示「全域地，從現在起每一刻 p 都成立」；F p 表示「終究，未來某一刻 p 成立」；X p 表示「下一步 p 成立」；而 p U q 表示「p 持續成立，直到 q 變真」。這四個小字眼讓你能俐落地陳述真實的需求。

看這些算子如何捕捉正確性的兩大家族。「兩個請求者絕不會同時被授予這道資源」是一條安全（safety）性質——壞事永不發生——讀作 G (not (grant1 and grant2))。「每個請求終將被授予」是一條活性（liveness）性質——好事不斷發生——讀作 G (request implies F grant)。注意，活性那條恰恰就是 Büchi 自動機生來要辨認的那種「無窮多次／終究」的形狀。這份吻合並非巧合：有一套機械的建構法，能把任何 LTL 公式變成一台 Büchi 自動機，恰好接受滿足它的那些無限運行。

現在是回報：模型檢驗，這項技術讓 Clarke、Emerson 與 Sifakis 贏得 2007 年的圖靈獎。你手上有兩樣材料。系統——一份晶片設計、一份協定、一台控制器——本身被建模成一台有限狀態機，一張由狀態與轉移構成的圖；它的無限行為就是穿過那張圖的那些無限運行，而這又不過是另一台 Büchi 自動機。規格則是你的時序邏輯性質，同樣被編譯成一台 Büchi 自動機。工具接著對這兩台自動機問一個機械性的問題，而答案要嘛是「正確」，要嘛是一個具體的反例——一段真實會打破規則的系統軌跡，工程師可以重播並除錯。

把系統建模成一台有限狀態機 M，它的無限運行恰好就是它隨時間推移的所有可能行為。
把需求寫成一條時序邏輯公式 phi，再把 phi 編譯成一台 Büchi 自動機，恰好接受滿足 phi 的那些運行。
把需求取否定：為「NOT phi」造一台 Büchi 自動機，恰好接受那些違反性質的壞運行。
取交集：把 M 與「壞運行」自動機作乘積——得到一台自動機，恰好接受那些「既是系統行為、又是違規」的行為。
問「空性」問題：這台乘積自動機接受任何無限運行嗎？空（接受不了任何運行）意味著沒有任何行為違反性質，所以系統正確；而任何被接受的運行，就是一段交回給工程師的反例軌跡。

描述複雜度：用邏輯量度難度

這個「邏輯等於自動機」的想法，還有一位更宏大的表親，它一路向上觸及前幾階梯的那些複雜度類別。描述複雜度提出一個驚人的問題：與其用「一台機器要花多久」來量度一個問題的難度，我們能不能用「你光是要描述它就需要多豐富的邏輯」來量度它？令人驚訝的是，答案往往是肯定的——計算的資源與邏輯的表達力恰好對齊，而其定義裡從頭到尾沒有提到任何圖靈機、任何時鐘，或任何磁帶。

奠基的結果是 Fagin 定理（1974）：NP 中的問題恰恰就是能在存在二階邏輯中表達的那些性質。回想 NP 是那一類拼圖問題——難以完成，但給了證書就易於檢查。Fagin 定理把那張證書重新詮釋為一個你能「量化使其存在」的邏輯物件：「存在一個關係（一種著色、一條巡迴、一組滿足賦值），使得這條一階條件成立」。舉例來說，NP 難的「圖的三著色」就變成「存在三個覆蓋整張圖的頂點集合，使得沒有任何一條邊連接同一集合中的兩個頂點」。那個「存在一個集合」就是二階量詞；其餘的是一條簡單的一階檢查——這正是 NP 的「證書加驗證者」圖像，以純邏輯重寫了一遍。

為何這正是早已在運轉世界的那套理論

退一步，看看一個卑微的想法已經把人帶到了多遠。同一台有限自動機，既是一道閘門、一條邏輯句子、一個無限行為的辨認器，也是一套驗證工具的引擎。正是這四重身分，使得這套理論的應用無處不在、且承重吃緊。每一個正規表示式引擎、每一個編譯器的詞法分析器、每一個協定模糊測試器，都奠基於有限自動機。而模型檢驗也不是個思想實驗：硬體公司用它來驗證快取一致性協定與浮點運算單元，NASA 曾把它用在太空船軟體上，而 SPIN 與 TLA+ 這類工具，在真實的分散式系統出貨前，就抓出過深藏其中的並行錯誤。

不過要對極限誠實，因為它們把本篇繫回了整條階梯。模型檢驗之所以可判定，恰恰是因為系統被建模成有限狀態的——正是這一點，使那次空性檢查不至於撞上你在兩階梯前遇見的那道不可判定的高牆。去驗證一個記憶體無上限的程式，或去問「任意兩個程式是否等價」，你就會一頭撞進不可判定性；那不是工具的缺口，而是一條定理。即便在有限的世界裡，仍有一道殘酷的代價：一個有 k 個布林變數的系統，狀態數可達 2^k，這就是惡名昭彰的狀態爆炸，所以一個對狀態圖而言是多項式的模型檢驗器，對程式碼本身而言仍可能是指數的。上述那些勝利，是靠著種種「不去建出整張圖」的巧妙手法贏來的——符號方法、抽象化、偏序歸約——而從不是靠逃離這套理論的硬邊界。

於是，這一階梯的諸般前沿，最終都成了你一再做過的同一個動作的變奏：取一個計算模型，恰好轉動一個旋鈕，看著「什麼可判定、什麼可表達、什麼有效率」的地貌隨之移動。隨機性給了我們 BPP；一個交互式的證明者給了我們 IP 等於 PSPACE；一個量子暫存器給了我們 BQP。而在這裡，讓一台自動機永遠運行，給了我們 Büchi 自動機，再栓上一套關於時間的邏輯，便給了我們整套驗證的機器。最後一篇將收攏這一切所留下的那些未解問題——而其中之首，依然是 P 對 NP。