信息物理系统逻辑基础

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

　　安德烈·普拉泽（André Platzer） 卡内基·梅隆大学计算机科学系教授。他拥有德国奥尔登堡大学的博士学位。研究领域包括形式化方法、编程语言和纯逻辑与应用逻辑。他曾于2009年获得ACM最佳博士论文荣誉提名奖，2011年获得NSF杰出青年奖，并入选美国Popular Science杂志2009年“十大杰出青年科学家”、IEEE Intelligent Systems杂志2010年“AI十大潜力人物”。

赞誉
译者序
推荐序
致谢
第1章　信息物理系统概述1
　11　引言1
　　111　举例分析信息物理系统1
　　112　应用领域2
　　113　意义2
　　114　安全的重要性3
　12　混成系统与信息物理系统4
　13　多动态系统5
　14　如何学习信息物理系统6
　15　信息物理系统的计算思维7
　16　学习目标8
　17　本书的结构9
　18　总结12
　参考文献12
第一部分　初等信息物理系统
第2章　微分方程与域18
　21　引言18
　22　作为连续物理过程模型的微分方程18
　23　微分方程的含义20
　24　微分方程示例的简短纲要21
　25　微分方程的域26
　26　连续程序的语法27
　　261　连续程序28
　　262　项28
　　263　一阶公式29
　27　连续程序的语义30
　　271　项30
　　272　一阶公式31
　　273　连续程序34
　28　总结35
　29　附录35
　　291　存在性定理35
　　292　唯一性定理36
　　293　常系数线性微分方程37
　　294　延拓与连续依赖38
　习题39
　参考文献41
第3章　选择与控制42
　31　引言42
　32　混成程序的逐步介绍43
　　321　混成程序的离散变化43
　　322　混成程序的合成44
　　323　混成程序中的决策45
　　324　混成程序中的选择45
　　325　混成程序中的测试47
　　326　混成程序中的重复48
　33　混成程序50
　　331　混成程序的语法50
　　332　混成程序的语义51
　34　混成程序设计54
　　341　制动还是不制动，这是个问题54
　　342　选择的问题55
　35　总结56
　36　附录：机器人弯道运动建模56
　习题58
　参考文献61
第4章　安全性与契约63
　41　引言63
　42　CPS契约的逐步介绍64
　　421　弹跳球Quantum历险记64
　　422　Quantum如何在时间结构中发现裂缝67
　　423　Quantum怎样学会放气68
　　424　CPS的后置条件契约69
　　425　CPS的前置条件契约70
　43　混成程序的逻辑公式71
　44　微分动态逻辑73
　　441　微分动态逻辑的语法73
　　442　微分动态逻辑的语义75
　45　逻辑形式的CPS契约77
　46　查明CPS的需求78
　47　总结82
　48　附录82
　　481　顺序合成证明的中间条件82
　　482　选择的证明84
　　483　测试的证明85
　习题86
　参考文献90
第5章　动态系统与动态公理92
　51　引言92
　52　CPS的中间条件93
　53　动态系统的动态公理95
　　531　非确定性选择的动态公理95
　　532　公理的可靠性97
　　533　赋值的动态公理98
　　534　微分方程的动态公理99
　　535　测试的动态公理101
　　536　顺序合成的动态公理102
　　537　循环的动态公理104
　　538　尖括号模态的公理105
　54　短暂弹跳球的证明105
　55　总结107
　56　附录108
　　561　模态肯定前件在方括号模态中的蕴涵108
　　562　如果没有任何相关变化，则为空虚状态变化109
　　563　哥德尔将永真性泛化到方括号模态中109
　　564　后置条件的单调性110
　　565　自由变量和约束变量111
　　566　自由变量和约束变量分析111
　习题113
　参考文献116
第6章　真理与证明118
　61　引言118
　62　真理和证明119
　　621　相继式120
　　622　证明122
　　623　命题证明规则122
　　624　证明规则的可靠性126
　　625　动态的证明127
　　626　量词证明规则129
　63　派生证明规则131
　64　单跳弹跳球的相继式证明132
　65　实算术证明规则133
　　651　实数量词消除法134
　　652　实例化实算术量词136
　　653　通过去除假设来弱化实算术137
　　654　相继式演算中的结构证明规则138
　　655　在公式中代入等式139
　　656　缩写项以降低复杂性139
　　657　创造性地切割实算术转化问题140
　66　总结140
　习题141
　参考文献143
第7章　控制回路与不变式145
　71　引言145
　72　控制循环146
　73　循环回路147
　　731　循环的归纳公理147
　　732　循环的归纳规则149
　　733　循环不变式150
　　734　上下文可靠性需求153
　74　一个欢快重复的弹跳球的证明154
　75　将后置条件拆分为单独的情况158
　76　总结159
　77　附录159
　　771　证明的循环159
　　772　打破证明循环161
　　773　循环的不变式证明163
　　774　归纳公理的替代形式163
　习题165
　参考文献166