內容簡介
《分數階系統高階邏輯形式化驗證》是分數階系統與高階邏輯形式化驗證的基礎理論研究著作。分數階系統是建立在分數階微積分方程理論上實際系統的數學模型。分數階微積分方程是擴展傳統微積分學的一種直接方式,即允許微積分方程中對函式的階次選擇分數,而不僅是現有的整數。分數階微積分不僅為系統科學提供了一個新的數學工具,它的廣泛套用也表明了實際系統動態過程本質上是分數階的。高階邏輯形式化驗證是形式化驗證方法的一種,它是一種人機互動的定理證明方法。《分數階系統高階邏輯形式化驗證》以分數階微積分和高階邏輯形式化驗證為切入點,系統性研究了分數階系統的求解、近似化、控制器設計與高階邏輯形式化分析驗證等內容。
目錄
目錄
第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