信息物理系統邏輯基礎 Logical Foundations of Cyber-Physical Systems

安德烈·普拉澤（André Platzer）
卡內基·梅隆大學計算機科學系教授。
他擁有德國奧爾登堡大學的博士學位。
研究領域包括形式化方法、編程語言和純邏輯與應用邏輯。
他曾於2009年獲得ACM最佳博士論文榮譽提名獎，2011年獲得NSF傑出青年獎，併入選美國Popular Science雜誌2009年“十大傑出青年科學家”、IEEE Intelligent Systems雜誌2010年“AI十大潛力人物”。

讚譽
譯者序
推薦序
致謝
第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

第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