交互式馬爾可夫鏈：并發(fā)系統(tǒng)的設(shè)計(jì)、驗(yàn)證與評(píng)價(jià)

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