模型檢驗（model checking）

你如何確信一個晶片設計或一個並行協定沒有致命錯誤——不只是它通過了你碰巧想到的那些測試，而是某件壞事在任何可能的執行上都絕不會發生？測試只抽樣少數幾次執行；模型檢驗做的事強得多。它窮盡而自動地探索系統所有可達狀態，以證明某個期望的性質在它們全體中都成立，或產生一個具體的反例，精確地展示它如何失敗。

這套做法有三個成分。第一，你把系統建成一個有限（或有限描述）的狀態機：狀態是格局，轉移是可能的步驟。第二，你把想要的性質寫成一個時序邏輯公式（例如「系統絕不死結」或「每個請求終究被服務」）。第三，模型檢驗器機械地判定模型的每個行為是否都滿足該公式。自動機的連結讓這變得具體：時序公式變成一個 Buchi 自動機，而檢查化約為追問「系統與被否定性質之乘積是否有任何接受的無窮執行」——若有，那條執行就是一條錯誤軌跡；若無，性質得證。著名的障礙是狀態爆炸：狀態數隨元件數呈指數成長，而符號方法（緊湊地表示龐大的狀態集）與巧妙的抽象正設法馴服它。

模型檢驗是自動機理論與邏輯在現實世界的重大回報之一。它在硬體設計中是例行公事（驗證處理器與快取一致性協定），也用於裝置驅動程式、通訊與安全協定，以及攸關安全的控制軟體。它的力量與極限是同一個事實：它對你所建的模型給出一個貨真價實的證明，所以一個被驗證過、但對現實的建模有誤或不完整的模型，仍可能誤導你——模型檢驗驗證的是模型，其可信度僅取決於那個模型與你所寫的性質。