书籍详情

信息物理系统逻辑基础

信息物理系统逻辑基础

作者:[美] 安德烈·普拉泽(André Platzer) 著,曾海波 李仁发译 译

出版社:机械工业出版社

出版时间:2021-08-01

ISBN:9787111685623

定价:¥179.00

购买这本书可以去
内容简介
  本书全面介绍如何采用逻辑与演绎语言推理信息物理系统。在这个过程中,读者将学习计算机科学、应用数学和控制论的许多基本概念,所有这些对了解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
猜您喜欢

读书导航