| 作者 |
| [美]安德烈·普拉泽（André Platzer） |
| 丛书名 |
| 计算机科学丛书 |
| 出版社 |
| 机械工业出版社 |
| ISBN |
| 9787111685623 |
| 简要 |
| 简介 |
| 内容简介书籍计算机书籍 本书全面介绍如何采用逻辑与演绎语言推理信息物理系统。在这个过程中，读者将学习计算机科学、应用数学和控制论的许多基本概念，所有这些对了解CPS都是必不可少的。本书分为以下四个部分。在第1部分中，读者将学习如何对包含连续变量和编程构造的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 第8章 事件与响应168 8.1 引言168 8.2 对控制的需要169 8.2.1 控制中的事件170 8.2.2 事件检测171 8.2.3 划分世界174 8.2.4 触发事件177 8.2.5 事件触发的验证177 8.2.6 事件触发控制范式178 8.2.7 物理与控制的差别179 8.3 总结180 习题180 参考文献181 第9章 反应与延时182 9.1 引言182 9.2 控制中的延时183 9.2.1 延时对事件检测的影响185 9.2.2 模型预测控制基础186 9.2.3 以不变式设计187 9.2.4 划分反应的优先级顺序188 9.2.5 验证时间触发控制190 9.3 总结191 习题192 参考文献194 第二部分 微分方程分析 第10章 微分方程与微分不变式196 10.1 引言196 10.2 微分不变式的逐步介绍197 10.2.1 局部微分方程的全局描述能力197 10.2.2 微分不变式的直观理解198 10.2.3 微分不变式的推导199 10.3 微分201 10.3.1 微分的语法201 10.3.2 微分符号的语义201 10.3.3 微分项的语义204 10.3.4 用微分等式表示的导子引理205 10.3.5 微分项引理206 10.3.6 微分不变项公理207 10.3.7 微分替代引理208 10.4 微分不变项210 10.5 通过泛化得到的微分不变式证明210 10.6 证明示例211 10.7 总结213 10.8 附录214 10.8.1 微分方程与循环214 10.8.2 微分不变项和不变函数216 习题217 参考文献218 第11章 微分方程与证明220 11.1 引言220 11.2 简要回顾：微分方程证明的要素221 11.3 微分弱化222 11.4 微分不变式中的运算符223 11.4.1 等式微分不变式223 11.4.2 微分不变式证明规则224 11.4.3 微分不变不等式226 11.4.4 不等式微分不变式227 11.4.5 合取微分不变式228 11.4.6 析取微分不变式229 11.5 微分不变式230 11.6 证明示例232 11.7 假设不变式233 11.8 微分切割235 11.9 再次微分弱化238 11.10 可解微分方程的微分不变式239 11.11 总结240 11.12 附录：证明空气动力弹跳球241 习题244 参考文献245 第12章 幽灵与微分幽灵247 12.1 引言247 12.2 简要回顾249 12.3 幽灵变量的逐步介绍249 12.3.1 离散幽灵249 12.3.2 用“偷偷摸摸”的解证明弹跳球250 12.3.3 时间的微分幽灵254 12.3.4 构造微分幽灵255 12.4 微分幽灵257 12.5 替代幽灵261 12.6 空气动力球的极限速度261 12.7 公理体系幽灵263 12.8 总结264 12.9 附录265 12.9.1 算术幽灵265 12.9.2 非确定性赋值与幽灵的选择265 12.9.3 微分代数幽灵267 习题268 参考文献269 第13章 微分不变式与证明论270 13.1 引言270 13.2 简要回顾272 13.3 比较演绎研究：证明的相对论272 13.4 微分不变式的等价性273 13.5 微分不变式与算术274 13.6 微分不变等式275 13.7 等式不完备性277 13.8 严格的微分不变不等式278 13.9 将微分不变等式表述为微分不变不等式280 13.10 微分不变原子280 13.11 总结281 13.12 附录：不同范数和次数下的曲线运动281 习题283 参考文献283 第三部分 对抗式信息物理系统 第14章 混成系统与博弈286 14.1 引言286 14.2 混成博弈的逐步介绍288 14.2.1 选择与非确定性288 14.2.2 控制与对偶控制289 14.2.3 Demon的派生控制290 14.3 微分博弈逻辑的语法291 14.3.1 混成博弈291 14.3.2 微分博弈逻辑公式294 14.3.3 示例294 14.4 非形式化操作博弈树语义298 14.5 总结301 习题302 参考文献304 第15章 必胜策略与区域306 15.1 引言306 15.2 微分博弈逻辑的语义307 15.2.1 可达性关系的局限性307 15.2.2 微分博弈逻辑公式的集值语义307 15.2.3 混成博弈必胜区域的语义308 15.3 混成博弈中重复的语义312 15.3.1 有预告的重复312 15.3.2 无穷迭代的重复314 15.3.3 重复的膨胀语义316 15.3.4 隐式表征重复的必胜区域319 15.4 混成博弈的语义322 15.5 总结324 习题324 参考文献325 第16章 获胜与证明混成博弈326 16.1 引言326 16.2 语义考量327 16.2.1 单调性327 16.2.2 决定性328 16.3 混成博弈的动态公理329 16.3.1 决定性的动态公理329 16.3.2 单调性330 16.3.3 赋值的动态公理330 16.3.4 微分方程的动态公理331 16.3.5 挑战博弈的动态公理331 16.3.6 选择博弈的动态公理332 16.3.7 顺序博弈的动态公理333 16.3.8 对偶博弈的动态公理333 16.3.9 重复博弈的动态公理334 16.3.10 重复博弈的证明规则336 16.4 证明示例337 16.5 公理化339 16.5.1 可靠性340 16.5.2 完备性341 16.6 来来回回的博弈342 16.7 总结343 习题343 参考文献345 第17章 博弈证明与分离性347 17.1 引言347 17.2 简要回顾：混成博弈348 17.3 分离公理348 17.4 重复的尖括号模态——收敛对比迭代352 17.5 总结354 17.6 附录：关联微分博弈逻辑与微分动态逻辑354 习题355 参考文献356 第四部分 综合CPS正确性 第18章 公理与一致替换359 18.1 引言359 18.2 公理对比公理模式361 18.3 公理需要什么362 18.4 带解释的微分动态逻辑364 18.4.1 语法364 18.4.2 语义365 18.5 一致替换366 18.5.1 一致替换规则367 18.5.2 示例368 18.5.3 一致替换应用370 18.5.4 一致替换引理372 18.5.5 可靠性373 18.6 dL的公理体系证明演算374 18.7 微分公理375 18.8 总结376 18.9 附录：规则和证明的一致替换376 习题377 参考文献379 第19章 已验证模型与已验证运行时确认380 19.1 引言380 19.2 必用模型的基本挑战381 19.3 运行时监控器383 19.4 模型遵从性385 19.5 可证明正确的监控器综合387 19.5.1 逻辑状态关系388 19.5.2 模型监控器389 19.5.3 构造即正确的综合390 19.6 总结391 习题391 参考文献392 第20章 虚拟替换与实方程393 20.1 引言393 20.2 构筑奇迹394 20.3 量词消除397 20.3.1 量词消除的同态归一化398 20.3.2 替换基础399 20.3.3 线性方程的项替换400 20.4 二次方的平方根虚拟替换402 20.4.1 平方根代数403 20.4.2 平方根虚拟替换405 20.5 优化408 20.6 总结408 20.7 附录：实代数几何409 习题410 参考文献411 第21章 虚拟替换与实算术414 21.1 引言414 21.2 简要回顾：二次方的平方根虚拟替换415 21.3 无穷大的虚拟替换415 21.4 无穷小的虚拟替换418 21.5 通过虚拟替换消除二次方的量词421 21.6 优化425 21.7 总结426 21.8 附录：半代数几何426 习题427 参考文献427 附录 运算符与公理429 索引432 |