隨機(jī)進(jìn)程代數(shù)的等價(jià)性判定計(jì)算.pdf

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

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

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

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