概率和實(shí)時(shí)時(shí)態(tài)認(rèn)知邏輯模型檢測(cè)中的抽象技術(shù).pdf

1、模型檢測(cè)是一種很重要的有限狀態(tài)系統(tǒng)的自動(dòng)驗(yàn)證技術(shù),已經(jīng)應(yīng)用到了通信協(xié)議、硬件檢測(cè)、控制系統(tǒng)等領(lǐng)域的驗(yàn)證中并受到了廣泛的關(guān)注。時(shí)態(tài)認(rèn)知邏輯是一種屬性規(guī)范描述語(yǔ)言,用模型檢測(cè)的方法對(duì)時(shí)態(tài)認(rèn)知邏輯描述的屬性進(jìn)行驗(yàn)證對(duì)確保系統(tǒng)的可靠性具有重要的意義。在時(shí)態(tài)認(rèn)知邏輯中加入概率因素可得到概率時(shí)態(tài)認(rèn)知邏輯,時(shí)態(tài)認(rèn)知邏輯與實(shí)時(shí)因素結(jié)合可得到實(shí)時(shí)時(shí)態(tài)認(rèn)知邏輯。
　　 與傳統(tǒng)模型檢測(cè)一樣,概率時(shí)態(tài)認(rèn)知邏輯和實(shí)時(shí)時(shí)態(tài)認(rèn)知邏輯模型檢測(cè)也面臨著狀態(tài)空間爆

2、炸問題。在為緩解狀態(tài)空間爆炸問題所提出的諸多理論和方法中,抽象技術(shù)是克服狀態(tài)空間爆炸問題的最為有效的方法之一。本文對(duì)概率和實(shí)時(shí)時(shí)態(tài)認(rèn)知邏輯模型檢測(cè)中的抽象技術(shù)進(jìn)行了系統(tǒng)的研究,有效的緩解了狀態(tài)空間爆炸問題。
　　 本文的主要研究?jī)?nèi)容包括:
　　 1.為緩解概率時(shí)態(tài)認(rèn)知邏輯模型檢測(cè)中的狀態(tài)空間爆炸問題,提出了三值抽象技術(shù)。建立了概率Kripke結(jié)構(gòu)的抽象模型,它的主要特點(diǎn)是利用概率轉(zhuǎn)換區(qū)間替換了原始模型中的概率轉(zhuǎn)換。證明了

3、由抽象技術(shù)演繹得到的抽象模型既是原始模型的上近似,又是它的下近似。開發(fā)了在抽象狀態(tài)空間上檢測(cè)概率時(shí)態(tài)認(rèn)知邏輯屬性的算法。為了確保抽象技術(shù)的完備性,給出了最小證據(jù)和最小反例引導(dǎo)的抽象系統(tǒng)求精的算法。最后通過Dining Cryptographer協(xié)議來(lái)說明抽象技術(shù)在約簡(jiǎn)系統(tǒng)狀態(tài)空間方面的效果。
　　 2.為解決實(shí)時(shí)時(shí)態(tài)認(rèn)知邏輯模型檢測(cè)中的狀態(tài)空間爆炸問題,提出了一種二值抽象技術(shù):對(duì)于實(shí)時(shí)時(shí)態(tài)認(rèn)知邏輯TACTLK中的實(shí)時(shí)部分TACT

4、L,采用抽象離散時(shí)鐘賦值;對(duì)于TACTLK中的認(rèn)知算子K,提出了抽象狀態(tài)關(guān)于智體認(rèn)知等價(jià)的定義。建立了實(shí)時(shí)解釋系統(tǒng)的抽象模型,并證明了由抽象技術(shù)演繹得到的抽象模型是原始模型的上近似。最后,通過對(duì)鐵路道口系統(tǒng)的狀態(tài)空間的簡(jiǎn)化來(lái)說明抽象技術(shù)的有效性。
　　 3.由于在二值抽象技術(shù)下,由抽象技術(shù)演繹得到的抽象模型只是原始模型的上近似。若待驗(yàn)證的屬性在抽象模型中不成立,不能推出該屬性在原始模型中也是不成立的。三值抽象技術(shù)可有效克服這一不