Buchi 自動機（Büchi automaton）
/ BUE-khee /
你至今遇到的每個有限自動機，都是讀完一個有限字串後就停下並做出判定。但對於一個永不停止的系統呢——一個作業系統、一個網路協定、一個永遠運行的控制器？它的行為是一個無窮的事件序列，一個無窮字。Buchi 自動機就是把有限自動機改裝後，用來接受（或拒絕）無窮字，因而成為對不終止、持續運行系統進行推理的天然工具。
它看起來和普通的非確定型有限自動機一模一樣——狀態、轉移、一個起始狀態、一組接受狀態——但它的接受條件被重新詮釋以適應永不結束的輸入。Buchi 自動機在一個無窮字上的執行，是一條穿過狀態的無窮路徑。接受規則是：若這條執行無窮多次造訪某個接受狀態，它就被接受。不只一次，而是永無止盡地一再造訪。所以我們問的不是「我們是否在接受狀態結束？」，而是「我們是否無窮地不斷回到某個良好狀態？」。這完美地捕捉了像「系統終究會回應每個請求」這樣的活性性質，以及像「這個行程被無窮多次排程」這樣的公平性。
Buchi 自動機處於自動驗證（模型檢驗）的核心。它們是自動機與時序邏輯之間的橋樑：一份關於系統在無窮時間上應如何表現的時序邏輯規格，可以翻譯成一個 Buchi 自動機，於是「把系統對照規格檢查」便化為關於這些自動機的問題。一個值得標明的誠實微妙處：與有限字自動機不同，非確定型 Buchi 自動機嚴格地比確定型更具表達力——你無法總是把 Buchi 自動機確定化（要確定化，必須改用更豐富的接受條件，如 Rabin 或 parity）。DFA 等於 NFA 的漂亮等價性並不延續到無窮字上。
一個在字母表 {req, ack} 上的雙狀態 Buchi 自動機，能把「每個請求終究被確認」表達成一個「反覆回到良好狀態」的條件：當某個請求尚未被回應時停留在「等待」狀態，每收到一個 ack 就回到「已滿足」這個接受狀態。一條無窮執行唯有無窮多次重訪「已滿足」狀態才被接受——意味著 ack 永不停歇，所以沒有任何請求被永遠忽略。
Buchi 自動機接受一個無窮字，若其執行無窮多次造訪某個接受狀態。
Buchi 的接受條件是「無窮多次造訪某接受狀態」，不是「在某接受狀態結束」——無窮字沒有結尾。而且與有限字自動機不同，非確定型 Buchi 自動機嚴格地比確定型更強；你無法總是把它們確定化。