等價化簡和抽象的概率模型檢測.pdf

1、模型檢測是一項(xiàng)很成功的自動化系統(tǒng)驗(yàn)證技術(shù)，對于不滿足的驗(yàn)證屬性，需要額外輸出一個反例。為了生成更好的模型反例，對原始系統(tǒng)模型進(jìn)行等價化簡和抽象。
　　在概率模型檢測中，使用離散時間的馬爾科夫鏈描述系統(tǒng)，使用時態(tài)邏輯的分支概率計算樹時態(tài)邏輯表示系統(tǒng)的屬性。本文設(shè)計了新的概率模型檢測算法，針對特定的模型屬性，將系統(tǒng)模型轉(zhuǎn)化為僅僅含有單個初始狀態(tài)和單個目標(biāo)狀態(tài)的馬爾科夫鏈模型。根據(jù)狀態(tài)之間的傳遞關(guān)系，得到新模型上的初始狀態(tài)傳遞閉包和目標(biāo)

2、狀態(tài)逆?zhèn)鬟f閉包，進(jìn)而實(shí)現(xiàn)對原始模型的等價化簡。采用深度優(yōu)先算法獲得所有極小連通分量，通過將抽象后的極小連通分量代替原始模型中的極小連通分量，進(jìn)而實(shí)現(xiàn)對原始模型的等價抽象。在無環(huán)路的模型上，采用關(guān)鍵子系統(tǒng)描述反例，采用局部搜索和全局搜索兩種策略生成反例，采用預(yù)防避免策略防止新路徑重復(fù)，采用運(yùn)籌學(xué)上最短路徑的算法獲得大概率路徑。
　　綜上所述，本文針對離散時間的馬爾科夫鏈模型，設(shè)計了一套基于等價化簡和抽象的反例生成框架。選取領(lǐng)導(dǎo)選舉協(xié)