掃一掃
關注中圖網
官方微博
本類五星書更多>
-
>
全國計算機等級考試最新真考題庫模擬考場及詳解·二級MSOffice高級應用
-
>
決戰行測5000題(言語理解與表達)
-
>
軟件性能測試.分析與調優實踐之路
-
>
第一行代碼Android
-
>
JAVA持續交付
-
>
EXCEL最強教科書(完全版)(全彩印刷)
-
>
深度學習
基于PETRI網的計算樹邏輯模型檢測 版權信息
- ISBN：9787030772848
- 條形碼：9787030772848 ; 978-7-03-077284-8
- 裝幀：平裝膠訂
- 冊數：暫無
- 重量：暫無
- 所屬分類：>
基于PETRI網的計算樹邏輯模型檢測 本書特色
介紹了我們開發的模型檢測工具，并針對一些應用實例，展示了我們的模型與檢測算法的優點。
基于PETRI網的計算樹邏輯模型檢測 內容簡介
本書介紹了基于Petri網的計算數邏輯模型檢測方法，主要內容分為以下三個部分：一、基于原型Petri網的計算樹邏輯（CTL）模型檢測，結合OBDD技術提出了一種更高效的驗證方法以緩解它的狀態爆炸問題；二、對多智能體系統的正確性驗證，提出了帶有認知的Petri網，模擬多智能體系統，然后結合OBDD技術提出了一種更高效的驗證計算樹認知邏輯（CTLK）的方法；三、對實時系統的正確性驗證，提出了點區間優先級時間Petri網，模擬搶占式實時系統，如多核多任務實時系統，并由此給出了一種驗證時間計算樹邏輯（TCTL）的方法。同時介紹了我們開發的模型檢測工具，并針對一些應用實例，展示了我們的模型與檢測算法的優點。
基于PETRI網的計算樹邏輯模型檢測 目錄
前言
第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 展望
參考文獻
展開全部
基于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。 何雷鋒，2023年1月獲得同濟大學計算機科學與技術專業博士學位。何雷鋒主要從事Petri網、計算樹邏輯、模型檢測等方面的理論與應用研究。在《軟件學報》、IEEE Transactions on Industrial Informatics、IEEE Transactions on Computational Social Systems等國內外期刊上發表學術論文10余篇，開發了（符號）模型檢測工具。
書友推薦
- >
我與地壇
- >
自卑與超越
- >
龍榆生：詞曲概論/大家小書
- >
推拿
- >
伯納黛特,你要去哪(2021新版)
- >
二體千字文
- >
煙與鏡
- >
苦雨齋序跋文-周作人自編集
本類暢銷
