模型檢測

模型檢測(model checking)是一種很重要的自動驗證技術。它最早由Clarke和Emerson以及Quielle和Sifakis在1981年分別提出，主要通過顯式狀態搜索或隱式不動點計算來驗證有窮狀態併發系統的模態/命題性質。由於模型檢測可以自動執行，並能在系統不滿足性質時提供反例路徑，因此在工業界比演繹證明更受推崇。儘管限制在有窮系統上是一個缺點，但模型檢測可以應用於許多非常重要的系統，如硬體控制器和通信協議等有窮狀態系統。很多情況下，可以把模型檢測和各種抽象與歸納原則結合起來驗證非有窮狀態系統(如實時系統)。