掃一掃
關注中圖網
官方微博
本類五星書更多>
-
>
全國計算機等級考試最新真考題庫模擬考場及詳解·二級MSOffice高級應用
-
>
決戰行測5000題(言語理解與表達)
-
>
軟件性能測試.分析與調優實踐之路
-
>
第一行代碼Android
-
>
JAVA持續交付
-
>
EXCEL最強教科書(完全版)(全彩印刷)
-
>
深度學習
模型檢驗原理(清華計算機圖書譯叢) 版權信息
- ISBN：9787302577355
- 條形碼：9787302577355 ; 978-7-302-57735-5
- 裝幀：70g膠版紙
- 冊數：暫無
- 重量：暫無
- 所屬分類：>
模型檢驗原理(清華計算機圖書譯叢) 本書特色
1．內容全面，條理系統。 2．實例豐富，便于理解。 3．理論充實，實踐性強4．文獻翔實，脈絡清晰。 5．習題充足，利于掌握。 6．附錄凝練，入門快速。 本書是全面、系統地介紹模型檢驗原理及其應用的鴻篇巨著。
模型檢驗原理(清華計算機圖書譯叢) 內容簡介
本書全面系統地介紹了模型檢驗的一般原理、應用工具及軟硬件系統的建模與驗證方法，同時介紹了克服模型檢驗中“狀態空間爆炸”問題的有效途徑，可作為計算機科學與技術、軟件工程等專業本科生、研究生的教材，也可作為模型檢驗領域研究人員及注重系統可靠性的設計與開發人員的參考書。
模型檢驗原理(清華計算機圖書譯叢) 目錄
目 錄
第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
展開全部
模型檢驗原理(清華計算機圖書譯叢) 作者簡介
趙光峰，男，1964年生，教授，博士，曾留學英國一年，主要研究方向為拓撲學、圖論、系統可信性自動驗證，發表學術論文30余篇，主編《Visual Basic 程序設計教程》（高等教育出版社）等教材5部。
書友推薦
- >
新文學天穹兩巨星--魯迅與胡適/紅燭學術叢書(紅燭學術叢書)
- >
李白與唐代文化
- >
大紅狗在馬戲團-大紅狗克里弗-助人
- >
推拿
- >
山海經
- >
伊索寓言-世界文學名著典藏-全譯本
- >
人文閱讀與收藏·良友文學叢書:一天的工作
- >
朝聞道
本類暢銷
