交互式馬爾可夫鏈：并發(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)的層次化沒計(jì)分析
　1.2 研究內(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 本書組織
第二章 預(yù)備知識(shí)
　2.1 概率、隨機(jī)變量與分布函數(shù)
　　2.1.1 測度空間與概率空間
　　2.1.2 隨機(jī)變量及其分布函數(shù)
　2.2 隨機(jī)過程
　　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ù)刻畫
　3.5 IMC的邏輯刻畫
　　3.5.1 IMC的路徑及其上的概率
　　3.5.2 aCSL邏輯的語法
　　3.5.3 aCSL邏輯的語義
第四章 分支時(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 同余性問題
　5.2 基本假設(shè)
　5.3 基于IMC代數(shù)刻畫的語法細(xì)化
　5.4 語義細(xì)化
　5.5 性質(zhì)
　　5.5.1 交織語義的等價(jià)關(guān)系概念
　　5.5.2 同余性
　　5.5.3 語法和語義細(xì)化的一致性
第六章 模型檢驗(yàn)
　6.1 概述
　6.2 基本原理
　6.3 IMC邏輯刻畫的表達(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)