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

定　價：￥179.00

作　者：	[美] 安德烈·普拉澤（André Platzer）著，曾海波李仁發(fā)譯譯
出版社：	機械工業(yè)出版社
叢編項：
標(biāo)　簽：	暫缺

購買這本書可以去

ISBN：	9787111685623	出版時間：	2021-08-01	包裝：	平裝
開本：	16開	頁數(shù)：	452	字?jǐn)?shù)：

內(nèi)容簡介

　　本書全面介紹如何采用邏輯與演繹語言推理信息物理系統(tǒng)。在這個過程中，讀者將學(xué)習(xí)計算機科學(xué)、應(yīng)用數(shù)學(xué)和控制論的許多基本概念，所有這些對了解CPS都是必不可少的。本書分為以下四個部分。在第1部分中，讀者將學(xué)習(xí)如何對包含連續(xù)變量和編程構(gòu)造的CPS建模，如何描述需求規(guī)約，以及如何用證明規(guī)則檢驗?zāi)Ｐ褪欠駶M足需求。第二部分增加了對物理世界建模采用的微分方程。第三部分介紹了對手的概念，在控制系統(tǒng)中，對手可以通過噪聲和其他干擾影響系統(tǒng)的周邊環(huán)境。在存在對手的時候做決策意味著需要對較壞情況做好準(zhǔn)備。第四部分進一步增加了如何在實際應(yīng)用中對系統(tǒng)做嚴(yán)格而高效的推理，比如采用實算術(shù)和監(jiān)控器條件。

作者簡介

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

圖書目錄

贊譽
譯者序
推薦序
致謝
第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)的計算思維7
　16　學(xué)習(xí)目標(biāo)8
　17　本書的結(jié)構(gòu)9
　18　總結(jié)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　總結(jié)35
　29　附錄35
　　291　存在性定理35
　　292　唯一性定理36
　　293　常系數(shù)線性微分方程37
　　294　延拓與連續(xù)依賴38
　習(xí)題39
　參考文獻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è)計54
　　341　制動還是不制動，這是個問題54
　　342　選擇的問題55
　35　總結(jié)56
　36　附錄：機器人彎道運動建模56
　習(xí)題58
　參考文獻61
第4章　安全性與契約63
　41　引言63
　42　CPS契約的逐步介紹64
　　421　彈跳球Quantum歷險記64
　　422　Quantum如何在時間結(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
　參考文獻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)中的蘊涵108
　　562　如果沒有任何相關(guān)變化，則為空虛狀態(tài)變化109
　　563　哥德爾將永真性泛化到方括號模態(tài)中109
　　564　后置條件的單調(diào)性110
　　565　自由變量和約束變量111
　　566　自由變量和約束變量分析111
　習(xí)題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　實算術(shù)證明規(guī)則133
　　651　實數(shù)量詞消除法134
　　652　實例化實算術(shù)量詞136
　　653　通過去除假設(shè)來弱化實算術(shù)137
　　654　相繼式演算中的結(jié)構(gòu)證明規(guī)則138
　　655　在公式中代入等式139
　　656　縮寫項以降低復(fù)雜性139
　　657　創(chuàng)造性地切割實算術(shù)轉(zhuǎn)化問題140
　66　總結(jié)140
　習(xí)題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　一個歡快重復(fù)的彈跳球的證明154
　75　將后置條件拆分為單獨的情況158
　76　總結(jié)159
　77　附錄159
　　771　證明的循環(huán)159
　　772　打破證明循環(huán)161
　　773　循環(huán)的不變式證明163
　　774　歸納公理的替代形式163
　習(xí)題165
　參考文獻166