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

贊譽(yù)
譯者序
推薦序
致謝
第1章　信息物理系統(tǒng)概述1
　11　引言1
　　111　舉例分析信息物理系統(tǒng)1
　　112　應(yīng)用領(lǐng)域2
　　113　意義2
　　114　安全的重要性3
　12　混成系統(tǒng)與信息物理系統(tǒng)4
　13　多動態(tài)系統(tǒng)5
　14　如何學(xué)習(xí)信息物理系統(tǒng)6
　15　信息物理系統(tǒng)的計(jì)算思維7
　16　學(xué)習(xí)目標(biāo)8
　17　本書的結(jié)構(gòu)9
　18　總結(jié)12
　參考文獻(xiàn)12
第一部分　初等信息物理系統(tǒng)
第2章　微分方程與域18
　21　引言18
　22　作為連續(xù)物理過程模型的微分方程18
　23　微分方程的含義20
　24　微分方程示例的簡短綱要21
　25　微分方程的域26
　26　連續(xù)程序的語法27
　　261　連續(xù)程序28
　　262　項(xiàng)28
　　263　一階公式29
　27　連續(xù)程序的語義30
　　271　項(xiàng)30
　　272　一階公式31
　　273　連續(xù)程序34
　28　總結(jié)35
　29　附錄35
　　291　存在性定理35
　　292　唯一性定理36
　　293　常系數(shù)線性微分方程37
　　294　延拓與連續(xù)依賴38
　習(xí)題39
　參考文獻(xiàn)41
第3章　選擇與控制42
　31　引言42
　32　混成程序的逐步介紹43
　　321　混成程序的離散變化43
　　322　混成程序的合成44
　　323　混成程序中的決策45
　　324　混成程序中的選擇45
　　325　混成程序中的測試47
　　326　混成程序中的重復(fù)48
　33　混成程序50
　　331　混成程序的語法50
　　332　混成程序的語義51
　34　混成程序設(shè)計(jì)54
　　341　制動還是不制動，這是個(gè)問題54
　　342　選擇的問題55
　35　總結(jié)56
　36　附錄：機(jī)器人彎道運(yùn)動建模56
　習(xí)題58
　參考文獻(xiàn)61
第4章　安全性與契約63
　41　引言63
　42　CPS契約的逐步介紹64
　　421　彈跳球Quantum歷險(xiǎn)記64
　　422　Quantum如何在時(shí)間結(jié)構(gòu)中發(fā)現(xiàn)裂縫67
　　423　Quantum怎樣學(xué)會放氣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　總結(jié)82
　48　附錄82
　　481　順序合成證明的中間條件82
　　482　選擇的證明84
　　483　測試的證明85
　習(xí)題86
　參考文獻(xiàn)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　總結(jié)107
　56　附錄108
　　561　模態(tài)肯定前件在方括號模態(tài)中的蘊(yùn)涵108
　　562　如果沒有任何相關(guān)變化，則為空虛狀態(tài)變化109
　　563　哥德爾將永真性泛化到方括號模態(tài)中109
　　564　后置條件的單調(diào)性110
　　565　自由變量和約束變量111
　　566　自由變量和約束變量分析111
　習(xí)題113
　參考文獻(xiàn)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　實(shí)算術(shù)證明規(guī)則133
　　651　實(shí)數(shù)量詞消除法134
　　652　實(shí)例化實(shí)算術(shù)量詞136
　　653　通過去除假設(shè)來弱化實(shí)算術(shù)137
　　654　相繼式演算中的結(jié)構(gòu)證明規(guī)則138
　　655　在公式中代入等式139
　　656　縮寫項(xiàng)以降低復(fù)雜性139
　　657　創(chuàng)造性地切割實(shí)算術(shù)轉(zhuǎn)化問題140
　66　總結(jié)140
　習(xí)題141
　參考文獻(xiàn)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　一個(gè)歡快重復(fù)的彈跳球的證明154
　75　將后置條件拆分為單獨(dú)的情況158
　76　總結(jié)159
　77　附錄159
　　771　證明的循環(huán)159
　　772　打破證明循環(huán)161
　　773　循環(huán)的不變式證明163
　　774　歸納公理的替代形式163
　習(xí)題165
　參考文獻(xiàn)166