模型檢測學習筆記（一）：緒論
一、概念
模型檢測是一種用於自動驗證有限狀態併發系統的技術；模型檢測演算法通常對系統狀態空間進行窮盡搜尋來確定性質的真假。如果資源充足，檢測過程總是以是或非終止，是表示系統滿足性質，否表示不滿足性質，並自動給出一個反例。
模型檢測中最大的困難是狀態空間爆炸；解決狀態空間爆炸有如下方法：
- 符號化模型檢驗技術；
- 偏序規約技術；
- on-the-fly技術；
- 對稱技術；
- 抽象和組合技術；
二、模型檢測的過程
使用模型檢測技術來進行系統設計的驗證包含以下三個步驟：
1、建模：第一個步驟是把設計轉化為被模型檢測工具接受的形式；可能由於驗證時間和計算機記憶體的限制，還需要使用抽象技術簡約不相關或不重要的細節（建模+簡約）
2、刻畫：宣告設計必須滿足的性質。性質刻畫通常以某種邏輯的形式（如時序邏輯，這種邏輯體系表示系統隨著時間的變化）表示。（用一種邏輯形式來刻畫一個性質）
3、驗證：理想上的驗證應該是完全自動的。但實際上常常需要人的幫助，其中之一就是分析結果。當得到失敗結果後，通常可以給使用者提供一個錯誤軌跡，可以把它看作檢測性質的一個反例。
三、解決狀態空間爆炸的方法簡介
1、符號化模型檢驗技術
1993年KL McMillan基於RE Byrant的有序二叉判定圖（OBDD）來有效地表示狀態遷移系統，提出了符號化模型檢驗，大大地提高了可有效應用模型檢驗技術的系統規模，使得模型檢驗在工業界逐步得到應用。
用布林公式刻畫狀態集合和狀態對集合，用OBDD來表示這些布林公式，使用OBDD上的布林操作來計算謂詞轉換子（其不動點刻畫了CTL模態子），從而使模型檢驗在壓縮了的符號化狀態空間上來驗證CTL性質。
2、偏序規約技術
通過發掘系統中併發執行的遷移的交換性，減少本質上相同的狀態，從而僅生成足以檢驗性質的小部分狀態空間。
3、on-the-fly技術
把狀態空間生成和檢驗它是否滿足性質合在一起做，而不去預先生成整個狀態空間，從而儘可能避免狀態爆炸。
4、對稱技術
針對由多個完全類似的程序組成的系統，利用其模型的狀態空間的對稱性來生成壓縮的且對模型檢驗等價的模型。
5、抽象和組合技術
抽象方法通過把原來模型中與待驗證性質無關的資訊去掉而獲得簡化模型的方式來減小模型檢驗時問題的規模，抽象必須是保持性質的，即若簡化的模型滿足性質，則原來的模型亦滿足該性質。
組合方法基於分而治之的思路來縮減模型檢驗時問題的規模，先驗證系統的構件的區域性性質，然後把這些性質組合起來獲得系統的全域性性質。