1、分布式算法在實際應用中具有重要的價值意義,本文采用一種基于概率模型檢測技術(shù)驗證和分析了兩類分布式算法的性質(zhì),并這些性質(zhì)給出了相應的證明。由于概率模型檢測可以窮舉狀態(tài)空間,相比于傳統(tǒng)方法,使得它更接近真實應用環(huán)境,更利于我們研究算法的安全性和有效性;同時概率模型檢測器中的馬爾科夫技術(shù)可以分析出模型中那些不確定因素。
　　隨機分布式算法中有一種自動恢復狀態(tài)的算法—自穩(wěn)定算法, Mitchell Flatebo提出的自穩(wěn)定算法是通過一個

2、簡單隨機的解決方案解決n個進程令牌環(huán)中的故障,使故障自動恢復正常。他證明出最壞的情況有n-1個令牌,所需要的時間的上界是0.5N2-0.5N-2。從實驗中,發(fā)現(xiàn)這個上限出現(xiàn)的可能很小。而在實際應用中,我們更注重系統(tǒng)預期恢復穩(wěn)定狀態(tài)的時間—預期最差時間。實驗中,主要采用PRISM工具驗證了Flatebo算法的性質(zhì),并且把它與同類型Herman自穩(wěn)定算法做了比較,當系統(tǒng)中的結(jié)點數(shù)目增加時,它的性能會逐漸提高,優(yōu)于Herman算法;另外,還用

3、線性回歸從實驗結(jié)果中擬合出預期最差時間在O(N1.45)和O(N1.47)之間;最后還給出一個驗證和分析自穩(wěn)定算法的簡單方法。
　　本文研究的另一個分布式算法是隨機互斥算法,提出了一個基于概率模型檢測工具PRISM方法,用于驗證和分析Kerry Raymond提出的分布式K互斥算法,首先驗證了互斥算法無死鎖和無饑餓兩種基本性質(zhì);然后通過PRISM驗證某一進程進入臨界區(qū)平均及時時間;接著分析我們的實驗結(jié)果,當各個進程的相對訪問臨界區(qū)