《隨機模型檢測理論與套用》是2014年科學出版社出版的圖書，作者是周從華。
基本介紹
- 書名：隨機模型檢測理論與套用
- 出版社：科學出版社
- 頁數：203頁
- 開本：5
- 作者：周從華
- 出版日期：2014年9月1日
- 語種：簡體中文
- ISBN：7030418921
內容簡介,圖書目錄,
內容簡介
《隨機模型檢測理論與套用》是作者多年從事隨機模型檢測相關科研工作的結晶.《隨機模型檢測理論與套用》致力於緩解隨機模型檢測中的狀態空間爆炸問題,深入系統地論述克服狀態空間爆炸的兩種基本技術:限界模型檢測技術與抽象技術.首先,介紹離散時間馬爾可夫鏈、馬爾可夫決策過程、連續時間馬爾可夫鏈和機率實時解釋系統中的限界檢測技術.然後,討論模型檢測機率、實時認知時態邏輯中的二值與三值抽象技術.最後,探討隨機模型檢測技術在雲計算和物聯網領域的套用.
《隨機模型檢測理論與套用》可作為高等院校計算機專業高年級本科生和研究生的教材，也可供相關領域的科研人員參考。
圖書目錄
前言
第1章隨機模型檢測概述
1.1模型檢測
1.2狀態空間約簡
1.2.1基於有序二叉決策圖的符號化模型檢測方法
1.2.2基於命題公式可滿足性判定的限界模型檢測方法
1.2.3抽象方法
1.2.4組合驗證
1.2.5其他約簡方法
1.3線性時態邏輯的限界模型檢測
1.3.1示例
1.3.2線性時態邏輯
1.3.3線性時態邏輯的限界語義
1.3.4轉換
1.4抽象
1.4.1互模擬與模擬
1.4.2數據抽象
1.5隨機模型檢測
1.6本章小結
參考文獻
第2章離散時間馬爾可夫鏈的限界模型檢測
2.1概述
2.2離散時間馬爾可夫鏈與機率計算樹邏輯
2.3機率計算樹邏輯的限界模型檢測
2.3.1機率計算樹邏輯的等價性
2.3.2機率計算樹邏輯的限界語義
2.3.3限界模型檢測過程終止的判斷
2.3.4機率計算樹邏輯的限界模型檢測算法
2.4實例：IPv4零配置協定
2.5實驗結果
2.6限界模型檢測過程終止判斷標準的修正
2.7相關工作
2.8本章小結
參考文獻
第3章馬爾可夫決策過程的限界模型檢測
3.1概述
3.2馬爾可夫決策過程與機率計算樹邏輯
3.3機率計算樹邏輯的限界模型檢測
3.3.1機率計算樹邏輯的等價性
3.3.2機率計算樹邏輯的限界語義
3.3.3限界模型檢測過程終止的判斷
3.3.4限界模型檢測算法
3.4實例研究
3.5實驗結果
3.6終止標準的修正
3.7本章小結
參考文獻
第4章連續時間馬爾可夫鏈的限界模型檢測
4.1連續隨機邏輯與連續時間馬爾可夫鏈
4.1.1連續隨機邏輯
4.1.2連續時間馬爾可夫鏈
4.1.3轉移機率與極限機率
4.1.4連續隨機邏輯的語義
4.2連續隨機邏輯的限界模型檢測
4.2.1連續隨機邏輯的限界語義
4.2.2限界下轉移機率的計算
4.2.3限界檢測算法
4.3實驗結果
4.4本章小結
參考文獻
第5章多智體系統的限界模型檢測
5.1概述
5.2相關工作
5.3機率實時解釋系統
5.3.1機率時間自動機
5.3.2機率時間自動機的平行組合
5.3.3機率時間自動機的語義
5.3.4機率實時解釋系統
5.4機率實時認知邏輯
5.4.1機率實時認知邏輯的語法
5.4.2機率實時認知邏輯的語義
5.5機率知識區域圖
5.6基於機率知識區域圖的限界模型檢測
5.6.1時態邏輯的轉換
5.6.2轉換邏輯的限界模型檢測
5.7限界模型檢測算法
5.8線性方程組的求解
5.9實例研究
5.9.1火車穿越控制系統
5.9.2控制系統的限界模型檢測
5.10終止性選擇標準
5.11本章小結
參考文獻
第6章模型檢測多智體系統中的抽象技術
6.1概述
6.2相關工作
6.3解釋系統與時態邏輯
6.4驗證屬性驅動的抽象
6.4.1屬性驅動的存在性抽象
6.4.2屬性的可滿足性保持
6.5反例真實性確認
6.5.1什麼是反例
6.5.2識別虛假反例
6.5.3反例引導的求精
6.6實例研究
6.6.1撲克遊戲
6.6.2抽象
6.7實驗
6.7.1密碼學家就餐協定
6.7.2實驗結果
6.8本章小結
參考文獻
第7章機率時態認知邏輯模型檢測中的抽象技術
7.1機率時態認知邏輯語法和語義
7.2建立抽象模型
7.3屬性保持關係
7.4機率時態認知邏輯模型檢測算法
7.5抽象模型的求精
7.5.1抽象失敗原因分析
7.5.2抽象求精
7.6模型檢測密碼學家就餐協定
7.6.1密碼學家就餐協定的機率Kripke結構
7.6.2建立密碼學家就餐協定的抽象模型
7.6.3實驗結果
7.7本章小結
參考文獻
第8章實時時態認知邏輯模型檢測中的抽象技術
8.1實時時態認知邏輯語法和語義
8.1.1實時時態認知邏輯的語法
8.1.2實時解釋系統
8.1.3實時時態認知邏輯的語義
8.2建立抽象模型
8.3屬性保持關係
8.4實例分析
8.4.1鐵路道口系統介紹
8.4.2建立鐵路道口系統的抽象模型
8.4.3模型檢測鐵路道口系統
8.5抽象模型及實時時態認知邏輯的三值語義
8.6三值抽象下的屬性保持關係
8.7模型檢測主動結構控制系統
8.7.1主動結構控制系統的一個演變形式
8.7.2建立主動結構控制系統的抽象模型
8.7.3模型檢測主動結構控制系統
8.8鐵路道口系統的進一步驗證
8.9本章小結
參考文獻
……
第9章快速安全協定的性能分析
第10章IEEE802.11P中MAC協定的性能分析
第11章RFID中S—ALOHA協定的性能分析
第1章隨機模型檢測概述
1.1模型檢測
1.2狀態空間約簡
1.2.1基於有序二叉決策圖的符號化模型檢測方法
1.2.2基於命題公式可滿足性判定的限界模型檢測方法
1.2.3抽象方法
1.2.4組合驗證
1.2.5其他約簡方法
1.3線性時態邏輯的限界模型檢測
1.3.1示例
1.3.2線性時態邏輯
1.3.3線性時態邏輯的限界語義
1.3.4轉換
1.4抽象
1.4.1互模擬與模擬
1.4.2數據抽象
1.5隨機模型檢測
1.6本章小結
參考文獻
第2章離散時間馬爾可夫鏈的限界模型檢測
2.1概述
2.2離散時間馬爾可夫鏈與機率計算樹邏輯
2.3機率計算樹邏輯的限界模型檢測
2.3.1機率計算樹邏輯的等價性
2.3.2機率計算樹邏輯的限界語義
2.3.3限界模型檢測過程終止的判斷
2.3.4機率計算樹邏輯的限界模型檢測算法
2.4實例：IPv4零配置協定
2.5實驗結果
2.6限界模型檢測過程終止判斷標準的修正
2.7相關工作
2.8本章小結
參考文獻
第3章馬爾可夫決策過程的限界模型檢測
3.1概述
3.2馬爾可夫決策過程與機率計算樹邏輯
3.3機率計算樹邏輯的限界模型檢測
3.3.1機率計算樹邏輯的等價性
3.3.2機率計算樹邏輯的限界語義
3.3.3限界模型檢測過程終止的判斷
3.3.4限界模型檢測算法
3.4實例研究
3.5實驗結果
3.6終止標準的修正
3.7本章小結
參考文獻
第4章連續時間馬爾可夫鏈的限界模型檢測
4.1連續隨機邏輯與連續時間馬爾可夫鏈
4.1.1連續隨機邏輯
4.1.2連續時間馬爾可夫鏈
4.1.3轉移機率與極限機率
4.1.4連續隨機邏輯的語義
4.2連續隨機邏輯的限界模型檢測
4.2.1連續隨機邏輯的限界語義
4.2.2限界下轉移機率的計算
4.2.3限界檢測算法
4.3實驗結果
4.4本章小結
參考文獻
第5章多智體系統的限界模型檢測
5.1概述
5.2相關工作
5.3機率實時解釋系統
5.3.1機率時間自動機
5.3.2機率時間自動機的平行組合
5.3.3機率時間自動機的語義
5.3.4機率實時解釋系統
5.4機率實時認知邏輯
5.4.1機率實時認知邏輯的語法
5.4.2機率實時認知邏輯的語義
5.5機率知識區域圖
5.6基於機率知識區域圖的限界模型檢測
5.6.1時態邏輯的轉換
5.6.2轉換邏輯的限界模型檢測
5.7限界模型檢測算法
5.8線性方程組的求解
5.9實例研究
5.9.1火車穿越控制系統
5.9.2控制系統的限界模型檢測
5.10終止性選擇標準
5.11本章小結
參考文獻
第6章模型檢測多智體系統中的抽象技術
6.1概述
6.2相關工作
6.3解釋系統與時態邏輯
6.4驗證屬性驅動的抽象
6.4.1屬性驅動的存在性抽象
6.4.2屬性的可滿足性保持
6.5反例真實性確認
6.5.1什麼是反例
6.5.2識別虛假反例
6.5.3反例引導的求精
6.6實例研究
6.6.1撲克遊戲
6.6.2抽象
6.7實驗
6.7.1密碼學家就餐協定
6.7.2實驗結果
6.8本章小結
參考文獻
第7章機率時態認知邏輯模型檢測中的抽象技術
7.1機率時態認知邏輯語法和語義
7.2建立抽象模型
7.3屬性保持關係
7.4機率時態認知邏輯模型檢測算法
7.5抽象模型的求精
7.5.1抽象失敗原因分析
7.5.2抽象求精
7.6模型檢測密碼學家就餐協定
7.6.1密碼學家就餐協定的機率Kripke結構
7.6.2建立密碼學家就餐協定的抽象模型
7.6.3實驗結果
7.7本章小結
參考文獻
第8章實時時態認知邏輯模型檢測中的抽象技術
8.1實時時態認知邏輯語法和語義
8.1.1實時時態認知邏輯的語法
8.1.2實時解釋系統
8.1.3實時時態認知邏輯的語義
8.2建立抽象模型
8.3屬性保持關係
8.4實例分析
8.4.1鐵路道口系統介紹
8.4.2建立鐵路道口系統的抽象模型
8.4.3模型檢測鐵路道口系統
8.5抽象模型及實時時態認知邏輯的三值語義
8.6三值抽象下的屬性保持關係
8.7模型檢測主動結構控制系統
8.7.1主動結構控制系統的一個演變形式
8.7.2建立主動結構控制系統的抽象模型
8.7.3模型檢測主動結構控制系統
8.8鐵路道口系統的進一步驗證
8.9本章小結
參考文獻
……
第9章快速安全協定的性能分析
第10章IEEE802.11P中MAC協定的性能分析
第11章RFID中S—ALOHA協定的性能分析
