模型檢驗原理 Principles of Model Checking

本書全面系統地介紹了模型檢驗的一般原理、應用工具及軟硬件系統的建模與驗證方法，同時介紹了剋服模型檢驗中“狀態空間爆炸”問題的有效途徑，可作為電腦科學與技術、軟件工程等專業本科生、研究生的教材，也可作為模型檢驗領域研究人員及註重系統可靠性的設計與開發人員的參考書。

趙光峰，男，1964年生，教授，博士，曾留學英國一年，主要研究方向為拓撲學、圖論、系統可信性自動驗證，發表學術論文30餘篇，主編《Visual Basic 程序設計教程》（高等教育出版社）等教材5部。

第1章  系統驗證 1
1.1  模型檢驗 4
1.2  模型檢驗的特徵 7
1.2.1  模型檢驗的步驟 7
1.2.2  模型檢驗的優點與缺點 9
1.3  文獻說明 10
第2章  並發系統的建模 12
2.1  遷移系統 12
2.1.1  執行 15
2.1.2  硬件和軟件系統的建模 16
2.2  並行與通信 23
2.2.1  並發與交錯 23
2.2.2  用共享變量通信 26
2.2.3  握手 32
2.2.4  通道系統 36
2.2.5  nanoPromela 42
2.2.6  同步並行性 51
2.3  狀態空間爆炸問題 53
2.4  總結 55
2.5  文獻說明 55
2.6  習題 56
第3章  線性時間性質 61
3.1  死鎖 61
3.2  線性時間行為 64
3.2.1  路徑與狀態圖 64
3.2.2  跡 66
3.2.3  線性時間性質 68
3.2.4  蹟等價與線性時間性質 71
3.3  安全性質與不變式 72
3.3.1  不變式 73
3.3.2  安全性質 76
3.3.3  蹟等價與安全性質 79
3.4  活性性質 82
3.4.1  活性性質概念 82
3.4.2  安全性質與活性性質 83
3.5  公平性 86
3.5.1  公平性約束 87
3.5.2  公平性策略 93
3.5.3  公平性與安全性 94
3.6  總結 96
3.7  文獻說明 97
3.8  習題 97
第4章  正則性質 103
4.1  有限單詞上的自動機 103
4.2  正則安全性質的模型檢驗 108
4.2.1  正則安全性質 108
4.2.2  驗證正則安全性質 111
4.3  無限單詞上的自動機 116
4.3.1  ??正則語言與性質 116
4.3.2  未定 Büchi 自動機 118
4.3.3  確定 Büchi 自動機 128
4.3.4  廣義未定 Büchi 自動機 131
4.4  模型檢驗?正則性質 136
4.4.1  持久性質與乘積 136
4.4.2  嵌套深度優先搜索 140
4.5  總結 149
4.6  文獻說明 149
4.7  習題 150
第5章  線性時序邏輯 157
5.1  線性時序邏輯述要 157
5.1.1  語法 158
5.1.2  語義 161
5.1.3  準述性質 164
5.1.4  LTL 公式的等價性 170
5.1.5  弱直到、釋放和正範式 173
5.1.6  LTL 中的公平性 177
5.2  基於自動機的 LTL 模型檢驗 186
5.2.1  LTL 模型檢驗問題的複雜度 199
5.2.2  LTL 可滿足性和有效性檢驗 205
5.3  總結 207
5.4  文獻說明 208
5.5  習題 208
第6章  計算樹邏輯 218
6.1  引言 218
6.2  計算樹邏輯 220
6.2.1  語法 220
6.2.2  語義 222
6.2.3  CTL 公式的等價性 229
6.2.4  CTL 範式 230
6.3  LTL 與 CTL 的表達力對比 232
6.4  CTL 模型檢驗 236
6.4.1  基本算法 236
6.4.2  直到和存在總是運算符  241
6.4.3  時間複雜度和空間複雜度 246
6.5  CTL 的公平性 249
6.6  反例和證據 259
6.6.1  CTL 中的反例 261
6.6.2  公平 CTL 中的反例和證據 264
6.7  符號 CTL 模型檢驗 265
6.7.1  開關函數 265
6.7.2  用開關函數編碼遷移系統 268
6.7.3  有序二叉決策圖 273
6.7.4  實現基於 ROBDD 的算法 283
6.8  CTL* 294
6.8.1  邏輯、表達力和等價 294
6.8.2  CTL* 模型檢驗 298
6.9  總結 300
6.10  文獻說明 301
6.11  習題 302
第7章  等價和抽象 314
7.1  互模擬 315
7.1.1  互模擬商 319
7.1.2  基於動作的互模擬 325
7.2  互模擬和CTL* 等價 327
7.3  求互模擬商的算法 332
7.3.1  確定初始劃分 334
7.3.2  細化劃分 334
7.3.3  第一個劃分細化算法 339
7.3.4  效率改進 340
7.3.5  遷移系統的等價檢驗 345
7.4  模擬關係 347
7.4.1  模擬等價 353
7.4.2  互模擬、模擬與蹟等價 357
7.5  模擬等價和\\forall CTL*等價 360
7.6  求模擬商的算法 364
7.7  踏步線性時間關係 369
7.7.1  踏步蹟等價 370
7.7.2  踏步蹟等價和LTL_\\setminus\\bigcirc 等價 373
7.8  踏步互模擬 374
7.8.1  發散敏感的踏步互模擬 379
7.8.2  賦範互模擬 385
7.8.3  踏步互模擬和CTL*_\\setminus\\bigcirc 等價 391
7.8.4  踏步互模擬求商 396
7.9  總結 404
7.10  文獻說明 404
7.11  習題 405
第8章  偏序約簡 414
8.1  動作的無關性 415
8.2  線性時間的充足集方法 421
8.2.1  充足集的條件 421
8.2.2  動態偏序約簡 431
8.2.3  計算充足集 436
8.2.4  靜態偏序約簡 442
8.3  分支時間的充足集方法 452
8.4  總結 460
8.5  文獻說明 461
8.6  習題 461
第9章  時控自動機 469
9.1  時控自動機述要 471
9.1.1  語義 476
9.1.2  時間發散、 時間鎖定 和芝諾性 481
9.2  時控計算樹邏輯 486
9.3  TCTL 模型檢驗 491
9.3.1  消去時間參數 492
9.3.2  區域遷移系統 494
9.3.3  TCTL 模型檢驗算法 511
9.4  總結 515
9.5  文獻說明 515
9.6  習題 516
第10章  概率系統 520
10.1  馬爾可夫鏈 521
10.1.1  可達性概率 530
10.1.2  定性性質 539
10.2  概率計算樹邏輯 546
10.2.1  PCTL 模型檢驗 549
10.2.2  PCTL 的定性片段 551
10.3  線性時間性質 557
10.4  PCTL* 和概率互模擬 565
10.4.1  PCTL* 565
10.4.2  概率互模擬 566
10.5  帶成本的馬爾可夫鏈 572
10.5.1  成本有界可達性 573
10.5.2  長遠性質 580
10.6  馬爾可夫決策過程 584
10.6.1  可達性概率 597
10.6.2  PCTL 模型檢驗 608
10.6.3  極限性質 611
10.6.4  線性時間性質和PCTL* 619
10.6.5  公平性 622
10.7  總結 630
10.8  文獻說明 632
10.9  習題 633
附錄 A  預備知識 641
A.1  常用符號與記號 641
A.2  形式語言 643
A.3  命題邏輯 645
A.4  圖論 649
A.5  計算複雜度 652
參考文獻 656
譯註 680