互動式馬爾可夫鏈

《互動式馬爾可夫鏈》是2007年6月1日科學出版社出版的圖書。本書主要介紹了IMC的理論及其在並發系統層次化設計以及功能驗證與性能評價方面的套用。

基本介紹

• 中文名：互動式馬爾可夫鏈 
• 出版社： 科學出版社
• 正文語種： 簡體中文
• 出版時間：2007年6月1日
• 叢書名：數學機械化叢書
• 包裝：平裝
• isbn：9787030188663, 7030188667
• 開本：5

內容簡介

《互動式馬爾可夫鏈:並發系統的設計、驗證與評價》主要內容包括IMC上的分支時間等價和前序關係、IMC的動作細化理論以及基於IMC的模型檢驗方法。通過正交結合經典的進程代數和連續時間馬爾可夫鏈模型，互動式馬爾可夫鏈(IMC)提供了完美的可組合化的並發系統設計和分析框架。《互動式馬爾可夫鏈:並發系統的設計、驗證與評價》可以供研究生、教師和科研人員作為了解並發系統理論研究及與數學機械化基本思想與方法相結合的形式在設計與分析技術最新成果的參考書。

圖書目錄

第一章 緒論

1.1 研究背景

1.1.1 並發系統的功能分析

1.1.2 並發系統的性能分析

1.1.3 並發系統的層次化沒計分析

1.2 研究內容

1.2.1 等價關係

1.2.2 模型檢驗

1.2.3 動作細化

1.2.4 相關工作

1.3 本書組織

第二章 預備知識

2.1 機率、隨機變數與分布函式

2.1.1 測度空間與機率空間

2.1.2 隨機變數及其分布函式

2.2 隨機過程

2.2.1 離散時間馬爾可夫鏈

2.2.2 連續時間馬爾可夫鏈

2.2.3 馬爾可夫分析

第三章 互動式馬爾可夫鏈

3.1 進程代數與標記轉移系統

3.2 帶標記的連續時間馬爾可夫鏈

3.3 互動式馬爾可夫鏈(IMC)

3.3.1 隨機進程代數模型

3.3.2 互動式馬爾可夫鏈

3.4 IMC的代數刻畫

3.5 IMC的邏輯刻畫

3.5.1 IMC的路徑及其上的機率

3.5.2 aCSL邏輯的語法

3.5.3 aCSL邏輯的語義

第四章 分支時間等價和前序關係

4.1 概述

4.2 互模擬等價關係

4.2.1 強互模擬等價

4.2.2 弱互模擬等價

4.3 模擬前序關係

4.3.1 強模擬前序關係

4.3.2 弱模擬前序關係

4.4 邏輯特徵

4.4.1 互模擬關係的邏輯特徵

4.4.2 模擬關係的邏輯特徵

4.5 小結

第五章 動作細化

5.1 概述

5.1.1 什麼是動作細化

5.1.2 動作細化的不同觀點

5.1.3 同餘性問題

5.2 基本假設

5.3 基於IMC代數刻畫的語法細化

5.4 語義細化

5.5 性質

5.5.1 交織語義的等價關係概念

5.5.2 同餘性

5.5.3 語法和語義細化的一致性

第六章 模型檢驗

6.1 概述

6.2 基本原理

6.3 IMC邏輯刻畫的表達能力回顧

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 算法效率分析及最佳化考慮

6.6.1 算法效率分析

6.6.2 最佳化考慮

參考文獻