本书全面介绍如何采用逻辑与演绎语言推理信息物理系统。在这个过程中，读者将学习计算机科学、应用数学和控制论的许多基本概念，所有这些对了解CPS都是必不可少的。本书分为以下四个部分。在第1部分中，读者将学习如何对包含连续变量和编程构造的CPS建模，如何描述需求规约，以及如何用证明规则检验模型是否满足需求。第二部分增加了对物理世界建模采用的微分方程。第三部分介绍了对手的概念，在控制系统中，对手可以通过噪声和其他干扰影响系统的周边环境。在存在对手的时候做决策意味着需要对较坏情况做好准备。第四部分进一步增加了如何在实际应用中对系统做严格而高效的推理，比如采用实算术和监控器条件。
从形式逻辑学的角度，深入讲解如何运用逻辑计算思维方式更好地设计与分析CPS
这本优秀的教材将信息物理系统的设计和分析与逻辑计算的思维方式有机结合在一起。本书的陈述方式堪称典范，它恰当平衡了严格的数学形式化与植根于系统设计实际问题的说明性案例研究等内容。
——Rajeev Alur，宾夕法尼亚大学
本书对信息物理系统做了精彩的介绍，从形式逻辑学的角度涵盖了计算机科学和控制论中的基本概念。大量教学示例、图示以及习题使得书中的理论栩栩如生。本书在正文以及每章的附录中提供了丰富的背景材料，这让本书具有自包含的特点，从而可以供所有层次的大学生使用。
——Goran Frehse，格勒诺布尔阿尔卑斯大学
信息物理系统越来越深入地影响我们的生活，作者针对这类系统的设计与控制开发了重要的工具。本书对于参与信息物理系统设计的计算机科学工作者、工程师以及数学家而言是“必读”的。
——Anil Nerode，康奈尔大学
信息物理系统源自计算与物理世界越来越广泛的交互，因此需要以合适的物理模型来丰富计算基础。本书以用于推动所开发的方法和工具的说明性示例和应用极好地平衡了为这一计算新时代建立基础的严格性。对于任何有志于针对信息物理系统发展一门现代计算系统科学的研究人员来说，本书都是必读的。
——George J.Pappas，宾夕法尼亚大学
这本教材对于信息物理系统而言具有决定性的意义，它用单一逻辑框架为这类系统的行为建立了形式化基础。相对于其他所有方法而言，Platzer的逻辑学脱颖而出，因为它以一致的方式同时处理了信息物理系统的离散和连续本质，并且也不惧于处理这类系统由于环境中的随机性、不确定性以及对抗智能体而引起的复杂行为。对于需要描述信息物理系统规约并验证其安全性的实践工程师而言，他的计算思维方法使得这一工作很容易理解。
——Jeannette M.Wing，哥伦比亚大学
计算机\网络
这本优秀的教材将信息物理系统的设计和分析与逻辑计算的思维方式有机结合在一起。本书的陈述方式堪称典范，它恰当平衡了严格的数学形式化与植根于系统设计实际问题的说明性案例研究等内容。
—— Rajeev Alur，宾夕法尼亚大学
本书对信息物理系统做了精彩的介绍，从形式逻辑学的角度涵盖了计算机科学和控制论中的基本概念。大量教学示例、图示以及习题使得书中的理论栩栩如生。本书在正文以及每章的附录中提供了丰富的背景材料，这让本书具有自包含的特点，从而可以供所有层次的大学生使用。
—— Goran Frehse，格勒诺布尔阿尔卑斯大学
信息物理系统越来越深入地影响我们的生活，作者针对这类系统的设计与控制开发了重要的工具。本书对于参与设计信息物理系统的计算机科学工作者、工程师以及数学家而言是必读著作。
—— Anil Nerode，康奈尔大学
信息物理系统源自计算与物理世界越来越广泛的交互，因此需要以合适的物理模型来丰富计算基础。本书以用于推动所开发的方法和工具的说明性示例和应用极好地平衡了为这一计算新时代建立基础的严格性。对于任何有志于针对信息物理系统发展一门现代计算系统科学的研究人员来说，本书都是必读的。
—— George J. Pappas，宾夕法尼亚大学
这本教材对于信息物理系统而言具有决定性的意义，它用单一逻辑框架为这类系统的行为建立了形式化基础。相对于其他所有方法而言，Platzer的逻辑学脱颖而出，因为它以一致的方式同时处理了信息物理系统的离散和连续本质，并且也不惧于处理这类系统由于环境中的随机性、不确定性以及对抗智能体而引起的复杂行为。对于需要描述信息物理系统规约并验证其安全性的实践工程师而言，他的计算思维方法使得这一工作很容易理解。
—— Jeannette M. Wing，哥伦比亚大学
两年前我们第一次接触到本书时是相当惊喜的，我们从事信息物理系统的教学和研究多年，但一直苦于缺乏合适的教材来系统而有效地讲述这类系统的特点和基础知识。这也许有如下几个原因。其一，信息物理系统是一个相对新兴的概念（由美国国家科学基金的Helen Gill等在2006年提出），对其中许多科学问题的研究还处于比较初级的阶段。其二，信息物理系统涵盖的内容非常广，从控制理论到计算机科学的方方面面。其三，这类系统产生的应用也非常多样而且各具特点，从天上的飞机到移植于人体内的微型医疗设备等。依我们的浅见，目前有关信息物理系统的其他书籍大都侧重于某一方面、某一类应用的具体技术，在基础性和通用性上难免有所欠缺。
本书恰好对此做了有益的补充。本书从逻辑基础的角度深入介绍信息物理系统，就系统性、严格性而言，无出其右。本书的写作风格也特别适合教学：书中包含大量示例，以及对背景材料（以注解、探索和附录的形式）的简短而通俗的补充说明和讨论。这样，即使本书中涉及某些相对高等的数学概念（如实代数几何），读者也无须太多前期知识即可理解。因此本书既适合作为计算机、控制、电子、通信等多学科研究生教材，也可以作为本科生相关专业的高年级教材。
从科研的角度而言，我们认为本书也是信息物理系统从业者必读的参考书。本书采用的方法可归于形式化方法中的自动定理证明，即利用计算机进行严格的自动推理来证明系统的性质。理解信息物理系统中的数理逻辑显然是大有裨益的。考虑到信息物理系统的安全关键性，这一点尤为必要。当然，这并不表明我们主张本书中的方法能解决所有信息物理系统中的问题。毕竟不是所有的工程问题都能用严格的逻辑推理来证明。但谁又能否认逻辑对于工程的基础作用呢？
以下是关于逻辑学的一个有趣的事实。为了提高人们对逻辑学的重要性的认识，联合国教科文组织确定，从2019年开始，将每年的1月14日定为世界逻辑日，以此纪念两位逻辑学大师——哥德尔的忌日以及塔斯基的生日均为1月14日。这也让逻辑学成为继统计学和哲学之后第三个联合国教科文组织认同的学科节日。哥德尔和塔斯基的理论也在本书中频繁提及，比如哥德尔的不完备性理论，塔斯基的一阶实算术的可判定性定理等。
本书作者——卡内基·梅隆大学（CMU）计算机系的André Platzer教授在读博期间发展了书中大部分的理论框架，其博士工作的系统性令人惊叹。他也因此获得了2009年美国计算机协会（ACM）最佳博士论文奖提名（全世界仅3名）。依照书中理论及其扩展，作者开发了一套具有深远影响的信息物理系统自动定理证明工具，并成功应用于一系列工业范例。这也让本书的使用尤为方便：读者不仅可以欣赏书中的理论，还可以动手使用相关工具尝试各种示例和实验。
从纯学术研究的角度而言，翻译工作是吃力不讨好的，毕竟学术水平的评判侧重于工作的原创性。但是我们同时也是教育工作者，我们真诚希望广大读者，尤其刚刚进入信息物理系统这一领域的学生能从这本书中获益。从这一角度来讲，对我们工作的回报又是无价的。
我们在翻译过程中尽可能采取直译并侧重其中的逻辑正确性，一是为了更好地体现原著的思想和风格，二是因为书中的理论以及写作已经是“严清美”（严格、清晰、优美）了。但译文中出现的错误和不足之处在所难免，敬请大家不吝赐教。
本书最终的译稿主要由曾海波完成，李仁发负责了初译及校对组织工作。湖南大学嵌入式与网络计算省重点实验室的硕士班部分同学（2018级的王起凤、蒋汝成、何滟、鲍志学、龙皓剑、程希文和2019级的龚用顶、肖想珍）做了前期初译及校对工作。同时，我们在翻译过程中得到了作者André Platzer教授以及他的学生Yong Kiam Tan和Brandon Bohrer的耐心解答与帮助，在此一并感谢。
本书还得到国家自然科学基金资助项目（项目批准号：61932010）的支持。
曾海波、李仁发
2020年9月
我第一次遇到André时，他刚完成博士学业并在卡内基·梅隆大学（CMU）做应聘学术报告（他拿到了那份工作），而我当时正在那里做访问学者。我得以与这位年轻的教职候选人共进午餐。André谈到他用“微分动态逻辑”和定理证明的方法验证信息物理系统（CyberPhysical System，CPS）。我当时表示怀疑，其一是相关的方法过去不算太成功，其二是我把宝押在另外的方法上。几年前，我已经开发了一个模型检验工具（PHAVer），并且还在开发一个名为SpaceEx的工具。当时，只有这两个验证工具可以做到一键式验证某些CPS及其他领域内包含随时间变化的连续变量的基准测试程序。我对此非常自豪，也认为算法验证（algorithmic verification）才行之有效。但是André下定决心让定理证明这一方法能够实用，而且他也真的将这一领域推进到了我以前认为不可能的程度。André和他的团队首先开发了一套逻辑框架，然后构建了一个非常强大的CPS定理证明器（KeYmaera），成功地将其应用于飞机防撞系统等工业界案例，最后解决了运行时模型确认等重要的应用问题。
本书呈现在读者面前的是对采用逻辑与演绎语言推理信息物理系统的全面介绍。在这个过程中，读者将熟悉计算机科学、应用数学和控制论的许多基本概念，所有这些对了解CPS都是必不可少的。本书在许多章节的正文和附录中提供了必需的背景材料，因此可以在没有太多前期知识的情况下阅读。本书分为四个部分。在第一部分中，读者将学习如何对包含连续变量和编程构造的CPS建模，如何描述需求规约，以及如何用证明规则检验模型是否满足需求。第二部分增加了用于建模物理世界的微分方程。第三部分介绍了对手的概念，对手采取的动作是系统不能直接控制的。在控制系统中，对手可以是通过噪声和其他干扰影响系统的周边环境。在存在对手的时候做决策意味着需要对最坏情况做好准备。第四部分增加了用于在实际应用中对系统做严格而高效推理的更多要素，比如采用实算术和我最爱的监控器条件。监控器条件将在系统运行时检验。只要这些条件符合，就可以确定不仅模型满足安全需求，而且实际的CPS实现也满足安全需求。到目前为止，André和他的团队处理的案例之多令人印象深刻，这超出了我所知道的任何模型检验工具的能力。幸运的是，我和我的方法反过来也是如此，因为有些问题在实践中只能用算法的方法求得数值解。如果你的目标是从逻辑学的美观和优雅的角度获得CPS坚如磐石的基础，那么这本书就是适合你的书。
Goran Frehse
格勒诺布尔阿尔卑斯大学副教授
2017年
赞誉
译者序
推荐序
致谢
第1章 信息物理系统概述1
1.1 引言1
1.1.1 举例分析信息物理系统1
1.1.2 应用领域2
1.1.3 意义2
1.1.4 安全的重要性3
1.2 混成系统与信息物理系统4
1.3 多动态系统5
1.4 如何学习信息物理系统6
1.5 信息物理系统的计算思维7
1.6 学习目标8
1.7 本书的结构9
1.8 总结12
参考文献12
第一部分 初等信息物理系统
第2章 微分方程与域18
2.1 引言18
2.2 作为连续物理过程模型的微分方程18
2.3 微分方程的含义20
2.4 微分方程示例的简短纲要21
2.5 微分方程的域26
2.6 连续程序的语法27
2.6.1 连续程序28
2.6.2 项28
2.6.3 一阶公式29
2.7 连续程序的语义30
2.7.1 项30
2.7.2 一阶公式31
2.7.3 连续程序34
2.8 总结35
2.9 附录35
2.9.1 存在性定理35
2.9.2 唯一性定理36
2.9.3 常系数线性微分方程37
2.9.4 延拓与连续依赖38
习题39
参考文献41
第3章 选择与控制42
3.1 引言42
3.2 混成程序的逐步介绍43
3.2.1 混成程序的离散变化43
3.2.2 混成程序的合成44
3.2.3 混成程序中的决策45
3.2.4 混成程序中的选择45
3.2.5 混成程序中的测试47
3.2.6 混成程序中的重复48
3.3 混成程序50
3.3.1 混成程序的语法50
3.3.2 混成程序的语义51
3.4 混成程序设计54
3.4.1 制动还是不制动，这是个问题54
3.4.2 选择的问题55
3.5 总结56
3.6 附录：机器人弯道运动建模56
习题58
参考文献61
第4章 安全性与契约63
4.1 引言63
4.2 CPS契约的逐步介绍64
4.2.1 弹跳球Quantum历险记64
4.2.2 Quantum如何在时间结构中发现裂缝67
4.2.3 Quantum怎样学会放气68
4.2.4 CPS的后置条件契约69
4.2.5 CPS的前置条件契约70
4.3 混成程序的逻辑公式71
4.4 微分动态逻辑73
4.4.1 微分动态逻辑的语法73
4.4.2 微分动态逻辑的语义75
4.5 逻辑形式的CPS契约77
4.6 查明CPS的需求78
4.7 总结82
4.8 附录82
4.8.1 顺序合成证明的中间条件82
4.8.2 选择的证明84
4.8.3 测试的证明85
习题86
参考文献90
第5章 动态系统与动态公理92
5.1 引言92
5.2 CPS的中间条件93
5.3 动态系统的动态公理95
5.3.1 非确定性选择的动态公理95
5.3.2 公理的可靠性97
5.3.3 赋值的动态公理98
5.3.4 微分方程的动态公理99
5.3.5 测试的动态公理101
5.3.6 顺序合成的动态公理102
5.3.7 循环的动态公理104
5.3.8 尖括号模态的公理105
5.4 短暂弹跳球的证明105
5.5 总结107
5.6 附录108
5.6.1 模态肯定前件在方括号模态中的蕴涵108
5.6.2 如果没有任何相关变化，则为空虚状态变化109
5.6.3 哥德尔将永真性泛化到方括号模态中109
5.6.4 后置条件的单调性110
5.6.5 自由变量和约束变量111
5.6.6 自由变量和约束变量分析111
习题113
参考文献116
第6章 真理与证明118
6.1 引言118
6.2 真理和证明119
6.2.1 相继式120
6.2.2 证明122
6.2.3 命题证明规则122
6.2.4 证明规则的可靠性126
6.2.5 动态的证明127
6.2.6 量词证明规则129
6.3 派生证明规则131
6.4 单跳弹跳球的相继式证明132
6.5 实算术证明规则133
6.5.1 实数量词消除法134
6.5.2 实例化实算术量词136
6.5.3 通过去除假设来弱化实算术137
6.5.4 相继式演算中的结构证明规则138
6.5.5 在公式中代入等式139
6.5.6 缩写项以降低复杂性139
6.5.7 创造性地切割实算术转化问题140
6.6 总结140
习题141
参考文献143
第7章 控制回路与不变式145
7.1 引言145
7.2 控制循环146
7.3 循环回路147
7.3.1 循环的归纳公理147
7.3.2 循环的归纳规则149
7.3.3 循环不变式150
7.3.4 上下文可靠性需求153
7.4 一个欢快重复的弹跳球的证明154
7.5 将后置条件拆分为单独的情况158
7.6 总结159
7.7 附录159
7.7.1 证明的循环159
7.7.2 打破证明循环161
7.7.3 循环的不变式证明163
7.7.4 归纳公理的替代形式163
习题165
参考文献166
第8章 事件与响应168
8.1 引言168
8.2 对控制的需要169
8.2.1 控制中的事件170
8.2.2 事件检测171
8.2.3 划分世界174
8.2.4 触发事件177
8.2.5 事件触发的验证177
8.2.6 事件触发控制范式178
8.2.7 物理与控制的差别179
8.3 总结180
习题180
参考文献181
第9章 反应与延时182
9.1 引言182
9.2 控制中的延时183
9.2.1 延时对事件检测的影响185
9.2.2 模型预测控制基础186
9.2.3 以不变式设计187
9.2.4 划分反应的优先级顺序188
9.2.5 验证时间触发控制190
9.3 总结191
习题192
参考文献194
第二部分 微分方程分析
第10章 微分方程与微分不变式196
10.1 引言196
10.2 微分不变式的逐步介绍197
10.2.1 局部微分方程的全局描述能力197
10.2.2 微分不变式的直观理解198
10.2.3 微分不变式的推导199
10.3 微分201
10.3.1 微分的语法201
10.3.2 微分符号的语义201
10.3.3 微分项的语义204
10.3.4 用微分等式表示的导子引理205
10.3.5 微分项引理206
10.3.6 微分不变项公理207
10.3.7 微分替代引理208
10.4 微分不变项210
10.5 通过泛化得到的微分不变式证明210
10.6 证明示例211
10.7 总结213
10.8 附录214
10.8.1 微分方程与循环214
10.8.2 微分不变项和不变函数216
习题217
参考文献218
第11章 微分方程与证明220
11.1 引言220
11.2 简要回顾：微分方程证明的要素221
11.3 微分弱化222
11.4 微分不变式中的运算符223
11.4.1 等式微分不变式223
11.4.2 微分不变式证明规则224
11.4.3 微分不变不等式226
11.4.4 不等式微分不变式227
11.4.5 合取微分不变式228
11.4.6 析取微分不变式229
11.5 微分不变式230
11.6 证明示例232
11.7 假设不变式233
11.8 微分切割235
11.9 再次微分弱化238
11.10 可解微分方程的微分不变式239
11.11 总结240
11.12 附录：证明空气动力弹跳球241
习题244
参考文献245
第12章 幽灵与微分幽灵247
12.1 引言247
12.2 简要回顾249
12.3 幽灵变量的逐步介绍249
12.3.1 离散幽灵249
12.3.2 用“偷偷摸摸”的解证明弹跳球250
12.3.3 时间的微分幽灵254
12.3.4 构造微分幽灵255
12.4 微分幽灵257
12.5 替代幽灵261
12.6 空气动力球的极限速度261
12.7 公理体系幽灵263
12.8 总结264
12.9 附录265
12.9.1 算术幽灵265
12.9.2 非确定性赋值与幽灵的选择265
12.9.3 微分代数幽灵267
习题268
参考文献269
第13章 微分不变式与证明论270
13.1 引言270
13.2 简要回顾272
13.3 比较演绎研究：证明的相对论272
13.4 微分不变式的等价性273
13.5 微分不变式与算术274
13.6 微分不变等式275
13.7 等式不完备性277
13.8 严格的微分不变不等式278
13.9 将微分不变等式表述为微分不变不等式280
13.10 微分不变原子280
13.11 总结281
13.12 附录：不同范数和次数下的曲线运动281
习题283
参考文献283
第三部分 对抗式信息物理系统
第14章 混成系统与博弈286
14.1 引言286
14.2 混成博弈的逐步介绍288
14.2.1 选择与非确定性288
14.2.2 控制与对偶控制289
14.2.3 Demon的派生控制290
14.3 微分博弈逻辑的语法291
14.3.1 混成博弈291
14.3.2 微分博弈逻辑公式294
14.3.3 示例294
14.4 非形式化操作博弈树语义298
14.5 总结301
习题302
参考文献304
第15章 必胜策略与区域306
15.1 引言306
15.2 微分博弈逻辑的语义307
15.2.1 可达性关系的局限性307
15.2.2 微分博弈逻辑公式的集值语义307
15.2.3 混成博弈必胜区域的语义308
15.3 混成博弈中重复的语义312
15.3.1 有预告的重复312
15.3.2 无穷迭代的重复314
15.3.3 重复的膨胀语义316
15.3.4 隐式表征重复的必胜区域319
15.4 混成博弈的语义322
15.5 总结324
习题324
参考文献325
第16章 获胜与证明混成博弈326
16.1 引言326
16.2 语义考量327
16.2.1 单调性327
16.2.2 决定性328
16.3 混成博弈的动态公理329
16.3.1 决定性的动态公理329
16.3.2 单调性330
16.3.3 赋值的动态公理330
16.3.4 微分方程的动态公理331
16.3.5 挑战博弈的动态公理331
16.3.6 选择博弈的动态公理332
16.3.7 顺序博弈的动态公理333
16.3.8 对偶博弈的动态公理333
16.3.9 重复博弈的动态公理334
16.3.10 重复博弈的证明规则336
16.4 证明示例337
16.5 公理化339
16.5.1 可靠性340
16.5.2 完备性341
16.6 来来回回的博弈342
16.7 总结343
习题343
参考文献345
第17章 博弈证明与分离性347
17.1 引言347
17.2 简要回顾：混成博弈348
17.3 分离公理348
17.4 重复的尖括号模态——收敛对比迭代352
17.5 总结354
17.6 附录：关联微分博弈逻辑与微分动态逻辑354
习题355
参考文献356
第四部分 综合CPS正确性
第18章 公理与一致替换359
18.1 引言359
18.2 公理对比公理模式361
18.3 公理需要什么362
18.4 带解释的微分动态逻辑364
18.4.1 语法364
18.4.2 语义365
18.5 一致替换366
18.5.1 一致替换规则367
18.5.2 示例368
18.5.3 一致替换应用370
18.5.4 一致替换引理372
18.5.5 可靠性373
18.6 dL的公理体系证明演算374
18.7 微分公理375
18.8 总结376
18.9 附录：规则和证明的一致替换376
习题377
参考文献379
第19章 已验证模型与已验证运行时确认380
19.1 引言380
19.2 必用模型的基本挑战381
19.3 运行时监控器383
19.4 模型遵从性385
19.5 可证明正确的监控器综合387
19.5.1 逻辑状态关系388
19.5.2 模型监控器389
19.5.3 构造即正确的综合390
19.6 总结391
习题391
参考文献392
第20章 虚拟替换与实方程393
20.1 引言393
20.2 构筑奇迹394
20.3 量词消除397
20.3.1 量词消除的同态归一化398
20.3.2 替换基础399
20.3.3 线性方程的项替换400
20.4 二次方的平方根虚拟替换402
20.4.1 平方根代数403
20.4.2 平方根虚拟替换405
20.5 优化408
20.6 总结408
20.7 附录：实代数几何409
习题410
参考文献411
第21章 虚拟替换与实算术414
21.1 引言414
21.2 简要回顾：二次方的平方根虚拟替换415
21.3 无穷大的虚拟替换415
21.4 无穷小的虚拟替换418
21.5 通过虚拟替换消除二次方的量词421
21.6 优化425
21.7 总结426
21.8 附录：半代数几何426
习题427
参考文献427
附录 运算符与公理429
索引432
