模型檢測學習筆記（一）：緒論

一、概念  模型檢測是一種用於自動驗證有限狀態併發系統的技術；模型檢測算法通常對系統狀態空間進行窮盡搜索來確定性質的真假。如果資源充足，檢測過程總是以是或非終止，是表示系統滿足性質，否表示不滿足性質，並自動給出一個反例。 模型檢測中最大的困難是狀態空間爆炸；解決狀態空間爆炸有如下方法： 符號化模型檢驗技術； 偏序規約技術； on-the-fly技術； 對稱技術； 抽象和組合技術； 二、模型檢測的過

>>阅读原文<<