中圖網(wǎng)小程序
一鍵登錄
更方便
本類五星書更多>
-
>
全國計算機等級考試最新真考題庫模擬考場及詳解·二級MSOffice高級應用
-
>
決戰(zhàn)行測5000題(言語理解與表達)
-
>
軟件性能測試.分析與調(diào)優(yōu)實踐之路
-
>
第一行代碼Android
-
>
JAVA持續(xù)交付
-
>
EXCEL最強教科書(完全版)(全彩印刷)
-
>
深度學習
模型檢驗原理(清華計算機圖書譯叢) 版權(quán)信息
- ISBN：9787302577355
- 條形碼：9787302577355 ; 978-7-302-57735-5
- 裝幀：70g膠版紙
- 冊數(shù)：暫無
- 重量：暫無
- 所屬分類：>
模型檢驗原理(清華計算機圖書譯叢) 本書特色
1．內(nèi)容全面，條理系統(tǒng)。 2．實例豐富，便于理解。 3．理論充實，實踐性強4．文獻翔實，脈絡(luò)清晰。 5．習題充足，利于掌握。 6．附錄凝練，入門快速。 本書是全面、系統(tǒng)地介紹模型檢驗原理及其應用的鴻篇巨著。
模型檢驗原理(清華計算機圖書譯叢) 內(nèi)容簡介
本書全面系統(tǒng)地介紹了模型檢驗的一般原理、應用工具及軟硬件系統(tǒng)的建模與驗證方法，同時介紹了克服模型檢驗中“狀態(tài)空間爆炸”問題的有效途徑，可作為計算機科學與技術(shù)、軟件工程等專業(yè)本科生、研究生的教材，也可作為模型檢驗領(lǐng)域研究人員及注重系統(tǒng)可靠性的設(shè)計與開發(fā)人員的參考書。
模型檢驗原理(清華計算機圖書譯叢) 目錄
目 錄
第1章 系統(tǒng)驗證 1
1.1 模型檢驗 4
1.2 模型檢驗的特征 7
1.2.1 模型檢驗的步驟 7
1.2.2 模型檢驗的優(yōu)點與缺點 9
1.3 文獻說明 10
第2章 并發(fā)系統(tǒng)的建模 12
2.1 遷移系統(tǒng) 12
2.1.1 執(zhí)行 15
2.1.2 硬件和軟件系統(tǒng)的建模 16
2.2 并行與通信 23
2.2.1 并發(fā)與交錯 23
2.2.2 用共享變量通信 26
2.2.3 握手 32
2.2.4 通道系統(tǒng) 36
2.2.5 nanoPromela 42
2.2.6 同步并行性 51
2.3 狀態(tài)空間爆炸問題 53
2.4 總結(jié) 55
2.5 文獻說明 55
2.6 習題 56
第3章 線性時間性質(zhì) 61
3.1 死鎖 61
3.2 線性時間行為 64
3.2.1 路徑與狀態(tài)圖 64
3.2.2 跡 66
3.2.3 線性時間性質(zhì) 68
3.2.4 跡等價與線性時間性質(zhì) 71
3.3 安全性質(zhì)與不變式 72
3.3.1 不變式 73
3.3.2 安全性質(zhì) 76
3.3.3 跡等價與安全性質(zhì) 79
3.4 活性性質(zhì) 82
3.4.1 活性性質(zhì)概念 82
3.4.2 安全性質(zhì)與活性性質(zhì) 83
3.5 公平性 86
3.5.1 公平性約束 87
3.5.2 公平性策略 93
3.5.3 公平性與安全性 94
3.6 總結(jié) 96
3.7 文獻說明 97
3.8 習題 97
第4章 正則性質(zhì) 103
4.1 有限單詞上的自動機 103
4.2 正則安全性質(zhì)的模型檢驗 108
4.2.1 正則安全性質(zhì) 108
4.2.2 驗證正則安全性質(zhì) 111
4.3 無限單詞上的自動機 116
4.3.1 ??正則語言與性質(zhì) 116
4.3.2 未定 Büchi 自動機 118
4.3.3 確定 Büchi 自動機 128
4.3.4 廣義未定 Büchi 自動機 131
4.4 模型檢驗?正則性質(zhì) 136
4.4.1 持久性質(zhì)與乘積 136
4.4.2 嵌套深度優(yōu)先搜索 140
4.5 總結(jié) 149
4.6 文獻說明 149
4.7 習題 150
第5章 線性時序邏輯 157
5.1 線性時序邏輯述要 157
5.1.1 語法 158
5.1.2 語義 161
5.1.3 準述性質(zhì) 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 總結(jié) 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 反例和證據(jù) 259
6.6.1 CTL 中的反例 261
6.6.2 公平 CTL 中的反例和證據(jù) 264
6.7 符號 CTL 模型檢驗 265
6.7.1 開關(guān)函數(shù) 265
6.7.2 用開關(guān)函數(shù)編碼遷移系統(tǒng) 268
6.7.3 有序二叉決策圖 273
6.7.4 實現(xiàn)基于 ROBDD 的算法 283
6.8 CTL* 294
6.8.1 邏輯、表達力和等價 294
6.8.2 CTL* 模型檢驗 298
6.9 總結(jié) 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 遷移系統(tǒng)的等價檢驗 345
7.4 模擬關(guān)系 347
7.4.1 模擬等價 353
7.4.2 互模擬、模擬與跡等價 357
7.5 模擬等價和\forall CTL*等價 360
7.6 求模擬商的算法 364
7.7 踏步線性時間關(guān)系 369
7.7.1 踏步跡等價 370
7.7.2 踏步跡等價和LTL_\setminus\bigcirc 等價 373
7.8 踏步互模擬 374
7.8.1 發(fā)散敏感的踏步互模擬 379
7.8.2 賦范互模擬 385
7.8.3 踏步互模擬和CTL*_\setminus\bigcirc 等價 391
7.8.4 踏步互模擬求商 396
7.9 總結(jié) 404
7.10 文獻說明 404
7.11 習題 405
第8章 偏序約簡 414
8.1 動作的無關(guān)性 415
8.2 線性時間的充足集方法 421
8.2.1 充足集的條件 421
8.2.2 動態(tài)偏序約簡 431
8.2.3 計算充足集 436
8.2.4 靜態(tài)偏序約簡 442
8.3 分支時間的充足集方法 452
8.4 總結(jié) 460
8.5 文獻說明 461
8.6 習題 461
第9章 時控自動機 469
9.1 時控自動機述要 471
9.1.1 語義 476
9.1.2 時間發(fā)散、 時間鎖定 和芝諾性 481
9.2 時控計算樹邏輯 486
9.3 TCTL 模型檢驗 491
9.3.1 消去時間參數(shù) 492
9.3.2 區(qū)域遷移系統(tǒng) 494
9.3.3 TCTL 模型檢驗算法 511
9.4 總結(jié) 515
9.5 文獻說明 515
9.6 習題 516
第10章 概率系統(tǒng) 520
10.1 馬爾可夫鏈 521
10.1.1 可達性概率 530
10.1.2 定性性質(zhì) 539
10.2 概率計算樹邏輯 546
10.2.1 PCTL 模型檢驗 549
10.2.2 PCTL 的定性片段 551
10.3 線性時間性質(zhì) 557
10.4 PCTL* 和概率互模擬 565
10.4.1 PCTL* 565
10.4.2 概率互模擬 566
10.5 帶成本的馬爾可夫鏈 572
10.5.1 成本有界可達性 573
10.5.2 長遠性質(zhì) 580
10.6 馬爾可夫決策過程 584
10.6.1 可達性概率 597
10.6.2 PCTL 模型檢驗 608
10.6.3 極限性質(zhì) 611
10.6.4 線性時間性質(zhì)和PCTL* 619
10.6.5 公平性 622
10.7 總結(jié) 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
展開全部
模型檢驗原理(清華計算機圖書譯叢) 作者簡介
趙光峰，男，1964年生，教授，博士，曾留學英國一年，主要研究方向為拓撲學、圖論、系統(tǒng)可信性自動驗證，發(fā)表學術(shù)論文30余篇，主編《Visual Basic 程序設(shè)計教程》（高等教育出版社）等教材5部。
書友推薦
- >
李白與唐代文化
- >
月亮虎
- >
羅庸西南聯(lián)大授課錄
- >
推拿
- >
煙與鏡
- >
史學評論
- >
龍榆生：詞曲概論/大家小書
- >
我與地壇
本類暢銷
