概率邏輯的限界模型檢測(cè)技術(shù).pdf

1、模型檢測(cè)是一種自動(dòng)化程度非常高的有限狀態(tài)系統(tǒng)驗(yàn)證技術(shù)，目前已經(jīng)在計(jì)算機(jī)硬件、通信與安全協(xié)議、軟件可靠性的驗(yàn)證方面獲得了較大的成功。傳統(tǒng)模型檢測(cè)技術(shù)關(guān)注的是系統(tǒng)行為的絕對(duì)正確性，如系統(tǒng)不能進(jìn)入死鎖狀態(tài)。然而分布式算法，多媒體協(xié)議，容錯(cuò)系統(tǒng)等往往關(guān)心某種量化屬性，如消息傳送失敗的概率不高于1％，在時(shí)間t內(nèi)至多m個(gè)消息丟失的概率不高于0.8％，請(qǐng)求發(fā)送后在5到7個(gè)時(shí)間單元內(nèi)得到響應(yīng)的概率不低于70％等等。隨機(jī)模型檢測(cè)致力于解決這類屬性的自動(dòng)化

2、驗(yàn)證問題。
　　 在隨機(jī)模型檢測(cè)中一般使用概率計(jì)算樹邏輯PCTL和連續(xù)隨機(jī)邏輯CSL刻畫屬性，使用馬爾科夫過程，概率時(shí)間自動(dòng)機(jī)等建立系統(tǒng)模型。與傳統(tǒng)模型檢測(cè)一樣，狀態(tài)空間爆炸問題也是隨機(jī)模型檢測(cè)技術(shù)實(shí)用化的主要瓶頸。在為緩解狀態(tài)空間爆炸問題已經(jīng)提出的諸多理論和方法中，限界模型檢測(cè)技術(shù)是克服狀態(tài)空間爆炸問題的最為有效的方法之一。本文主要工作是提出了概率獎(jiǎng)勵(lì)計(jì)算樹邏輯和概率實(shí)時(shí)認(rèn)知邏輯的限界模型檢測(cè)技術(shù)，具體包括以下兩個(gè)方面:

3、>　　 1.概率獎(jiǎng)勵(lì)計(jì)算樹邏輯以離散時(shí)間馬爾可夫鏈作為系統(tǒng)模型，為緩解該模型上的狀態(tài)空間爆炸問題，提出了概率獎(jiǎng)勵(lì)計(jì)算樹邏輯的限界檢測(cè)技術(shù)。首先定義概率獎(jiǎng)勵(lì)計(jì)算樹邏輯的限界語義，并證明其正確性;其次提出基于線性方程組求解的限界模型檢測(cè)算法;然后通過實(shí)例說明了限界模型檢測(cè)的過程。最后在概率獎(jiǎng)勵(lì)計(jì)算樹邏輯的基礎(chǔ)上提出了重復(fù)可達(dá)性和持續(xù)性的限界語義和限界模型檢測(cè)算法，并以實(shí)例來說明限界模型檢測(cè)的過程。實(shí)驗(yàn)結(jié)果表明在屬性成立的證據(jù)較短的情況下，

4、限界模型檢測(cè)能夠快速的完成驗(yàn)證。
　　 2.為了形式化描述多智體系統(tǒng)中與概率、實(shí)時(shí)、知識(shí)相關(guān)的性質(zhì)，提出了一種概率實(shí)時(shí)認(rèn)知邏輯PTCTLK。模型檢測(cè)是驗(yàn)證多智體系統(tǒng)是否滿足PTCTLK公式的主要技術(shù)，狀態(tài)空間爆炸是該技術(shù)實(shí)用化的主要瓶頸。為此提出一種PTCTLK的限界模型檢測(cè)算法。首先，將PTCTLK的模型檢測(cè)問題轉(zhuǎn)換為無實(shí)時(shí)算子的PBTLK的模型檢測(cè)問題;其次，定義PBTLK的限界語義，并證明其正確性;然后，設(shè)計(jì)基于線性方程組