《隨機模型檢測理論與應(yīng)用》致力于緩解隨機模型檢測中的狀態(tài)空間爆炸問題。首先介紹了離散時間馬爾科夫鏈、馬爾科夫決策過程、連續(xù)時間馬爾科夫鏈和概率實時解釋系統(tǒng)上的限界檢測技術(shù)。然后討論了模型檢測概率、實時認知時態(tài)邏輯中的二值與三值抽象技術(shù)。最后從應(yīng)用出發(fā)，探討了隨機模型檢測技術(shù)在云計算和物聯(lián)網(wǎng)領(lǐng)域的應(yīng)用。
更多科學(xué)出版社服務(wù)，請掃碼獲取。
計算機科學(xué)與技術(shù)專業(yè)的碩士生、博士生，相關(guān)領(lǐng)域的研究人員。
目錄
前言
第1章 隨機模型檢測概述 1
1.1 模型檢測 1
1.2 狀態(tài)壁間約簡 3
1.2.1 基于有序工叉決策圖的符號化模型檢測方法 3
1.2.2 基于命題公式可滿足性判定的限界模型檢測方法 4
1.2.3 抽象方法 5
1.2.4 組合驗證 6
1.2.5 其他約簡方法 6
1.3 線性時態(tài)邏輯的限界模型檢測 7
1.3.1 示例 7
1.3.2 線性時態(tài)邏輯 7
1.3.3 線性時態(tài)邏輯的限界語義 8
1.3.4 轉(zhuǎn)換 9
1.4 抽象 11
1.4.1 互模擬與模擬 11
1.4.2 數(shù)據(jù)抽象 12
1.5 隨機模型檢測 14
1.6 本章小結(jié) 16
參考文獻 16
第2章 離散時間馬爾可夫鏈的限界模型檢測 19
2.1 概述 19
2.2 離散時間馬爾可夫鏈與概率計算樹邏輯 19
2.3 概率計算樹邏輯的限界模型檢測 21
2.3.1 概率計算樹邏輯的等價性 21
2.3.2 概率計算樹邏輯的限界語義 22
2.3.3 限界模型檢測過程終止的判斷 23
2.3.4 概率計算樹邏輯的限界模型檢測算法 26
2.4 實例：IPv4零配置協(xié)議 27
2.5 實驗結(jié)果 30
2.6 限界模型檢測過程終止判斷標準的修正 32
2.7 相關(guān)工作 34
2.8 本章小結(jié) 34
參考文獻 35
第3章 馬爾可夫決策過程的限界模型檢測 36
3.1 概述 36
3.2 馬爾可夫決策過程與概率計算樹邏輯 36
3.3 概率計算樹邏輯的限界模型檢測 38
3.3.1 概率計算樹邏輯的等價性 38
3.3.2 概率計算樹邏輯的限界語義 39
3.3.3 限界模型檢測過程終止的判斷 42
3.3.4 限界模型檢測算法 44
3.4 實例研究 48
3.5 實驗結(jié)果 50
3.6 終止標準的修正 53
3.7 本章小結(jié) 55
參考文獻 56
第4章 連續(xù)時間馬爾可夫鏈的限界模型檢測 57
4.1 連續(xù)隨機邏輯與連續(xù)時間馬爾可夫鏈 57
4.1.1 連續(xù)隨機邏輯 57
4.1.2 連續(xù)時間馬爾可夫鏈 57
4.1.3 轉(zhuǎn)移概率與極限概率 59
4.1.4 連續(xù)隨機邏輯的語義 60
4.2 連續(xù)隨機邏輯的限界模型檢測 60
4.2.1 連續(xù)隨機邏輯的眼界語且 60
4.2.2 限界下轉(zhuǎn)移概率的計算 62
4.2.3 限界檢測算法 63
4.3 實驗結(jié)果 68
4.4 本章小結(jié) 74
參考文獻 74
第5章 多智體系統(tǒng)的限界模型檢測 75
5.1 概述 75
5.2 相關(guān)工作 76
5.3 概率實時解釋系統(tǒng) 77
5.3.1 概率時間自動機 77
5.3.2 概率時間自動機的平行組合 79
5.3.3 概率時間自動機的語義 81
5.3.4 概率實時解釋系統(tǒng) 82
5.4 概率實時認知邏輯 85
5.4.1 概率實時認知邏輯的語法 85
5.4.2 概率實時認知邏輯的語義 85
5.5 概率知識區(qū)域圖 87
5.6 基于概率知識區(qū)域圖的限界模型檢測 91
5.6.1 時態(tài)邏輯的轉(zhuǎn)換 91
5.6.2 轉(zhuǎn)換邏輯的限界模型檢測 93
5.7 限界模型檢測算法 96
5.8 線性方程組的求解 99
5.9 實例研究 100
5.9.1 火牢穿越控制系統(tǒng) 100
5.9.2 控制系統(tǒng)的限界模型檢測 102
5.10 終止性選擇標準 106
5.11 本章小結(jié) 107
參考文獻 107
第6章 模型檢測多智體系統(tǒng)申的抽象技術(shù) 109
6.1 概述 109
6.2 相關(guān)工作 109
6.3 解釋系統(tǒng)與時態(tài)邏輯 110
6.4 驗證屬性驅(qū)動的抽象 111
6.4.1 屬性驅(qū)動的存在性抽象 111
6.4.2 屬性的可滿足性保持 113
6.5 反例真實性確認 115
6.5.1 什么是反例 115
6.5.2 識別虛假反例 119
6.5.3 反例引導(dǎo)的求精 119
6.6 實例研究 120
6.6.1 撲克橋戲 120
6.6.2 抽象 122
6.7 實驗 123
6.7.1 密碼學(xué)家就餐協(xié)議 123
6.7.2 實驗結(jié)果 124
6.8 本章小結(jié) 125
參考文獻 125
第7章 概率時態(tài)認知邏輯模型檢測中的抽象技術(shù) 126
7.1 概率時態(tài)認知邏輯語法和語義 126
7.2 建立抽象模型 127
7.3 屬性保持關(guān)系 130
7.4 概率時態(tài)認知邏輯模型檢測算法 131
7.5 抽象模型的求精 134
7.5.1 抽象失敗原因分析 134
7.5.2 抽象求精 135
7.6 模型檢測密碼學(xué)家就餐協(xié)議 139
7.6.1 密碼學(xué)家就餐協(xié)議的概率Kripke結(jié)構(gòu) 139
7.6.2 建立密碼學(xué)家就餐協(xié)議的抽象模型 140
7.6.3 實驗結(jié)果 141
7.7 本章小結(jié) 142
參考文獻 142
第8章 實時時態(tài)認知邏輯模型檢測中的抽象技術(shù) 143
8.1 實時時態(tài)認知邏輯語法和語義 143
8.1.1 實時時態(tài)認知邏輯的語法 143
8.1.2 實時解釋系統(tǒng) 143
8.1.3 實時時態(tài)認知邏輯的語義 144
8.2 建立抽象模型 145
8.3 屬性保持關(guān)系 146
8.4 實例分析 148
8.4.1 鐵路道口系統(tǒng)介紹 148
8.4.2 建立鐵路道口系統(tǒng)的抽象模型 149
8.4.3 模型檢測鐵路道口系統(tǒng) 151
8.5 抽象模型及實時時態(tài)認知邏輯的三值語義 151
8.6 三值抽象下的屬性保持關(guān)系 153
8.7 模型檢測主動結(jié)構(gòu)控制系統(tǒng) 156
8.7.1 主動結(jié)構(gòu)控制系統(tǒng)的一個演變形式 156
8.7.2 建立主動結(jié)構(gòu)控制系統(tǒng)的抽象模型 158
8.7.3 模型檢測主動結(jié)構(gòu)控制系統(tǒng) 159
8.8 鐵路道口系統(tǒng)的進一步驗證 160
8.9 本章小結(jié) 161
參考文獻 161
第9章 快速安全協(xié)議的性能分析 162
9.1 模型檢測工具PRISM 162
9.2 基本建模過程 163
9.3 快速安全協(xié)議 165
9.4 FASP建模 165
9.5 FASP模型統(tǒng)計 169
9.6 性能屬性分析 171
9.6.1 FASP的可靠性分析 171
9.6.2 FASP的快速性分析 173
9.6.3 吞吐量分析 175
9.7 本章小結(jié) 176
參考文獻 177
第10章 IEEE 802.11P中MAC協(xié)議的性能分析 178
10.1 IEEE 802.11P中MAC協(xié)議的工作特性 178
10.2 MAC協(xié)議的概率時間自動機模型 180
10.3 IEEE 802.11P模型的靜態(tài)數(shù)據(jù)分析 183
10.4 IEEE 802.11P模型的驗證分析 184
10.4.1 IEEE 802.11P模型的概率可達性 184
10.4.2 IEEE 802.11P模型的期望可達性 185
10.5 本章小結(jié) 188
參考文獻 189
第11章 RFID中S-ALOHA協(xié)議的性能分析 190
11.1 概述 190
11.2 協(xié)議建模 191
11.2.1 協(xié)議工作原理 191
11.2.2 協(xié)議的馬爾可夫決策過程模型 192
11.3 模型的驗證與分析 194
11.3.1 模型統(tǒng)計 194
11.3.2 概率可達性 195
11.3.3 S-ALOHA與ALOHA的屬性驗證對比 196
11.3.4 預(yù)期可達性 198
11.4 本章小結(jié) 200
參考文獻 201
后記 202
書單推薦
