信息物理系統(tǒng)邏輯基礎

贊譽
譯者序
推薦序
致謝
第1章　信息物理系統(tǒng)概述1
　11　引言1
　　111　舉例分析信息物理系統(tǒng)1
　　112　應用領域2
　　113　意義2
　　114　安全的重要性3
　12　混成系統(tǒng)與信息物理系統(tǒng)4
　13　多動態(tài)系統(tǒng)5
　14　如何學習信息物理系統(tǒng)6
　15　信息物理系統(tǒng)的計算思維7
　16　學習目標8
　17　本書的結構9
　18　總結12
　參考文獻12
第一部分　初等信息物理系統(tǒng)
第2章　微分方程與域18
　21　引言18
　22　作為連續(xù)物理過程模型的微分方程18
　23　微分方程的含義20
　24　微分方程示例的簡短綱要21
　25　微分方程的域26
　26　連續(xù)程序的語法27
　　261　連續(xù)程序28
　　262　項28
　　263　一階公式29
　27　連續(xù)程序的語義30
　　271　項30
　　272　一階公式31
　　273　連續(xù)程序34
　28　總結35
　29　附錄35
　　291　存在性定理35
　　292　唯一性定理36
　　293　常系數(shù)線性微分方程37
　　294　延拓與連續(xù)依賴38
　習題39
　參考文獻41
第3章　選擇與控制42
　31　引言42
　32　混成程序的逐步介紹43
　　321　混成程序的離散變化43
　　322　混成程序的合成44
　　323　混成程序中的決策45
　　324　混成程序中的選擇45
　　325　混成程序中的測試47
　　326　混成程序中的重復48
　33　混成程序50
　　331　混成程序的語法50
　　332　混成程序的語義51
　34　混成程序設計54
　　341　制動還是不制動，這是個問題54
　　342　選擇的問題55
　35　總結56
　36　附錄：機器人彎道運動建模56
　習題58
　參考文獻61
第4章　安全性與契約63
　41　引言63
　42　CPS契約的逐步介紹64
　　421　彈跳球Quantum歷險記64
　　422　Quantum如何在時間結構中發(fā)現(xiàn)裂縫67
　　423　Quantum怎樣學會放氣68
　　424　CPS的后置條件契約69
　　425　CPS的前置條件契約70
　43　混成程序的邏輯公式71
　44　微分動態(tài)邏輯73
　　441　微分動態(tài)邏輯的語法73
　　442　微分動態(tài)邏輯的語義75
　45　邏輯形式的CPS契約77
　46　查明CPS的需求78
　47　總結82
　48　附錄82
　　481　順序合成證明的中間條件82
　　482　選擇的證明84
　　483　測試的證明85
　習題86
　參考文獻90
第5章　動態(tài)系統(tǒng)與動態(tài)公理92
　51　引言92
　52　CPS的中間條件93
　53　動態(tài)系統(tǒng)的動態(tài)公理95
　　531　非確定性選擇的動態(tài)公理95
　　532　公理的可靠性97
　　533　賦值的動態(tài)公理98
　　534　微分方程的動態(tài)公理99
　　535　測試的動態(tài)公理101
　　536　順序合成的動態(tài)公理102
　　537　循環(huán)的動態(tài)公理104
　　538　尖括號模態(tài)的公理105
　54　短暫彈跳球的證明105
　55　總結107
　56　附錄108
　　561　模態(tài)肯定前件在方括號模態(tài)中的蘊涵108
　　562　如果沒有任何相關變化，則為空虛狀態(tài)變化109
　　563　哥德爾將永真性泛化到方括號模態(tài)中109
　　564　后置條件的單調(diào)性110
　　565　自由變量和約束變量111
　　566　自由變量和約束變量分析111
　習題113
　參考文獻116
第6章　真理與證明118
　61　引言118
　62　真理和證明119
　　621　相繼式120
　　622　證明122
　　623　命題證明規(guī)則122
　　624　證明規(guī)則的可靠性126
　　625　動態(tài)的證明127
　　626　量詞證明規(guī)則129
　63　派生證明規(guī)則131
　64　單跳彈跳球的相繼式證明132
　65　實算術證明規(guī)則133
　　651　實數(shù)量詞消除法134
　　652　實例化實算術量詞136
　　653　通過去除假設來弱化實算術137
　　654　相繼式演算中的結構證明規(guī)則138
　　655　在公式中代入等式139
　　656　縮寫項以降低復雜性139
　　657　創(chuàng)造性地切割實算術轉(zhuǎn)化問題140
　66　總結140
　習題141
　參考文獻143
第7章　控制回路與不變式145
　71　引言145
　72　控制循環(huán)146
　73　循環(huán)回路147
　　731　循環(huán)的歸納公理147
　　732　循環(huán)的歸納規(guī)則149
　　733　循環(huán)不變式150
　　734　上下文可靠性需求153
　74　一個歡快重復的彈跳球的證明154
　75　將后置條件拆分為單獨的情況158
　76　總結159
　77　附錄159
　　771　證明的循環(huán)159
　　772　打破證明循環(huán)161
　　773　循環(huán)的不變式證明163
　　774　歸納公理的替代形式163
　習題165
　參考文獻166