目   录

第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