基於Petri網的計算樹邏輯模型檢測 劉關俊 何雷鋒 9787030772848 【台灣高等教育出版社】
圖書均為代購，正常情形下，訂後約兩周可抵台。
物品所在地：中國大陸
原出版社：科學
物品所在地：中國大陸
原出版社：科學
NT$687
商品編號:
供貨狀況:
尚有庫存
加入最愛
此商品 「 最高 」可以折抵紅利
0
點
(約等於 NT$0 )
商品介紹
| *數量非實際在台庫存 *完成訂單後正常情形下約兩周可抵台。 *本賣場提供之資訊僅供參考，以到貨標的為實際資訊。 印行年月：202401*若逾兩年請先於私訊洽詢存貨情況，謝謝。 台灣(台北市)在地出版社，每筆交易均開具統一發票，祝您中獎最高1000萬元。 書名：基於Petri網的計算樹邏輯模型檢測 ISBN：9787030772848 出版社：科學 著編譯者：劉關俊 何雷鋒 頁數：208 所在地：中國大陸 *此為代購商品 書號：1606974 可大量預訂，請先連絡。 內容簡介 本書主要介紹原型Petri網、知識Petri網、帶有優先順序的時間Petri網，用於對有限狀態併發系統控制流、安全多方計算協議、多處理器搶佔式實時系統等在一定層級上的抽象建模，如刻畫併發、選擇、衝突、多方交互、多方認知過程、（搶佔式）資源分配、事件的實時性約束等。本書介紹的計算樹邏輯、知識計算樹邏輯、時間計算樹邏輯等可以用於規約這些系統所關注的設計需求，如無死鎖、公平性、隱私性、可調度性、最壞執行時間等。本書重點介紹使用這些Petri網模型驗證以上時序邏輯的演算法。另外，本書介紹簡化有序二叉決策圖，介紹如何將其用於表達Petri網的狀態、狀態間的遷移關係及狀態間的等價關係，並將其應用於計算樹邏輯與知識計算樹邏輯的模型檢測上。 本書可供從事模型檢測、Petri網、形式化方法等理論及其應用方面的研究人員使用。作者簡介 劉關俊，男，教授，博士生導師。2011年獲得同濟大學計算機軟體與理論專業博士學位，同年赴新加坡科技設計大學從事博士后研究工作；2013年回國，並進入同濟大學計算機科學系任教，同年獲得德國洪堡基金資助，赴柏林洪堡大學從事博士后研究工作。 主要從事形式化方法、模型檢測、Petri網等方面的理論與應用研究，目前也從事機器學習及其在網路交易欺詐檢測方面的研究。已出版學術專著1本，發表學術論文90餘篇，包括Science China Information Sciences、ACM Transactions on Embedded Computing Systems、ACM Transactionson Cyber-Physical Systems、IEEE Transactions on Services Computing、IEEE Transactions on Industrial Informatics等期刊論文近50篇，以及國際Petri網年會（International Conference on Application and Theory of Petri Nets and Concurrency）等會議論文40餘篇。 劉關俊主持國家自然科學基金面上項目與青年基金項目、上海市曙光計劃人才項目、中央高校交叉項目（重大）等多項，獲得國家科技進步獎二等獎、上海市科技進步獎一等獎、中國電子學會自然科學一等獎、吳文俊人工智慧技術發明獎一等獎、上海市優秀博士論文獎以及首屆教育部國務院學位委員會博士研究生學術新人獎等。劉關俊是中國計算機學會形式化方法專委會委員、中國自動化學會網路信息服務專委會委員、中國人工智慧學會智能空天系統專委會委員、IEEESenior Member。目錄 前言第1章 緒論 1 1 研究背景 1 2 研究現狀 1 2 1 有限狀態併發系統控制流的模型檢測 1 2 2 安全多方計算協議的模型檢測 1 2 3 多處理器搶佔式實時系統的模型檢測 1 3 內容概述 第2章 基礎知識 2 1 原型Petri網 2 1 1 常用的集合符號 2 1 2 原型Petri網的定義 2 1 3 原型Petri網的性質 2 2 時間Petri網 2 2 1 時間Petri網的定義 2 2 2 時間Petri網的狀態類圖 2 3 優先順序時間Petri網 2 3 1 優先順序時間Petri網的定義 2 3 2 狀態類圖 2 4 模型檢測 第3章 簡化有序二叉決策圖 3 1 布爾函數簡介 3 1 1 布爾函數 3 1 2 布爾函數的其他描述形式 3 2 簡化有序二叉決策圖簡介 3 2 1 ROBDD的定義 3 2 2 ROBDD的性質 3 3 ROBDD的變數排序方法 3 3 1 動態變數排序法 3 3 2 靜態變數排序法 3 4 基於ROBDD符號表達Petri網 3 4 1 基於ROBDD符號表達安全Petri網 3 4 2 基於ROBDD符號表達有界Petri網 第4章 計算樹邏輯模型檢測 4 1 計算樹邏輯 4 1 1 CTL的語法與語義 4 1 2 CTL的標準範式 4 2 CTL的傳統驗證方法 4 3 基於ROBDD的CTL驗證方法 4 3 1 第一種符號模型檢測CTL的方法 4 3 2 第二種符號模型檢測CTL的方法 4 4 應用實例 4 4 1 柔性製造系統 4 4 2 多線程程序 4 5 實驗與分析 4 5 1 哲學家就餐問題 4 5 2 資源分配系統 4 5 3 埃拉托色尼篩選法 4 5 4 n皇后問題 第5章 知識Petri網 5 1 知識Petri網的定義 5 2 帶有等價關係的可達圖RGER 5 3 基於ROBDD符號表達RGER 第6章 知識計算樹邏輯模型檢測 6 1 知識計算樹邏輯 6 2 基於RGER的CTLK的驗證方法 6 3 基於ROBDD的CTLK的驗證方法 6 3 1 第一種符號模型檢測CTLK的方法 6 3 2 第二種符號模型檢測CTLK的方法 6 4 應用實例：密碼學家就餐協議 第7章 帶有計時器的時間Petri網 7 1 傳統的四種帶有計時器的時間Petri網 7 1 1 調度擴展時間Petri網 7 1 2 搶佔式時間Petri網 7 1 3 帶有抑止超弧的時間Petri網 7 1 4 計時器時間Petri網 7 2 優先順序時間點區間Petri網 7 2 1 優先順序時間點區間Petri網PToPN的定義 7 2 2 PToPN的狀態圖 第8章 時間計算樹邏輯模型檢測 8 1 時間計算樹邏輯 8 1 1 TCTL的語法與語義 8 1 2 TCTL的標準範式 8 2 基於 PToPN的TCTL的驗證方法 8 3 帶有時間未知數的時間計算樹邏輯 8 3 1 TCTLx的語法與語義 8 3 2 基於PToPN的TCTLx的驗證方法 8 4 應用實例 8 4 1 系統描述與兩個不同的網模型 8 4 2 基於TCTLx的性質規約 8 4 3 實驗結果與分析 第9章 模型檢測器 9 1 模型檢測器框架概述 9 2 CTL模型檢測器 9 3 CTLK模型檢測器 9 4 TCTL模型檢測器 9 5 TCTLx模型檢測器 第10章 總結與展望 10 1 總結 10 2 展望 參考文獻 詳細資料或其他書籍請至台灣高等教育出版社查詢，查後請於PChome商店街私訊告知ISBN或書號，我們即儘速上架。 |
