信息物理系统逻辑基础

信息物理系统逻辑基础
分享
扫描下方二维码分享到微信
打开微信,点击右上角”+“,
使用”扫一扫“即可将网页分享到朋友圈。
作者: [美] (André Platzer)
2021-08
版次: 1
ISBN: 9787111685623
定价: 179.00
装帧: 其他
开本: 16开
纸张: 胶版纸
字数: 410千字
4人买过
  • 本书全面介绍如何采用逻辑与演绎语言推理信息物理系统。在这个过程中,读者将学习计算机科学、应用数学和控制论的许多基本概念,所有这些对了解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
  • 内容简介:
    本书全面介绍如何采用逻辑与演绎语言推理信息物理系统。在这个过程中,读者将学习计算机科学、应用数学和控制论的许多基本概念,所有这些对了解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
查看详情
12
相关图书 / 更多
信息物理系统逻辑基础
信息系统监理师教程(第2版)
贾卓生、张树玲、李京、吕小刚、陈兵
信息物理系统逻辑基础
信息论基础
翟明岳
信息物理系统逻辑基础
信息系统分析与设计
熊伟、陈浩、陈荦
信息物理系统逻辑基础
信息系统项目管理师案例分析一本通(第二版)
王树文
信息物理系统逻辑基础
信息差:看透大数据背后的底层逻辑
(英) 保罗·古德温 著,文通天下 出品
信息物理系统逻辑基础
信息安全法研究(第二版)
马民虎 方婷著
信息物理系统逻辑基础
信息可视化设计
周承君、姜朝阳、王之娇 著
信息物理系统逻辑基础
信息检索与深度学习
郭嘉丰 兰艳艳 程学旗
信息物理系统逻辑基础
信息系统监理师考试大纲
全国计算机专业技术资格考试办公室
信息物理系统逻辑基础
信息处理技术员考试32小时通关
薛大龙 编
信息物理系统逻辑基础
信息助推,或适得其反--为什么知道的并非越多越好?
(美) 卡斯·R.桑斯坦 著,杨帅华 译
信息物理系统逻辑基础
信息学竞赛宝典 动态规划
张新华 胡向荣 伍婉秋
您可能感兴趣 / 更多
信息物理系统逻辑基础
亚拉山大的读心术(数学大师的逻辑课) 伦理学、逻辑学 [美]雷蒙德·m.斯穆里安(raymondm.smullyan)
[美]雷蒙德·m.斯穆里安(raymondm.smullyan)
信息物理系统逻辑基础
纳博科夫精选集第五辑
[美]弗拉基米尔·纳博科夫著
信息物理系统逻辑基础
九桃盘(美国二十世纪重要女诗人玛丽安·摩尔诗歌精选集,由知名女诗人和女性诗学研究者倪志娟倾情翻译)
[美]玛丽安•摩尔
信息物理系统逻辑基础
全新正版图书 制造德·戴维尼浙江教育出版社9787572276880
[美]理查德·戴维尼
信息物理系统逻辑基础
血泪之泣
[美]希瑟·丘·麦克亚当
信息物理系统逻辑基础
小学生趣味心理学(培养执行技能的40个练习,发展共情能力的46个练习,学会应对焦虑的40个练习 共3册) (美)莎伦·格兰德 王佳妮译
[美]莎伦·格兰德(sharon grand)
信息物理系统逻辑基础
(当代学术棱镜译丛)艺术批评入门:历史、策略与声音
[美]克尔·休斯顿
信息物理系统逻辑基础
数据工程之道:设计和构建健壮的数据系统 [美]乔·里斯 [美]马特·豪斯利
[美]乔·里斯(Joe Reis),[美]马特·豪斯利(Matt Housley)
信息物理系统逻辑基础
矿王谷的黎明:塞拉俱乐部诉莫顿案与美国环境法的转变(精装典藏版)
[美]丹尼尔·P.塞尔米,(Daniel,P.Selmi)
信息物理系统逻辑基础
体式神话:瑜伽传统故事精粹(第二版) (从30个体式古老起源中汲取灵感与力量,内附精美插图)
[美]阿兰娜·凯瓦娅(Alanna Kaivalya)[荷]阿诸那·范德·库伊(Arjuna van der Kooij)
信息物理系统逻辑基础
诺奖作家给孩子的阅读课·生命教育(3-9年级,莫言余华的文学启蒙,垫高阅读起点,提升作文能力)
[美]海明威等
信息物理系统逻辑基础
蚯蚓的日记(全4册)【平装版】
[美]朵琳·克罗宁