基於Petri網的計算樹邏輯模型檢測
劉關俊,何雷鋒
相關主題
商品描述
本書主要介紹原型 Petri 網、知識 Petri 網、帶有優先級的時間 Petri網，用於對有限狀態並發系統控制流、安全多方計算協議、多處理器搶占式實時系統等在一定層級上的抽象建模，如刻畫並發、選擇、沖突、多方交互、多方認知過程、（搶占式）資源分配、事件的實時性約束等。本書介紹的計算樹邏輯、知識計算樹邏輯、時間計算樹邏輯等可以用於規約這些系統所關註的設計需求，如無死鎖、公平性、隱私性、可調度性、最壞執行時間等。本書重點介紹使用這些 Petri 網模型驗證以上時序邏輯的算法。另外，本書介紹簡化有序二叉決策圖，介紹如何將其用於表達 Petri 網的狀態、狀態間的遷移關系及狀態間的等價關系，並將其應用於計算樹邏輯與 知識計算樹邏輯的模型檢測上。
目錄大綱
目錄
前言
第1章 緒論 1
1.1 研究背景 1
1.2 研究現狀 3
1.2.1 有限狀態並發系統控制流的模型檢測 3
1.2.2 安全多方計算協議的模型檢測 5
1.2.3 多處理器搶占式實時系統的模型檢測 7
1.3 內容概述 9
第2章 基礎知識 11
2.1 原型 Petri 網 11
2.1.1 常用的集合符號 11
2.1.2 原型 Petri 網的定義 12
2.1.3 原型 Petri 網的性質 15
2.2 時間 Petri 網 16
2.2.1 時間 Petri 網的定義 17
2.2.2 時間 Petri 網的狀態類圖 18
2.3 優先級時間 Petri 網 21
2.3.1 優先級時間 Petri 網的定義 21
2.3.2 狀態類圖 21
2.4 模型檢測 22
第3章 簡化有序二叉決策圖 24
3.1 布爾函數簡介 24
3.1.1 布爾函數 24
3.1.2 布爾函數的其他描述形式 27
3.2 簡化有序二叉決策圖簡介 31
3.2.1 ROBDD 的定義 31
3.2.2 ROBDD 的性質 33
3.3 ROBDD 的變量排序方法 34
3.3.1 動態變量排序法 35
3.3.2 靜態變量排序法 37
3.4 基於 ROBDD 符號表達 Petri 網 41
3.4.1 基於 ROBDD 符號表達安全 Petri 網 41
3.4.2 基於 ROBDD 符號表達有界 Petri 網 49
第4章 計算樹邏輯模型檢測 59
4.1 計算樹邏輯 59
4.1.1 CTL 的語法與語義 59
4.1.2 CTL 的標準範式 62
4.2 CTL 的傳統驗證方法 62
4.3 基於 ROBDD 的 CTL 驗證方法 66
4.3.1 第一種符號模型檢測 CTL 的方法 67
4.3.2 第二種符號模型檢測 CTL 的方法 70
4.4 應用實例 73
4.4.1 柔性製造系統 73
4.4.2 多線程程序 74
4.5 實驗與分析 76
4.5.1 哲學家就餐問題 77
4.5.2 資源分配系統 84
4.5.3 埃拉托色尼篩選法 86
4.5.4 n 皇後問題 89
第5章 知識 Petri 網 92
5.1 知識 Petri 網的定義 92
5.2 帶有等價關系的可達圖 RGER 93
5.3 基於 ROBDD 符號表達 RGER 97
第6章 知識計算樹邏輯模型檢測 100
6.1 知識計算樹邏輯 100
6.2 基於 RGER 的 CTLK 的驗證方法 102
6.3 基於 ROBDD 的 CTLK 的驗證方法 108
6.3.1 第一種符號模型檢測 CTLK 的方法 108
6.3.2 第二種符號模型檢測 CTLK 的方法 111
6.4 應用實例：密碼學家就餐協議 116
第7章 帶有計時器的時間 Petri 網 127
7.1 傳統的四種帶有計時器的時間 Petri 網 127
7.1.1 調度擴展時間 Petri 網 127
7.1.2 搶占式時間 Petri 網 130
7.1.3 帶有抑止超弧的時間 Petri 網 132
7.1.4 計時器時間 Petri 網 135
7.2 優先級時間點區間 Petri 網 138
7.2.1 優先級時間點區間 Petri 網 PToPN 的定義 138
7.2.2 PToPN 的狀態圖 141
第8章 時間計算樹邏輯模型檢測 145
8.1 時間計算樹邏輯 145
8.1.1 TCTL 的語法與語義 145
8.1.2 TCTL 的標準範式 147
8.2 基於 PToPN 的 TCTL 的驗證方法 148
8.3 帶有時間未知數的時間計算樹邏輯 155
8.3.1 TCTLx 的語法與語義 155
8.3.2 基於 PToPN 的 TCTLx 的驗證方法 157
8.4 應用實例 159
8.4.1 系統描述與兩個不同的網模型 159
8.4.2 基於 TCTLx 的性質規約 163
8.4.3 實驗結果與分析 165
第9章 模型檢測器 169
9.1 模型檢測器框架概述 169
9.2 CTL 模型檢測器 170
9.3 CTLK 模型檢測器 173
9.4 TCTL 模型檢測器 175
9.5 TCTLx 模型檢測器 177
第10章 總結與展望 180
10.1 總結 180
10.2 展望 181
參考文獻 183
前言
第1章 緒論 1
1.1 研究背景 1
1.2 研究現狀 3
1.2.1 有限狀態並發系統控制流的模型檢測 3
1.2.2 安全多方計算協議的模型檢測 5
1.2.3 多處理器搶占式實時系統的模型檢測 7
1.3 內容概述 9
第2章 基礎知識 11
2.1 原型 Petri 網 11
2.1.1 常用的集合符號 11
2.1.2 原型 Petri 網的定義 12
2.1.3 原型 Petri 網的性質 15
2.2 時間 Petri 網 16
2.2.1 時間 Petri 網的定義 17
2.2.2 時間 Petri 網的狀態類圖 18
2.3 優先級時間 Petri 網 21
2.3.1 優先級時間 Petri 網的定義 21
2.3.2 狀態類圖 21
2.4 模型檢測 22
第3章 簡化有序二叉決策圖 24
3.1 布爾函數簡介 24
3.1.1 布爾函數 24
3.1.2 布爾函數的其他描述形式 27
3.2 簡化有序二叉決策圖簡介 31
3.2.1 ROBDD 的定義 31
3.2.2 ROBDD 的性質 33
3.3 ROBDD 的變量排序方法 34
3.3.1 動態變量排序法 35
3.3.2 靜態變量排序法 37
3.4 基於 ROBDD 符號表達 Petri 網 41
3.4.1 基於 ROBDD 符號表達安全 Petri 網 41
3.4.2 基於 ROBDD 符號表達有界 Petri 網 49
第4章 計算樹邏輯模型檢測 59
4.1 計算樹邏輯 59
4.1.1 CTL 的語法與語義 59
4.1.2 CTL 的標準範式 62
4.2 CTL 的傳統驗證方法 62
4.3 基於 ROBDD 的 CTL 驗證方法 66
4.3.1 第一種符號模型檢測 CTL 的方法 67
4.3.2 第二種符號模型檢測 CTL 的方法 70
4.4 應用實例 73
4.4.1 柔性製造系統 73
4.4.2 多線程程序 74
4.5 實驗與分析 76
4.5.1 哲學家就餐問題 77
4.5.2 資源分配系統 84
4.5.3 埃拉托色尼篩選法 86
4.5.4 n 皇後問題 89
第5章 知識 Petri 網 92
5.1 知識 Petri 網的定義 92
5.2 帶有等價關系的可達圖 RGER 93
5.3 基於 ROBDD 符號表達 RGER 97
第6章 知識計算樹邏輯模型檢測 100
6.1 知識計算樹邏輯 100
6.2 基於 RGER 的 CTLK 的驗證方法 102
6.3 基於 ROBDD 的 CTLK 的驗證方法 108
6.3.1 第一種符號模型檢測 CTLK 的方法 108
6.3.2 第二種符號模型檢測 CTLK 的方法 111
6.4 應用實例：密碼學家就餐協議 116
第7章 帶有計時器的時間 Petri 網 127
7.1 傳統的四種帶有計時器的時間 Petri 網 127
7.1.1 調度擴展時間 Petri 網 127
7.1.2 搶占式時間 Petri 網 130
7.1.3 帶有抑止超弧的時間 Petri 網 132
7.1.4 計時器時間 Petri 網 135
7.2 優先級時間點區間 Petri 網 138
7.2.1 優先級時間點區間 Petri 網 PToPN 的定義 138
7.2.2 PToPN 的狀態圖 141
第8章 時間計算樹邏輯模型檢測 145
8.1 時間計算樹邏輯 145
8.1.1 TCTL 的語法與語義 145
8.1.2 TCTL 的標準範式 147
8.2 基於 PToPN 的 TCTL 的驗證方法 148
8.3 帶有時間未知數的時間計算樹邏輯 155
8.3.1 TCTLx 的語法與語義 155
8.3.2 基於 PToPN 的 TCTLx 的驗證方法 157
8.4 應用實例 159
8.4.1 系統描述與兩個不同的網模型 159
8.4.2 基於 TCTLx 的性質規約 163
8.4.3 實驗結果與分析 165
第9章 模型檢測器 169
9.1 模型檢測器框架概述 169
9.2 CTL 模型檢測器 170
9.3 CTLK 模型檢測器 173
9.4 TCTL 模型檢測器 175
9.5 TCTLx 模型檢測器 177
第10章 總結與展望 180
10.1 總結 180
10.2 展望 181
參考文獻 183
