本书是分数阶系统与高阶逻辑形式化验证的基础理论研究著作。分数阶系统是建立在分数阶微积分方程理论上实际系统的数学模型。分数阶微积分方程是扩展传统微积分学的一种直接方式，即允许微积分方程中对函数的阶次选择分数，而不仅是现有的整数。分数阶微积分不仅为系统科学提供了一个新的数学工具，它的广泛应用也表明了实际系统动态过程本质上是分数阶的。高阶逻辑形式化验证是形式化验证方法的一种，它是一种人机交互的定理证明方法。本书以分数阶微积分和高阶逻辑形式化验证为切入点，系统性研究了分数阶系统的求解、近似化、控制器设计与高阶逻辑形式化分析验证等内容。
样章试读
目录
- 目录
第1章 分数阶系统概述 1
1.1 分数阶系统简介 2
1.2 分数阶系统求解 3
1.3 分数阶系统近似化 5
1.4 成比例分数阶系统 5
1.5 分数阶PID控制器 6
参考文献 7
第2章 相关理论基础 9
2.1 基本函数 9
2.2 分数阶微积分定义 12
2.2.1 Grunwald-Letnikov分数阶微积分定义 12
2.2.2 Riemann-Liouville分数阶微积分定义 13
2.2.3 Caputo分数阶微积分定义 13
2.2.4 分数阶微积分定义间的关系 14
2.2.5 分数阶微积分的性质 14
2.3 分数阶微积分的基本变换 15
2.3.1 Laplace变换 15
2.3.2 Fourier变换 16
2.4 分数阶微积分方程的解 16
2.4.1 分数阶微积分方程 16
2.4.2 解的存在与唯一性 17
第3章 分数阶系统求解 18
3.1 分数阶线性微积分方程求解 18
3.1.1 求解算法 18
3.1.2 步长的影响 21
3.2 分数阶微积分框图求解法 22
3.2.1 分数阶微积分模块 22
3.2.2 框图法求解分数阶线性微积分方程 23
3.2.3 框图法求解分数阶非线性微积分方程 24
参考文献 28
第4章 分数阶微积分算子近似 29
4.1 直接近似化方法 29
4.2 间接近似化方法 31
4.3 改进近似法 34
4.3.1 系数的选取 36
4.3.2 Taylor级数的剪切 39
4.4 分数阶系统最优降阶 41
4.5 仿真实例 41
参考文献 46
第5章 成比例分数阶系统 47
5.1 成比例分数阶系统表示方法 47
5.2 状态空间与传递函数的关系 49
5.3 成比例分数阶系统的稳定性 50
5.4 成比例分数阶系统的能控性与能观性 52
5.4.1 能控性 52
5.4.2 能观性 54
5.5 成比例分数阶系统的响应分析 54
5.6 理想传递函数 56
5.7 成比例分数阶系统实例分析 57
5.8 成比例分数阶系统的H2范数 59
5.9 控制器设计与仿真 60
参考文献 64
第6章 分数阶PID控制器设计 65
6.1 分数阶PID 控制器 65
6.2 简单分数阶系统的分数阶PID 控制器设计与仿真 66
6.2.1 控制器设计 66
6.2.2 仿真实例 68
6.3 分数阶系统的分数阶PID 控制器设计与仿真 74
6.3.1 控制器设计 74
6.3.2 仿真实例 75
参考文献 77
第7章 分数阶PID控制器对比研究 78
7.1 位置伺服系统 78
7.2 分数阶PID控制器与模型预测控制的比较 79
7.3 分数阶PID控制器与整数阶PID控制器的对比研究 81
7.3.1 控制器设计 81
7.3.2 分数阶PID控制器对于负载变化的鲁棒性 85
7.3.3 近似中N的选取 89
7.4 分数阶PI 控制器与整数阶PI 控制器的对比研究 93
7.4.1 控制器设计 94
7.4.2 分数阶PI控制器对于负载变化的鲁棒性 96
7.5 分数阶控制器对于弹性参数的鲁棒性 101
7.5.1 分数阶PID控制器的鲁棒性 101
7.5.2 分数阶PI控制器的鲁棒性 104
7.6 分数阶控制器对于机械非线性的鲁棒性 107
参考文献 110
第8章 智能PID温度控制算法研究 111
8.1 PID 参数模糊自整定温度测控仪 111
8.1.1 模糊PID 控制器的设计 111
8.1.2 硬件部分 114
8.1.3 软件部分 115
8.2 基于遗传算法的连续重整装置智能PID 温度控制系统 116
8.2.1 系统组成 117
8.2.2 遗传算法的基本操作 117
8.2.3 基于遗传算法的PID参数寻优的过程 118
8.2.4 连续重整装置反应器温度控制系统PID参数的寻优设计 119
8.2.5 控制效果分析 121
8.3 连续重整装置模糊自适应PID 温度控制系统 122
8.3.1 PID型模糊控制器结构 122
8.3.2 参数自适应方法 124
8.3.3 隶属度函数的调整和可调因子的自整定 125
8.3.4 控制效果分析 128
参考文献 128
第9章 风暴灾害中的分数阶模型 129
9.1 人员伤亡损失评估 129
9.2 直接经济损失评估 131
9.3 间接经济损失评估 133
9.4 举例分析 134
参考文献 135
第10章 教育评估的分数阶模型 136
10.1 教育评估简介 136
10.2 分数阶评估方法 137
10.2.1 课程评估指标体系 137
10.2.2 确定指标权重 138
10.2.3 基于关联距离度的评估模型 140
10.3 实例分析 144
参考文献 148
第11章 分数阶序列最小优化方法 149
11.1 支持向量机 149
11.1.1 线性可分支持向量机 150
11.1.2 线性不可分支持向量机 154
11.1.3 非线性支持向量机与核函数 155
11.2 序列最小优化算法 156
11.3 序列最小优化算法的分数阶拓展 159
11.4 实例验证 163
第12章 LIBSVM工具箱中分数阶C-支持向量分类方法 172
12.1 泰勒展开式推导 173
12.1.1 一元泰勒展开式 173
12.1.2 多元泰勒展开式 173
12.1.3 分数阶泰勒展开式 174
12.2 目标函数的分数阶改进 176
12.3 拉格朗日乘子的更新 177
12.3.1 选取拉格朗日乘子α的下标i 177
12.3.2 选取拉格朗日乘子α的下标j 179
12.3.3 对拉格朗日乘子的更新 184
12.4 分数阶导数集合的更新 186
12.5 法向量w和偏移量b的计算 187
12.6 确定分类结果 188
12.7 实例验证 188
第13章 高阶逻辑定理证明器 197
13.1 形式化验证 197
13.1.1 等价性验证 199
13.1.2 模型检验 199
13.1.3 定理证明 200
13.2 HOL系统概述 202
13.2.1 HOL系统的发展 202
13.2.2 ML语言 204
13.2.3 HOL类型 204
13.2.4 定理库 205
13.2.5 对策和策略 207
13.2.6 证明方法 208
13.2.7 HOL 的基本逻辑符号 208
第14章 分数阶微积分的高阶逻辑形式化 210
14.1 实数二项式系数的形式化 210
14.1.1 阶乘幂的形式化 210
14.1.2 实数二项式系数的形式化 212
14.2 基本函数的高阶逻辑形式化 214
14.2.1 Gamma函数 214
14.2.2 Beta函数 216
14.2.3 Mittag-Leffler函数 216
14.3 分数阶微积分的形式化 218
14.3.1 分数阶微积分定义的形式化建模 218
14.3.2 零阶性的形式化 219
14.3.3 齐次性质 221
14.3.4 线性性质的形式化 222
14.3.5 常函数的分数阶微积分 225
14.3.6 分数阶微积分与整数阶微积分的关系 226
14.3.7 叠加性的形式化 229
14.3.8 分数阶微积分Caputo与GL、RL定义关系的形式化验证 232
14.3.9 傅里叶变换 234
参考文献 235
第15章 函数极限的高阶逻辑形式化建模与验证 236
15.1 函数无穷远处极限定义的建模与验证 236
15.2 函数极限相关性质的建模与验证 238
15.2.1 函数极限基本性质的建模与验证 238
15.2.2 函数极限四则运算的建模与验证 240
15.3 函数积分极限的高阶逻辑形式化建模与验证 244
15.3.1 正无穷函数积分上限取绝对值的建模与验证 244
15.3.2 正无穷函数积分上限与常数之和的建模与验证 245
15.3.3 正无穷函数积分上限与非负常数之积的建模与验证 247
第16章 拉普拉斯变换的高阶逻辑形式化建模验证 249
16.1 拉普拉斯变换定义形式化的建模与验证 250
16.2 基本性质的建模与验证 252
16.2.1 线性性质的建模与验证 252
16.2.2 微积分性质的建模与验证 253
16.2.3 积分性质的建模与验证 253
16.2.4 频移性质的建模与验证 254
16.2.5 延迟性质的建模与验证 255
16.2.6 尺度变换性的建模与验证 256
16.2.7 卷积定理的建模与验证 257
16.3 分数阶拉普拉斯变换模型 259
第17章 分数阶系统的形式化分析 262
17.1 FC 元件的形式化分析 262
17.2 分抗元件的形式化 263
17.3 分数阶微积分电路的形式化 264
17.4 直流电机传递函数的高阶逻辑形式化建模与验证 266
17.5 RL 电路电流的高阶逻辑形式化建模与验证 269
17.6 药物动力学验证 272
17.7 分数阶控制系统的形式化 274
17.7.1 分数阶PID控制器的形式化 274
17.7.2 分数阶闭环系统的形式化 282
17.7.3 位置伺服系统的形式化 284
参考文献 286
京公网安备 11010102004214号