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

定　價(jià)：￥179.00

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

購(gòu)買(mǎi)這本書(shū)可以去

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

內(nèi)容簡(jiǎn)介

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

作者簡(jiǎn)介

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

圖書(shū)目錄

贊譽(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　多動(dòng)態(tài)系統(tǒng)5
　14　如何學(xué)習(xí)信息物理系統(tǒng)6
　15　信息物理系統(tǒng)的計(jì)算思維7
　16　學(xué)習(xí)目標(biāo)8
　17　本書(shū)的結(jié)構(gòu)9
　18　總結(jié)12
　參考文獻(xiàn)12
第一部分　初等信息物理系統(tǒng)
第2章　微分方程與域18
　21　引言18
　22　作為連續(xù)物理過(guò)程模型的微分方程18
　23　微分方程的含義20
　24　微分方程示例的簡(jiǎn)短綱要21
　25　微分方程的域26
　26　連續(xù)程序的語(yǔ)法27
　　261　連續(xù)程序28
　　262　項(xiàng)28
　　263　一階公式29
　27　連續(xù)程序的語(yǔ)義30
　　271　項(xiàng)30
　　272　一階公式31
　　273　連續(xù)程序34
　28　總結(jié)35
　29　附錄35
　　291　存在性定理35
　　292　唯一性定理36
　　293　常系數(shù)線(xiàn)性微分方程37
　　294　延拓與連續(xù)依賴(lài)38
　習(xí)題39
　參考文獻(xiàn)41
第3章　選擇與控制42
　31　引言42
　32　混成程序的逐步介紹43
　　321　混成程序的離散變化43
　　322　混成程序的合成44
　　323　混成程序中的決策45
　　324　混成程序中的選擇45
　　325　混成程序中的測(cè)試47
　　326　混成程序中的重復(fù)48
　33　混成程序50
　　331　混成程序的語(yǔ)法50
　　332　混成程序的語(yǔ)義51
　34　混成程序設(shè)計(jì)54
　　341　制動(dòng)還是不制動(dòng)，這是個(gè)問(wèn)題54
　　342　選擇的問(wèn)題55
　35　總結(jié)56
　36　附錄：機(jī)器人彎道運(yùn)動(dòng)建模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é)會(huì)放氣68
　　424　CPS的后置條件契約69
　　425　CPS的前置條件契約70
　43　混成程序的邏輯公式71
　44　微分動(dòng)態(tài)邏輯73
　　441　微分動(dòng)態(tài)邏輯的語(yǔ)法73
　　442　微分動(dòng)態(tài)邏輯的語(yǔ)義75
　45　邏輯形式的CPS契約77
　46　查明CPS的需求78
　47　總結(jié)82
　48　附錄82
　　481　順序合成證明的中間條件82
　　482　選擇的證明84
　　483　測(cè)試的證明85
　習(xí)題86
　參考文獻(xiàn)90
第5章　動(dòng)態(tài)系統(tǒng)與動(dòng)態(tài)公理92
　51　引言92
　52　CPS的中間條件93
　53　動(dòng)態(tài)系統(tǒng)的動(dòng)態(tài)公理95
　　531　非確定性選擇的動(dòng)態(tài)公理95
　　532　公理的可靠性97
　　533　賦值的動(dòng)態(tài)公理98
　　534　微分方程的動(dòng)態(tài)公理99
　　535　測(cè)試的動(dòng)態(tài)公理101
　　536　順序合成的動(dòng)態(tài)公理102
　　537　循環(huán)的動(dòng)態(tài)公理104
　　538　尖括號(hào)模態(tài)的公理105
　54　短暫彈跳球的證明105
　55　總結(jié)107
　56　附錄108
　　561　模態(tài)肯定前件在方括號(hào)模態(tài)中的蘊(yùn)涵108
　　562　如果沒(méi)有任何相關(guān)變化，則為空虛狀態(tài)變化109
　　563　哥德?tīng)枌⒂勒嫘苑夯椒嚼ㄌ?hào)模態(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　動(dòng)態(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　通過(guò)去除假設(shè)來(lái)弱化實(shí)算術(shù)137
　　654　相繼式演算中的結(jié)構(gòu)證明規(guī)則138
　　655　在公式中代入等式139
　　656　縮寫(xiě)項(xiàng)以降低復(fù)雜性139
　　657　創(chuàng)造性地切割實(shí)算術(shù)轉(zhuǎn)化問(wè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