本书系统阐述了计算机科学和软件工程中形式语言、自动机、形式逻辑、软件系统建模和验证等核心理论与方法。全书从基础知识开始，介绍了有限自动机、正则表示与正则语言、上下文无关文法、下推自动机与上下文无关语言、图灵机与计算模型，深入探讨问题的可判定性与计算复杂性、命题逻辑、谓词逻辑和时序逻辑，并进一步扩展至软件形式化建模与验证和抽象解释等相关领域。
　　本书知识体系连贯、结构严谨，叙述与证明简洁，注重理论推导的同时兼顾实际应用。内容编排循序渐进，尝试架构软件基础知识体系，使复杂概念的表述和推理更加清晰、准确和易懂，对应课程于2020年入选教育部“国家级一流本科课程”。


更多科学出版社服务，请扫码获取。

1992-07，毕业于中科院系统所，获博士学位。 1992起，在清华大学从事教学与科研工作。从1992年起，在清华大学从事教学和科研，教学的课程有10多门，如：形式语言与自动机、软件理论基础、数据建模、人工智能基础、自动机与形式逻辑、软件工程探索、数据科学导论、系统辨识、自适应控制等，教学课程多次被学生教评学校top 5%.2020年教育部国家级一流本科课程 2024年人工智能学会教学成果一等奖

