《信息物理系统逻辑基础/计算机科学丛书》（(美)安德烈·普拉泽|责编:姚蕾//唐晓琳|译者:曾海波//李仁发）-图书推荐
内容提要
本书全面介绍如何采用逻辑与演绎语言推理信息物理系统。在这个过程中，读者将学习计算机科学、应用数学和控制论的许多基本概念，所有这些对了解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.2CPS契约的逐步介绍64
4.2.1弹跳球Quantum历险记64
4.2.2Quantum如何在时间结构中发现裂缝67
4.2.3Quantum怎样学会放气68
4.2.4CPS的后置条件契约69
4.2.5CPS的前置条件契约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.2CPS的中间条件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
第二部分微分方程分析
**0章微分方程与微分不变式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总结21
10.8附录214
10.8.1微分方程与循环214
10.8.2微分不变项和不变函数216
习题217
参考文献218
**1章微分方程与证明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
**2章幽灵与微分幽灵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
**3章微分不变式与证明论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
第三部分对抗式信息物理系统
**4章混成系统与博弈286
14.1引言286
14.2混成博弈的逐步介绍288
14.2.1选择与非确定性288
14.2.2控制与对偶控制289
14.2.3Demon的派生控制290
14.3微分博弈逻辑的语法291
14.3.1混成博弈291
14.3.2微分博弈逻辑公式294
14.3.3示例294
14.4非形式化操作博弈树语义298
14.5总结301
习题302
参考文献304
**5章必胜策略与区域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
**6章获胜与证明混成博弈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
**7章博弈证明与分离性347
17.1引言347
17.2简要回顾：混成博弈348
17.3分离公理348
17.4重复的尖括号模态——收敛对比迭代352
17.5总结354
17.6附录：关联微分博弈逻辑与微分动态逻辑354
习题355
参考文献356
第四部分综合CPS正确性
**8章公理与一致替换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.6dL的公理体系证明演算374
18.7微分公理375
18.8总结376
18.9附录：规则和证明的一致替换376
习题377
参考文献379
**9章已验证模型与已验证运行时确认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
卖贝商城 推荐：《信息物理系统逻辑基础/计算机科学丛书》（(美)安德烈·普拉泽|责编:姚蕾//唐晓琳|译者:曾海波//李仁发）