[套装书]信息物理系统逻辑基础+信息物理系统强化学习：网络安全示例（2册）

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



---------------------------8078731 - 信息物理系统强化学习：网络安全示例---------------------------


出版者的话
译者序
前言
作者简介
第一部分　介绍
第1章　强化学习概述 2
1.1　强化学习综述 2
1.1.1　引言 2
1.1.2　与其他机器学习方法的比较 4
1.1.3　强化学习示例 6
1.1.4　强化学习应用 7
1.2　强化学习的发展历史 9
1.2.1　传统的强化学习 9
1.2.2　深度强化学习 11
1.3　强化学习的仿真工具 12
1.4　本章小结 13
第2章　信息物理系统和网络安全概述 14
2.1　引言 14
2.2　信息物理系统研究示例 16
2.2.1　资源分配 16
2.2.2　数据传输与管理 18
2.2.3　能源控制 18
2.2.4　基于模型的软件设计 19
2.3　网络安全威胁 20
2.3.1　网络安全的对手 20
2.3.2　网络安全的目标 21
2.4　本章小结 26
2.5　练习 26
第二部分　强化学习在信息物理系统中的应用
第3章　强化学习问题 30
3.1　多臂赌博机问题 30
3.1.1　ε-greedy算法 33
3.1.2　softmax算法 35
3.1.3　UCB算法 36
3.2　上下文赌博机问题 37
3.3　完整的强化学习问题 39
3.3.1　强化学习的要素 40
3.3.2　马尔可夫决策过程介绍 41
3.3.3　值函数 42
3.4　本章小结 45
3.5　练习 45
第4章　基于模型的强化学习 49
4.1　引言 49
4.2　动态规划 51
4.2.1　策略迭代法 52
4.2.2　价值迭代法 55
4.2.3　异步动态规划 56
4.3　部分可观察马尔可夫决策过程 58
4.4　连续马尔可夫决策过程 61
4.4.1　惰性近似 61
4.4.2　函数近似 62
4.5　本章小结 63
4.6　练习 64
第5章　无模型强化学习 66
5.1　引言 66
5.2　强化学习预测 66
5.2.1　蒙特卡罗学习 66
5.2.2　时序差分学习 69
5.3　强化学习控制 71
5.3.1　蒙特卡罗控制 71
5.3.2　基于时序差分的控制 72
5.3.3　策略梯度 77
5.3.4　actor-critic 81
5.4　高级算法 84
5.4.1　期望Sarsa 84
5.4.2　双Q-learning 85
5.5　本章小结 85
5.6　练习 86
第6章　深度强化学习 90
6.1　引言 90
6.2　深度神经网络 90
6.2.1　卷积神经网络 92
6.2.2　循环神经网络 94
6.3　深度学习在值函数上的应用 95
6.4　深度学习在策略函数上的应用 100
6.4.1　DDPG 102
6.4.2　A3C 104
6.5　深度学习在强化学习模型上的应用 107
6.6　深度强化学习计算效率 108
6.7　本章小结 109
6.8　练习 109
第三部分　案例研究
第7章　强化学习与网络安全 112
7.1　传统的网络安全方法 112
7.1.1　传统的网络安全技术 112
7.1.2　新兴网络安全威胁 113
7.2　强化学习在网络安全中的应用 114
7.2.1　移动群智感知中的虚假感知攻击 114
7.2.2　认知无线电网络中的安全强化 115
7.2.3　移动边缘计算中的安全问题 117
7.2.4　网络安全分析师的动态调度 118
7.3　本章小结 119
7.4　练习 119
第8章　案例研究：智能电网中的在线网络攻击检测 120
8.1　引言 120
8.2　系统模型和状态估计 122
8.2.1　系统模型 122
8.2.2　状态估计 123
8.3　问题描述 124
8.4　解决方案 127
8.5　仿真结果 130
8.5.1　仿真设计与参数设置 130
8.5.2　性能评估 130
8.6　本章小结 134
第9章　案例研究：击败中间人攻击 135
9.1　引言 135
9.2　强化学习方法 137
9.2.1　状态空间 137
9.2.2　行动空间 139
9.2.3　奖励 139
9.3　实验和结果 139
9.3.1　模型训练 140
9.3.2　在线实验 141
9.4　讨论 143
9.4.1　基于探测器的检测系统 143
9.4.2　运用SDN/OpenFlow使模型实用 144
9.5　本章小结 144
参考文献 145
索引 161

.　　
　　本书的灵感来自强化学习（RL）与信息物理系统（CPS）领域近期的发展。强化学习植根于行为心理学，是机器学习的主要分支。与监督学习和无监督学习这样的机器学习算法不同，强化学习的主要特征是其独一无二的学习范式——试错法。通过与深度神经网络结合，深度强化学习变得非常强大，使得AI智能体能够以超人类的水平自动管理许多复杂的系统。此外，人们期望信息物理系统能够在不久的将来给我们的社会带来颠覆性改变，例如新兴智能建筑、智能交通和电网。
　　然而，信息物理系统领域的传统人工编程控制器，既不能处理日益复杂的系统，也不能自动适应它以前从未遇到过的新情况。如何应用现有的深度强化学习算法或开发新的强化学习算法以实现实时适应性信息物理系统？此问题仍然悬而未决。本书通过系统介绍强化学习领域的基础与算法，在两个领域之间建立起联系，并在每一部分列举了一个或几个最新的信息物理系统示例，以帮助读者直观地理解强化学习技术的实用性。
　　本书特色
　　介绍强化学习，包括强化学习领域的高级主题。
　　将强化学习应用到信息物理系统和网络安全。
　　每章都包含最新的示例和练习。
　　用两个案例研究介绍网络安全问题。
　　本书适用于科学、工程、计算机科学或应用数学领域的研究生或大三/大四本科生，以及对于网络安全、强化学习和信息物理系统等领域感兴趣的研究人员和工程师。阅读本书的读者需要微积分和概率论的基础知识。