目录
第1章 基础知识 1
1.1 数学结构 1
1.1.1 集合与映射 1
1.1.2 图结构 3
1.1.3 同构与同态 3
1.2 符号逻辑 4
1.2.1 逻辑概念与运算 5
1.2.2 运算的性质与量词 5
1.3 证明方法 6
1.3.1 演绎法 7
1.3.2 反证法 8
1.3.3 数学归纳法 8
1.3.4 鸽巢原理 10
1.4 语言 11
1.4.1 语言的结构 11
1.4.2 语言的运算 12
1.5 形式文法 13
1.5.1 文法的概念 13
1.5.2 文法的定义与类型 14
1.5.3 文法的语言 15
小结 16
练习 16
第2章 有限自动机 18
2.1 确定有限自动机 18
2.1.1 确定有限自动机的概念 18
2.1.2 确定有限自动机的定义 19
2.1.3 DFA状态转移函数的扩展 20
2.1.4 正则语言 21
2.1.5 自动机的积 24
2.2 非确定有限自动机 24
2.2.1 非确定有限自动机的概念 24
2.2.2 非确定有限自动机的定义 25
2.2.3 NFA状态转移函数的扩展 26
2.2.4 NFA与DFA的关系 27
2.3 有限自动机的应用 32
小结 35
练习 35
第3章 正则语言与表示 37
3.1 正则语言运算的封闭性 37
3.1.1 单一终态的NFA 37
3.1.2 正则语言的运算性质 38
3.2 正则表示 40
3.2.1 正则表示的文法 40
3.2.2 正则表示的语义 41
3.3 正则表示与正则语言 42
3.3.1 自动机的扩展 42
3.3.2 正则表示的构造 43
3.3.3 正则表示与正则语言的关系 47
3.3.4 正则表示的代数律 48
3.4 正则语言的同态 49
3.5 正则表示的应用 51
3.5.1 UNIX正则表示 52
3.5.2 应用实例 53
3.6 正则文法 53
小结 56
练习 56
第4章 正则语言的判定性质与优化算法 59
4.1 正则语言的判定性质 59
4.1.1 正则语言与元素的关系 59
4.1.2 属性检测 60
4.2 泵引理 61
4.2.1 泵引理介绍 61
4.2.2 泵引理的应用 62
4.3 自动机的优化 63
4.3.1 状态集上的关系 63
4.3.2 填表算法 64
4.3.3 最小化的DFA 66
小结 67
练习 67
第5章 上下文无关文法和语言 69
5.1 上下文无关文法的概念 69
5.2 文法的推理 69
5.2.1 递归推理与推导 70
5.2.2 最左推导与最右推导 71
5.3 语法分析树 71
5.3.1 语法分析树介绍 71
5.3.2 文法推理与分析树的关系 73
5.4 上下文无关语言与上下文无关文法 73
5.4.1 上下文无关语言 73
5.4.2 上下文无关文法的构造 75
5.5 上下文无关文法的应用 77
5.5.1 形式定义中的应用 77
5.5.2 语法分析器 78
5.5.3 标记语言 80
5.6 二义文法 83
5.6.1 二义文法的概念 84
5.6.2 文法二义性的消除法 85
5.6.3 固有二义语言 87
小结 88
练习 89
第6章 下推自动机 91
6.1 下推自动机的概念 91
6.1.1 下推自动机的介绍 91
6.1.2 下推自动机的定义 92
6.1.3 下推自动机的即时描述 95
6.2 PDA的语言 97
6.2.1 终态型PDA语言 97
6.2.2 空栈型PDA语言 97
6.2.3 PDA的语言表示 98
6.3 PDA与CFG的关系 101
6.3.1 从CFG构造PDA 101
6.3.2 从PDA构造CFG 102
6.3.3 PDA与CFG的等价性 104
6.4 确定的下推自动机 105
6.4.1 确定PDA的概念 105
6.4.2 DPDA语言与正则语言 108
6.4.3 确定PDA与二义文法 108
小结 109
练习 110
第7章 上下文无关语言的性质 112
7.1 CFG的规范 112
7.1.1 变量替换 112
7.1.2 CFG的简化 113
7.1.3 Chomsky范式 119
7.2 CFL的泵引理及运算性质 121
7.2.1 CFL泵引理 121
7.2.2 CFL运算的封闭性 123
7.2.3 CFL“交”运算性质 127
7.3 CFL的判定性质 130
7.3.1 空语言和无限语言 130
7.3.2 CFL与字符串 131
小结 133
练习 133
第8章 图灵机 136
8.1 图灵机的概念 136
8.1.1 图灵机的介绍 136
8.1.2 图灵机的定义 138
8.1.3 图灵机的即时描述和语言 140
8.2 图灵机的计算 144
8.2.1 图灵机的计算设计 144
8.2.2 图灵机的编程技术 146
8.3 图灵机的扩展 149
8.3.1 等价证明 149
8.3.2 图灵机带的扩展 150
8.3.3 图灵机移动的扩展 153
8.3.4 受限图灵机 157
8.3.5 TM的文法 158
8.4 图灵机与其他自动机的关系 158
8.4.1 TM与PDA 158
8.4.2 TM与计算机 161
小结 162
练习 162
第9章 判定性问题 166
9.1 TM语言的性质 166
9.1.1 编码TM 166
9.1.2 TM语言的补 169
9.2 问题的判定性质 171
9.2.1 问题与语言 171
9.2.2 不可判定问题 173
9.3 POST对应问题 176
9.3.1 POST对应问题介绍 177
9.3.2 GPOST对应问题 179
9.3.3 CFG二义性的判定 181
9.4 计算复杂性 183
9.4.1 时间复杂度 183
9.4.2 可满足性问题 187
小结 188
练习 188
第10章 命题逻辑 192
10.1 命题逻辑介绍 192
10.1.1 基本符号 192
10.1.2 命题逻辑的文法 193
10.2 命题逻辑的语义 193
10.2.1 命题的解释 193
10.2.2 命题的模型 194
10.2.3 命题运算的规则与性质 195
10.2.4 命题的范式 195
10.3 命题逻辑中的证明 196
10.3.1 证明系统介绍 196
10.3.2 演绎系统介绍 198
小结 199
练习 200
第11章 一阶逻辑 202
11.1 一阶逻辑介绍 202
11.1.1 个体词与谓词 202
11.1.2 量词与作用域 203
11.1.3 一阶逻辑的文法 204
11.1.4 一阶逻辑的语义 207
11.1.5 一阶逻辑的替换 208
11.2 一阶逻辑的证明系统 210
11.2.1 一阶逻辑的推理 210
11.2.2 一阶逻辑的属性 213
11.3 一阶逻辑比较 214
11.3.1 一阶逻辑与命题逻辑 214
11.3.2 一阶逻辑与高阶逻辑 215
小结 215
练习 216
第12章 时序逻辑 219
12.1 线性时序逻辑 219
12.1.1 Kripke结构 219
12.1.2 线性时序逻辑介绍 220
12.2 LTL公式转换与属性描述 222
12.2.1 LTL公式转换 222
12.2.2 LTL属性描述 223
12.3 计算树逻辑 224
12.3.1 CTL文法 224
12.3.2 CTL语义 225
12.4 CTL公式转换与属性描述 227
12.4.1 CTL公式转换 227
12.4.2 CTL属性描述 227
12.5 LTL与CTL 229
12.5.1 LTL与CTL的关系 229
12.5.2 时序逻辑的扩展 230
小结 231
练习 231
第13章 软件形式化建模与验证 235
13.1 软件的形式化方法 235
13.1.1 软件可靠性面临的挑战 235
13.1.2 形式化方法 236
13.2 时间自动机 237
13.2.1 时间自动机介绍 237
13.2.2 时间自动机结构 238
13.3 Büchi自动机 240
13.3.1 Büchi自动机介绍 241
13.3.2 LTL到BA的转换 242
13.4 软件的验证 243
13.4.1 定理证明 243
13.4.2 模型检测 245
小结 249
练习 249
第14章 抽象解释 252
14.1 抽象解释理论 252
14.1.1 抽象解释简介 252
14.1.2 Galois连接 253
14.2 抽象逼近 254
14.2.1 最优抽象逼近 254
14.2.2 不动点理论 255
14.2.3 收敛算子 255
14.3 形式语义的抽象 257
14.3.1 迁移系统 257
14.3.2 迁移系统的语义 258
14.3.3 语义抽象分析 261
14.4 形式化方法的应用 263
14.4.1 状态空间抽象 263
14.4.2 MVB形式化建模与实现 266
小结 270
练习 270
参考文献 272