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