前言 第1章 緒論 1.1 研究背景 1.2 研究現狀 1.2.1 有限狀態并發系統控制流的模型檢測 1.2.2 安全多方計算協議的模型檢測 1.2.3 多處理器搶占式實時系統的模型檢測 1.3 內容概述 第2章 基礎知識 2.1 原型Petri網 2.1.1 常用的集合符號 2.1.2 原型Petri網的定義 2.1.3 原型Petri網的性質 2.2 時間Petri網 2.2.1 時間Petri網的定義 2.2.2 時間Petri網的狀態類圖 2.3 優先級時間Petri網 2.3.1 優先級時間Petri網的定義 2.3.2 狀態類圖 2.4 模型檢測 第3章 簡化有序二叉決策圖 3.1 布爾函數簡介 3.1.1 布爾函數 3.1.2 布爾函數的其他描述形式 3.2 簡化有序二叉決策圖簡介 3.2.1 ROBDD的定義 3.2.2 ROBDD的性質 3.3 ROBDD的變量排序方法 3.3.1 動態變量排序法 3.3.2 靜態變量排序法 3.4 基于ROBDD符號表達Petri網 3.4.1 基于ROBDD符號表達安全Petri網 3.4.2 基于ROBDD符號表達有界Petri網 第4章 計算樹邏輯模型檢測 4.1 計算樹邏輯 4.1.1 CTL的語法與語義 4.1.2 CTL的標準范式 4.2 CTL的傳統驗證方法 4.3 基于ROBDD的CTL驗證方法 4.3.1 **種符號模型檢測CTL的方法 4.3.2 第二種符號模型檢測CTL的方法 4.4 應用實例 4.4.1 柔性制造系統 4.4.2 多線程程序 4.5 實驗與分析 4.5.1 哲學家就餐問題 4.5.2 資源分配系統 4.5.3 埃拉托色尼篩選法 4.5.4 n皇后問題 第5章 知識Petri網 5.1 知識Petri網的定義 5.2 帶有等價關系的可達圖RGER 5.3 基于ROBDD符號表達RGER 第6章 知識計算樹邏輯模型檢測 6.1 知識計算樹邏輯 6.2 基于RGER的CTLK的驗證方法 6.3 基于ROBDD的CTLK的驗證方法 6.3.1 **種符號模型檢測CTLK的方法 6.3.2 第二種符號模型檢測CTLK的方法 6.4 應用實例：密碼學家就餐協議 第7章 帶有計時器的時間Petri網 7.1 傳統的四種帶有計時器的時間Petri網 7.1.1 調度擴展時間Petri網 7.1.2 搶占式時間Petri網 7.1.3 帶有抑止超弧的時間Petri網 7.1.4 計時器時間Petri網 7.2 優先級時間點區間Petri網 7.2.1 優先級時間點區間Petri網PToPN的定義 7.2.2 PToPN的狀態圖 第8章 時間計算樹邏輯模型檢測 8.1 時間計算樹邏輯 8.1.1 TCTL的語法與語義 8.1.2 TCTL的標準范式 8.2 基于 PToPN的TCTL的驗證方法 8.3 帶有時間未知數的時間計算樹邏輯 8.3.1 TCTLx的語法與語義 8.3.2 基于PToPN的TCTLx的驗證方法 8.4 應用實例 8.4.1 系統描述與兩個不同的網模型 8.4.2 基于TCTLx的性質規約 8.4.3 實驗結果與分析 第9章 模型檢測器 9.1 模型檢測器框架概述 9.2 CTL模型檢測器 9.3 CTLK模型檢測器 9.4 TCTL模型檢測器 9.5 TCTLx模型檢測器 第10章 總結與展望 10.1 總結 10.2 展望 參考文獻