隨機進程代數(shù)的等價性判定計算.pdf

1、隨機進程代數(shù)(SPA)是一種功能與性能相結合的并發(fā)系統(tǒng)模型，是通過給經典進程代數(shù)模型中的動作發(fā)生附加上一個隨機變量值，來反映在系統(tǒng)的運行中，動作出現(xiàn)的時間延遲規(guī)律而得到的模型。它既能夠描述系統(tǒng)的功能，又能夠對系統(tǒng)運行的性能進行評價，很多涉及資源共享的系統(tǒng)，例如，大型計算、客戶-服務器結構、網(wǎng)絡等都可以用這種隨機模型作精確的形式化描述。隨機進程代數(shù)中應用最廣泛的是馬爾可夫進程代數(shù)，在馬爾可夫進程代數(shù)中，動作出現(xiàn)的隨機延遲時間是滿足指數(shù)分布

2、的隨機變量。本論文主要研究了馬爾可夫隨機進程代數(shù)的各種操作語義模型，在這些語義模型下的等價性概念的定義，以及對馬爾可夫隨機進程的等價性進行判定的計算算法。主要包括以下三方面的內容： 1．馬爾可夫鏈代數(shù)上的模擬等價判定。馬爾可夫鏈代數(shù)是進程間只有時間延遲轉移的進程代數(shù)，連續(xù)時間馬爾可夫鏈(CTMC)代數(shù)是并發(fā)系統(tǒng)性能評價最早使用的模型。通過狀態(tài)轉移的馬爾可夫鏈分析，可給出系統(tǒng)的性能指標的刻畫。在一個CTMC代數(shù)模型上的互模擬等價關

3、系是以狀態(tài)間滿足的轉移概率值為基礎定義的，這和CTMC上的聚集等價關系一致，所以給出了基于狀態(tài)的“聚集塊”的等價塊劃分算法，并給出了算法的復雜度分析。 2．交互式馬爾可夫鏈(IMC)代數(shù)上的等價性判定。交互式馬爾可夫鏈代數(shù)是通過正交結合經典的進程代數(shù)和連續(xù)時間馬爾可夫鏈代數(shù)得到的隨機進程代數(shù)模型。本文研究了IMC上的互模擬等價的計算，計算算法的主要思想是對動作和概率轉移分別進行劃分細化計算，最終得到一個遞減關系鏈的不動點，從而得

4、到互模擬等價。并在CTMC模型的弱模擬等價定義的基礎上提出了IMC上強(弱)模擬等價的概念，并且給出了判定模擬前序關系的計算算法，算法的主要思想是通過求解一個線性方程組，判定兩個狀態(tài)的馬爾可夫模擬關系，并去掉所有不能進行模擬的狀態(tài)對。 3．一般隨機進程代數(shù)上的等價性判定。一般隨機進程代數(shù)是指既有動作轉移，又有帶隨機時間延遲的動作轉移的進程代數(shù)。這種進程代數(shù)的一個關鍵點是如何定義兩個并發(fā)進程巾同步馬爾可夫動作轉移的隨機延遲分布φ(