等價(jià)化簡(jiǎn)和抽象的概率模型檢測(cè).pdf

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

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