掃一掃
關注中圖網
官方微博
本類五星書更多>
-
>
全國計算機等級考試最新真考題庫模擬考場及詳解·二級MSOffice高級應用
-
>
決戰行測5000題(言語理解與表達)
-
>
軟件性能測試.分析與調優實踐之路
-
>
第一行代碼Android
-
>
JAVA持續交付
-
>
EXCEL最強教科書(完全版)(全彩印刷)
-
>
深度學習
信息物理系統邏輯基礎 版權信息
- ISBN：9787111685623
- 條形碼：9787111685623 ; 978-7-111-68562-3
- 裝幀：一般膠版紙
- 冊數：暫無
- 重量：暫無
- 所屬分類：>
信息物理系統邏輯基礎 本書特色
適讀人群 ：本書可作為高等院校信息物理系統相關課程的本科生或者研究生教材，也可供對信息物理系統感興趣的讀者閱讀。本書基于作者在卡內基·梅隆大學計算機科學系講授的 “信息物理系統基礎”課程的講義撰寫而成。在許多章節的正文和附錄中提供了必需的背景材料，因此讀者可以在沒有太多預備知識的情況下閱讀。本書分為四個部分。**部分是對初等信息物理系統的概述，講解了如何對包含連續變量和編程構造的CPS建模，如何描述需求規約，以及如何用證明規則檢驗模型是否滿足需求。第二部分增加了用于建模物理世界的微分方程，介紹微分不變式、微分方程的證明以及微分幽靈等內容。第三部分圍繞對抗性信息物理系統進行詳細的解說，用示例闡述混成程序、混成系統、混成博弈、必勝策略等相關概念和公理。第四部分進一步增加了在實際應用中綜合CPS正確性的內容，以對系統做嚴格而高效的推理，涉及的內容有一致替換、虛擬替換、量詞消除和監控器等。
信息物理系統邏輯基礎 內容簡介
本書全面介紹如何采用邏輯與演繹語言推理信息物理系統。在這個過程中，讀者將學習計算機科學、應用數學和控制論的許多基本概念，所有這些對了解CPS都是必不可少的。本書分為以下四個部分。在第1部分中，讀者將學習如何對包含連續變量和編程構造的CPS建模，如何描述需求規約，以及如何用證明規則檢驗模型是否滿足需求。第二部分增加了對物理世界建模采用的微分方程。第三部分介紹了對手的概念，在控制系統中，對手可以通過噪聲和其他干擾影響系統的周邊環境。在存在對手的時候做決策意味著需要對較壞情況做好準備。第四部分進一步增加了如何在實際應用中對系統做嚴格而高效的推理，比如采用實算術和監控器條件。
信息物理系統邏輯基礎 目錄
贊譽
譯者序
推薦序
致謝
第1章 信息物理系統概述1
11 引言1
111 舉例分析信息物理系統1
112 應用領域2
113 意義2
114 安全的重要性3
12 混成系統與信息物理系統4
13 多動態系統5
14 如何學習信息物理系統6
15 信息物理系統的計算思維7
16 學習目標8
17 本書的結構9
18 總結12
參考文獻12
**部分 初等信息物理系統
第2章 微分方程與域18
21 引言18
22 作為連續物理過程模型的微分方程18
23 微分方程的含義20
24 微分方程示例的簡短綱要21
25 微分方程的域26
26 連續程序的語法27
261 連續程序28
262 項28
263 一階公式29
27 連續程序的語義30
271 項30
272 一階公式31
273 連續程序34
28 總結35
29 附錄35
291 存在性定理35
292 唯一性定理36
293 常系數線性微分方程37
294 延拓與連續依賴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如何在時間結構中發現裂縫67
423 Quantum怎樣學會放氣68
424 CPS的后置條件契約69
425 CPS的前置條件契約70
43 混成程序的邏輯公式71
44 微分動態邏輯73
441 微分動態邏輯的語法73
442 微分動態邏輯的語義75
45 邏輯形式的CPS契約77
46 查明CPS的需求78
47 總結82
48 附錄82
481 順序合成證明的中間條件82
482 選擇的證明84
483 測試的證明85
習題86
參考文獻90
第5章 動態系統與動態公理92
51 引言92
52 CPS的中間條件93
53 動態系統的動態公理95
531 非確定性選擇的動態公理95
532 公理的可靠性97
533 賦值的動態公理98
534 微分方程的動態公理99
535 測試的動態公理101
536 順序合成的動態公理102
537 循環的動態公理104
538 尖括號模態的公理105
54 短暫彈跳球的證明105
55 總結107
56 附錄108
561 模態肯定前件在方括號模態中的蘊涵108
562 如果沒有任何相關變化，則為空虛狀態變化109
563 哥德爾將永真性泛化到方括號模態中109
564 后置條件的單調性110
565 自由變量和約束變量111
566 自由變量和約束變量分析111
習題113
參考文獻116
第6章 真理與證明118
61 引言118
62 真理和證明119
621 相繼式120
622 證明122
623 命題證明規則122
624 證明規則的可靠性126
625 動態的證明127
626 量詞證明規則129
63 派生證明規則131
64 單跳彈跳球的相繼式證明132
65 實算術證明規則133
651 實數量詞消除法134
652 實例化實算術量詞136
653 通過去除假設來弱化實算術137
654 相繼式演算中的結構證明規則138
655 在公式中代入等式139
656 縮寫項以降低復雜性139
657 創造性地切割實算術轉化問題140
66 總結140
習題141
參考文獻143
第7章 控制回路與不變式145
71 引言145
72 控制循環146
73 循環回路147
731 循環的歸納公理147
732 循環的歸納規則149
733 循環不變式150
734 上下文可靠性需求153
74 一個歡快重復的彈跳球的證明154
75 將后置條件拆分為單獨的情況158
76 總結159
77 附錄159
771 證明的循環159
772 打破證明循環161
773 循環的不變式證明163
774 歸納公理的替代形式163
習題165
參考文獻166
譯者序
推薦序
致謝
第1章 信息物理系統概述1
11 引言1
111 舉例分析信息物理系統1
112 應用領域2
113 意義2
114 安全的重要性3
12 混成系統與信息物理系統4
13 多動態系統5
14 如何學習信息物理系統6
15 信息物理系統的計算思維7
16 學習目標8
17 本書的結構9
18 總結12
參考文獻12
**部分 初等信息物理系統
第2章 微分方程與域18
21 引言18
22 作為連續物理過程模型的微分方程18
23 微分方程的含義20
24 微分方程示例的簡短綱要21
25 微分方程的域26
26 連續程序的語法27
261 連續程序28
262 項28
263 一階公式29
27 連續程序的語義30
271 項30
272 一階公式31
273 連續程序34
28 總結35
29 附錄35
291 存在性定理35
292 唯一性定理36
293 常系數線性微分方程37
294 延拓與連續依賴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如何在時間結構中發現裂縫67
423 Quantum怎樣學會放氣68
424 CPS的后置條件契約69
425 CPS的前置條件契約70
43 混成程序的邏輯公式71
44 微分動態邏輯73
441 微分動態邏輯的語法73
442 微分動態邏輯的語義75
45 邏輯形式的CPS契約77
46 查明CPS的需求78
47 總結82
48 附錄82
481 順序合成證明的中間條件82
482 選擇的證明84
483 測試的證明85
習題86
參考文獻90
第5章 動態系統與動態公理92
51 引言92
52 CPS的中間條件93
53 動態系統的動態公理95
531 非確定性選擇的動態公理95
532 公理的可靠性97
533 賦值的動態公理98
534 微分方程的動態公理99
535 測試的動態公理101
536 順序合成的動態公理102
537 循環的動態公理104
538 尖括號模態的公理105
54 短暫彈跳球的證明105
55 總結107
56 附錄108
561 模態肯定前件在方括號模態中的蘊涵108
562 如果沒有任何相關變化，則為空虛狀態變化109
563 哥德爾將永真性泛化到方括號模態中109
564 后置條件的單調性110
565 自由變量和約束變量111
566 自由變量和約束變量分析111
習題113
參考文獻116
第6章 真理與證明118
61 引言118
62 真理和證明119
621 相繼式120
622 證明122
623 命題證明規則122
624 證明規則的可靠性126
625 動態的證明127
626 量詞證明規則129
63 派生證明規則131
64 單跳彈跳球的相繼式證明132
65 實算術證明規則133
651 實數量詞消除法134
652 實例化實算術量詞136
653 通過去除假設來弱化實算術137
654 相繼式演算中的結構證明規則138
655 在公式中代入等式139
656 縮寫項以降低復雜性139
657 創造性地切割實算術轉化問題140
66 總結140
習題141
參考文獻143
第7章 控制回路與不變式145
71 引言145
72 控制循環146
73 循環回路147
731 循環的歸納公理147
732 循環的歸納規則149
733 循環不變式150
734 上下文可靠性需求153
74 一個歡快重復的彈跳球的證明154
75 將后置條件拆分為單獨的情況158
76 總結159
77 附錄159
771 證明的循環159
772 打破證明循環161
773 循環的不變式證明163
774 歸納公理的替代形式163
習題165
參考文獻166
展開全部
信息物理系統邏輯基礎 作者簡介
安德烈·普拉澤（André Platzer） 卡內基·梅隆大學計算機科學系教授。他擁有德國奧爾登堡大學的博士學位。研究領域包括形式化方法、編程語言和純邏輯與應用邏輯。他曾于2009年獲得ACM最佳博士論文榮譽提名獎，2011年獲得NSF杰出青年獎，并入選美國Popular Science雜志2009年“十大杰出青年科學家”、IEEE Intelligent Systems雜志2010年“AI十大潛力人物”。
書友推薦
- >
李白與唐代文化
- >
自卑與超越
- >
月亮虎
- >
人文閱讀與收藏·良友文學叢書:一天的工作
- >
名家帶你讀魯迅:朝花夕拾
- >
推拿
- >
姑媽的寶刀
- >
企鵝口袋書系列·偉大的思想20:論自然選擇(英漢雙語)
本類暢銷
