●前言
第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連續隨機邏輯
……

《隨機模型檢測理論與應用》是作者多年從事隨機模型檢測相關科研工作的結晶。《隨機模型檢測理論與應用》致力於緩解隨機模型檢測中的狀態空間爆炸問題，深入繫統地論述克服狀態空間爆炸的兩種基本技術：限界模型檢測技術與抽像技術。首先，介紹離散時間馬爾可夫鏈、馬爾可夫決策過程、連續時間馬爾可夫鏈和概率實時解釋繫統中的限界檢測技術。然後，討論模型檢測概率、實時認知時態邏輯中的二值與三值抽像技術。最後，探討隨機模型檢測技術在雲計算和物聯網領域的應用。