作者：安德烈·普拉泽
页数：452
出版社：机械工业出版社
出版日期：2021
ISBN：9787111685623
电子书格式：pdf/epub/txt
内容简介
本书全面介绍如何采用逻辑与演绎语言推理信息物理系统。在这个过程中，读者将学习计算机科学、应用数学和控制论的许多基本概念，所有这些对了解CPS都是必不可少的。本书分为以下四个部分。在第1部分中，读者将学习如何对包含连续变量和编程构造的CPS建模，如何描述需求规约，以及如何用证明规则检验模型是否满足需求。第二部分增加了对物理世界建模采用的微分方程。第三部分介绍了对手的概念，在控制系统中，对手可以通过噪声和其他干扰影响系统的周边环境。在存在对手的时候做决策意味着需要对较坏情况做好准备。第四部分进一步增加了如何在实际应用中对系统做严格而高效的推理，比如采用实算术和监控器条件。
作者简介
安德烈·普拉泽（André Platzer） 卡内基·梅隆大学计算机科学系教授。他拥有德国奥尔登堡大学的博士学位。研究领域包括形式化方法、编程语言和纯逻辑与应用逻辑。他曾于2009年获得ACM最佳博士论文荣誉提名奖，2011年获得NSF杰出青年奖，并入选美国Popular Science杂志2009年“十大杰出青年科学家”、IEEE Intelligent Systems杂志2010年“AI十大潜力人物”。
本书特色
适读人群 ：本书可作为高等院校信息物理系统相关课程的本科生或者研究生教材，也可供对信息物理系统感兴趣的读者阅读。本书基于作者在卡内基·梅隆大学计算机科学系讲授的 “信息物理系统基础”课程的讲义撰写而成。在许多章节的正文和附录中提供了必需的背景材料，因此读者可以在没有太多预备知识的情况下阅读。本书分为四个部分。第一部分是对初等信息物理系统的概述，讲解了如何对包含连续变量和编程构造的CPS建模，如何描述需求规约，以及如何用证明规则检验模型是否满足需求。第二部分增加了用于建模物理世界的微分方程，介绍微分不变式、微分方程的证明以及微分幽灵等内容。第三部分围绕对抗性信息物理系统进行详细的解说，用示例阐述混成程序、混成系统、混成博弈、必胜策略等相关概念和公理。第四部分进一步增加了在实际应用中综合CPS正确性的内容，以对系统做严格而高效的推理，涉及的内容有一致替换、虚拟替换、量词消除和监控器等。
目录
译者序
推荐序
致谢
第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
