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

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

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

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

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