模型檢測

由於模型檢測可以自動執行，並能在系統不滿足性質時提供反例路徑，因此在工業界比演繹證明更受推崇。

儘管限制在有窮系統上是一個缺點，但模型檢測可以應用於許多非常重要的系統，如硬件控制器和通信協議等有窮狀態系統。很多情況下，可以把模型檢測和各種抽象與歸納原則結合起來驗證非有窮狀態系統(如實時系統)。

模型檢測的基本思想是用狀態遷移系統(S)表示系統的行為，用模態邏輯公式(F)描述系統的性質。這樣“系統是否具有所期望的性質”就轉化為數學問題“狀態遷移系統S是否是公式F的一個模型”，用公式表示為S╞F。對有窮狀態系統，這個問題是可判定的，即可以用計算機程序在有限時間內自動確定。

模型檢測已被應用於計算機硬件、通信協議、控制系統、安全認證協議等方面的分析與驗證中，取得了令人矚目的成功，並從學術界輻射到了產業界。