本书全面介绍如何采用逻辑与演绎语言推理信息物理系统。在这个过程中，读者将学习计算机科学、应用数学和控制论的许多基本概念，所有这些对了解CPS都是必不可少的。本书分为以下四个部分。在第1部分中，读者将学习如何对包含连续变量和编程构造的CPS建模，如何描述需求规约，以及如何用证明规则检验模型是否满足需求。第二部分增加了对物理世界建模采用的微分方程。第三部分介绍了对手的概念，在控制系统中，对手可以通过噪声和其他干扰影响系统的周边环境。在存在对手的时候做决策意味着需要对较坏情况做好准备。第四部分进一步增加了如何在实际应用中对系统做严格而高效的推理，比如采用实算术和监控器条件。

本书基于作者在卡内基·梅隆大学计算机科学系讲授的 信息物理系统基础课程的讲义撰写而成。在许多章节的正文和附录中提供了必需的背景材料，因此读者可以在没有太多预备知识的情况下阅读。
本书分为四个部分。部分是对初等信息物理系统的概述，讲解了如何对包含连续变量和编程构造的CPS建模，如何描述需求规约，以及如何用证明规则检验模型是否满足需求。第二部分增加了用于建模物理世界的微分方程，介绍微分不变式、微分方程的证明以及微分幽灵等内容。第三部分围绕对抗性信息物理系统进行详细的解说，用示例阐述混成程序、混成系统、混成博弈、必胜策略等相关概念和公理。第四部分进一步增加了在实际应用中综合CPS正确性的内容，以对系统做严格而高效的推理，涉及的内容有一致替换、虚拟替换、量词消除和监控器等。

赞誉
译者序
推荐序
致谢
第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