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

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

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

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