交互式馬爾可夫鏈：并發(fā)系統(tǒng)的設(shè)計、驗證與評價

第一章 緒論
　1.1 研究背景
　　1.1.1 并發(fā)系統(tǒng)的功能分析
　　1.1.2 并發(fā)系統(tǒng)的性能分析　　
　　1.1.3 并發(fā)系統(tǒng)的層次化沒計分析
　1.2 研究內(nèi)容
　　1.2.1 等價關(guān)系
　　1.2.2 模型檢驗
　　1.2.3 動作細(xì)化
　　1.2.4 相關(guān)工作
　1.3 本書組織
第二章 預(yù)備知識
　2.1 概率、隨機變量與分布函數(shù)
　　2.1.1 測度空間與概率空間
　　2.1.2 隨機變量及其分布函數(shù)
　2.2 隨機過程
　　2.2.1 離散時間馬爾可夫鏈
　　2.2.2 連續(xù)時間馬爾可夫鏈
　　2.2.3 馬爾可夫分析
第三章 交互式馬爾可夫鏈
　3.1 進(jìn)程代數(shù)與標(biāo)記轉(zhuǎn)移系統(tǒng)
　3.2 帶標(biāo)記的連續(xù)時間馬爾可夫鏈
　3.3 交互式馬爾可夫鏈(IMC)
　　3.3.1 隨機進(jìn)程代數(shù)模型
　　3.3.2 交互式馬爾可夫鏈
　3.4 IMC的代數(shù)刻畫
　3.5 IMC的邏輯刻畫
　　3.5.1 IMC的路徑及其上的概率
　　3.5.2 aCSL邏輯的語法
　　3.5.3 aCSL邏輯的語義
第四章 分支時間等價和前序關(guān)系
　4.1 概述
　4.2 互模擬等價關(guān)系
　　4.2.1 強互模擬等價
　　4.2.2 弱互模擬等價
　4.3 模擬前序關(guān)系
　　4.3.1 強模擬前序關(guān)系
　　4.3.2 弱模擬前序關(guān)系
　4.4 邏輯特征
　　4.4.1 互模擬關(guān)系的邏輯特征
　　4.4.2 模擬關(guān)系的邏輯特征
　4.5 小結(jié)
第五章 動作細(xì)化
　5.1 概述
　　5.1.1 什么是動作細(xì)化
　　5.1.2 動作細(xì)化的不同觀點
　　5.1.3 同余性問題
　5.2 基本假設(shè)
　5.3 基于IMC代數(shù)刻畫的語法細(xì)化
　5.4 語義細(xì)化
　5.5 性質(zhì)
　　5.5.1 交織語義的等價關(guān)系概念
　　5.5.2 同余性
　　5.5.3 語法和語義細(xì)化的一致性
第六章 模型檢驗
　6.1 概述
　6.2 基本原理
　6.3 IMC邏輯刻畫的表達(dá)能力回顧
　6.4 模型檢驗算法
　　6.4.1 基本布爾運算的計算
　　6.4.2 概率算子ρ的計算
　　6.4.3 F(s,t)與G(s,z)的計算
　　6.4.4 IMC模型檢驗算法
　6.5 實例分析
　6.6 算法效率分析及優(yōu)化考慮
　　6.6.1 算法效率分析
　　6.6.2 優(yōu)化考慮
參考文獻(xiàn)