模型檢測

在計算機科學領域，模型檢測或屬性檢測是一種用於驗證系統的有限狀態模型是否滿足給定規範（即正確性）的方法。這種方法通常應用於硬件或軟件系統；在此類系統中，規範不僅包含安全性需求（例如避免導致系統崩潰的狀態），同時也包含活性需求（例如避免活鎖現象）。

為了能夠通過算法解決此類問題，系統的模型及其規範均需使用精確的數學語言進行形式化表述。為此，該問題被轉化為邏輯範疇下的任務，即驗證某個特定的結構是否滿足給定的邏輯公式。這一通用概念適用於多種邏輯類型及各類結構。最基礎的模型檢測問題，即是驗證給定的結構是否滿足命題邏輯中的某個公式。

參見