《信息物理系统逻辑基础》安德烈・普拉泽 | PDF下载|ePub下载

创建

2024 年 10 月 29 日

查看

类别: 计算机/网络

信息物理系统逻辑基础版权信息

出版社：机械工业出版社
出版时间：2021-08-01
ISBN：9787111685623
条形码：9787111685623 ; 978-7-111-68562-3

信息物理系统逻辑基础本书特色

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

信息物理系统逻辑基础内容简介

本书全面介绍如何采用逻辑与演绎语言推理信息物理系统。在这个过程中，读者将学习计算机科学、应用数学和控制论的许多基本概念，所有这些对了解CPS都是必不可少的。本书分为以下四个部分。在第1部分中，读者将学习如何对包含连续变量和编程构造的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

信息物理系统逻辑基础作者简介

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