基于μ-演算的局部模型檢測(cè)算法設(shè)計(jì).pdf

1、隨著計(jì)算機(jī)軟件系統(tǒng)、硬件系統(tǒng)的發(fā)展，系統(tǒng)也變得越來(lái)越復(fù)雜，因此設(shè)法保證系統(tǒng)的正確性和可靠性變得越來(lái)越重要。為此，許多學(xué)者投入到該問(wèn)題的研究中，并提出了很多理論與方法，模型檢測(cè)因高度自動(dòng)化而引起了學(xué)者的關(guān)注。模型檢測(cè)是一種形式化驗(yàn)證技術(shù)。其過(guò)程就是通過(guò)對(duì)系統(tǒng)建立模型，然后驗(yàn)證該模型是否滿足給定的性質(zhì)。在模型檢測(cè)常用的邏輯中，命題μ-演算吸引了很多學(xué)者的興趣，它是由Kozen提出的，是個(gè)表達(dá)能力很強(qiáng)的邏輯語(yǔ)言，其較強(qiáng)的表達(dá)能力主要來(lái)自于最大

2、不動(dòng)點(diǎn)算子和最小不動(dòng)點(diǎn)算子的交替嵌套。由于命題μ-演算有著較強(qiáng)的表達(dá)能力，因此其它一些邏輯驗(yàn)證都可以轉(zhuǎn)換為命題μ-演算來(lái)驗(yàn)證，而且驗(yàn)證效率也較高。模型檢測(cè)需要對(duì)系統(tǒng)狀態(tài)空間進(jìn)行窮舉搜索，驗(yàn)證并發(fā)系統(tǒng)時(shí)，其狀態(tài)數(shù)是呈指數(shù)增長(zhǎng)的。
　　目前已經(jīng)有許多關(guān)于命題μ-演算的模型檢測(cè)算法，這些算法可以分為全局模型檢測(cè)算法和局部模型檢測(cè)算法。對(duì)于命題μ-演算，目前已知的最好的局部模型檢測(cè)算法的時(shí)間復(fù)雜度與交替嵌套深度d呈指數(shù)關(guān)系，其復(fù)雜度較高，

3、本文將對(duì)其不動(dòng)點(diǎn)交替嵌套迭代過(guò)程進(jìn)行分析，提出時(shí)間復(fù)雜度較低的局部模型檢測(cè)算法。
　　本文從命題μ-演算出發(fā)，研究不動(dòng)點(diǎn)交替嵌套迭代的中間結(jié)果之間的偏序關(guān)系，設(shè)計(jì)高效的局部模型檢測(cè)算法，并對(duì)算法的復(fù)雜度進(jìn)行研究分析。本文主要分為三個(gè)部分：
　　第一部分主要分析基于命題μ-演算的局部模型檢測(cè)算法，對(duì)其不動(dòng)點(diǎn)交替嵌套迭代過(guò)程進(jìn)行分析，然后從三支決策的角度改進(jìn)算法。
　　第二部分主要分析不動(dòng)點(diǎn)交替嵌套迭代過(guò)程的中間結(jié)果之間的