模型检验原理(清华计算机图书译丛)

目 录 第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