目錄
前言
第1章 隨機(jī)模型檢測(cè)概述 1
1.1 模型檢測(cè) 1
1.2 狀態(tài)壁間約簡 3
1.2.1 基于有序工叉決策圖的符號(hào)化模型檢測(cè)方法 3
1.2.2 基于命題公式可滿足性判定的限界模型檢測(cè)方法 4
1.2.3 抽象方法 5
1.2.4 組合驗(yàn)證 6
1.2.5 其他約簡方法 6
1.3 線性時(shí)態(tài)邏輯的限界模型檢測(cè) 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ī)模型檢測(cè) 14
1.6 本章小結(jié) 16
參考文獻(xiàn) 16
第2章 離散時(shí)間馬爾可夫鏈的限界模型檢測(cè) 19
2.1 概述 19
2.2 離散時(shí)間馬爾可夫鏈與概率計(jì)算樹邏輯 19
2.3 概率計(jì)算樹邏輯的限界模型檢測(cè) 21
2.3.1 概率計(jì)算樹邏輯的等價(jià)性 21
2.3.2 概率計(jì)算樹邏輯的限界語義 22
2.3.3 限界模型檢測(cè)過程終止的判斷 23
2.3.4 概率計(jì)算樹邏輯的限界模型檢測(cè)算法 26
2.4 實(shí)例：IPv4零配置協(xié)議 27
2.5 實(shí)驗(yàn)結(jié)果 30
2.6 限界模型檢測(cè)過程終止判斷標(biāo)準(zhǔn)的修正 32
2.7 相關(guān)工作 34
2.8 本章小結(jié) 34
參考文獻(xiàn) 35
第3章 馬爾可夫決策過程的限界模型檢測(cè) 36
3.1 概述 36
3.2 馬爾可夫決策過程與概率計(jì)算樹邏輯 36
3.3 概率計(jì)算樹邏輯的限界模型檢測(cè) 38
3.3.1 概率計(jì)算樹邏輯的等價(jià)性 38
3.3.2 概率計(jì)算樹邏輯的限界語義 39
3.3.3 限界模型檢測(cè)過程終止的判斷 42
3.3.4 限界模型檢測(cè)算法 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í)間馬爾可夫鏈的限界模型檢測(cè) 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ī)邏輯的限界模型檢測(cè) 60
4.2.1 連續(xù)隨機(jī)邏輯的眼界語且 60
4.2.2 限界下轉(zhuǎn)移概率的計(jì)算 62
4.2.3 限界檢測(cè)算法 63
4.3 實(shí)驗(yàn)結(jié)果 68
4.4 本章小結(jié) 74
參考文獻(xiàn) 74
第5章 多智體系統(tǒng)的限界模型檢測(cè) 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ū)域圖的限界模型檢測(cè) 91
5.6.1 時(shí)態(tài)邏輯的轉(zhuǎn)換 91
5.6.2 轉(zhuǎn)換邏輯的限界模型檢測(cè) 93
5.7 限界模型檢測(cè)算法 96
5.8 線性方程組的求解 99
5.9 實(shí)例研究 100
5.9.1 火牢穿越控制系統(tǒng) 100
5.9.2 控制系統(tǒng)的限界模型檢測(cè) 102
5.10 終止性選擇標(biāo)準(zhǔn) 106
5.11 本章小結(jié) 107
參考文獻(xiàn) 107
第6章 模型檢測(cè)多智體系統(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)知邏輯模型檢測(cè)中的抽象技術(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)知邏輯模型檢測(cè)算法 131
7.5 抽象模型的求精 134
7.5.1 抽象失敗原因分析 134
7.5.2 抽象求精 135
7.6 模型檢測(cè)密碼學(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)知邏輯模型檢測(cè)中的抽象技術(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 模型檢測(cè)鐵路道口系統(tǒng) 151
8.5 抽象模型及實(shí)時(shí)時(shí)態(tài)認(rèn)知邏輯的三值語義 151
8.6 三值抽象下的屬性保持關(guān)系 153
8.7 模型檢測(cè)主動(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 模型檢測(cè)主動(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 模型檢測(cè)工具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