基于模擬理論的模型檢測(cè)研究.pdf

1、形式化驗(yàn)證是用嚴(yán)格的數(shù)學(xué)方法來(lái)證明系統(tǒng)設(shè)計(jì)是否滿足規(guī)約的驗(yàn)證方法。近幾年來(lái)基于模型檢測(cè)的形式化驗(yàn)證工具的使用范圍不斷擴(kuò)大，而且大量的實(shí)例證明了模型檢測(cè)在發(fā)現(xiàn)問(wèn)題方面的能力?？梢哉f(shuō)，模型檢測(cè)是自動(dòng)推理在計(jì)算機(jī)科學(xué)中最成功的應(yīng)用之一。
　　 自動(dòng)機(jī)理論為線性時(shí)序邏輯模型檢測(cè)提供了統(tǒng)一的算法框架。標(biāo)準(zhǔn)線性時(shí)序邏輯模型檢測(cè)由線性時(shí)序邏輯公式轉(zhuǎn)換為B(u)chi 自動(dòng)機(jī)、計(jì)算自動(dòng)機(jī)的乘積和積自動(dòng)機(jī)語(yǔ)言判空的三個(gè)步驟構(gòu)成。結(jié)果自動(dòng)機(jī)的質(zhì)量直

2、接決定了模型檢測(cè)的應(yīng)用范圍，因此，產(chǎn)生狀態(tài)數(shù)和遷移數(shù)少，接受狀態(tài)簡(jiǎn)單的自動(dòng)機(jī)成為了模型檢測(cè)的研究重點(diǎn)。
　　 在模型檢測(cè)中，自動(dòng)機(jī)A0 可以替代另一個(gè)自動(dòng)機(jī)A的條件是兩個(gè)自動(dòng)機(jī)所識(shí)別的語(yǔ)言相同，而語(yǔ)言相同的計(jì)算是十分困難的。因?yàn)槟M蘊(yùn)含著語(yǔ)言的包含關(guān)系，而且計(jì)算直接模擬、公平模擬以及延遲模擬的時(shí)間復(fù)雜度為多項(xiàng)式時(shí)間，因此在實(shí)際中一般借助各種模擬的概念來(lái)完成對(duì)自動(dòng)機(jī)的優(yōu)化。K-模擬(當(dāng)K =1 時(shí)對(duì)應(yīng)的就是各種普通模擬)的實(shí)質(zhì)就是

3、對(duì)應(yīng)于反對(duì)者的每次移動(dòng)一顆寶石，擁護(hù)者可以移動(dòng)K 顆寶石?；贙-模擬可以對(duì)B(u)chi 自動(dòng)機(jī)進(jìn)行更大程度的優(yōu)化。本文研究了基于K-模擬的B(u)chi 自動(dòng)機(jī)優(yōu)化算法。
　　 線性時(shí)序邏輯可以更自然的轉(zhuǎn)化為廣義B(u)chi 自動(dòng)機(jī)，廣義B(u)chi 自動(dòng)機(jī)的接受狀態(tài)為l個(gè)集合，而其狀態(tài)數(shù)為等價(jià)B(u)chi 自動(dòng)機(jī)的1=l。因此直接對(duì)廣義B(u)chi 自動(dòng)機(jī)進(jìn)行優(yōu)化是十分重要的工作，本文研究了基于直接模擬，延遲模擬，

4、公平模擬的廣義B(u)chi 自動(dòng)機(jī)優(yōu)化算法。
　　 基于左右語(yǔ)言的優(yōu)化是完全基于自動(dòng)機(jī)理論的優(yōu)化方法，所謂左語(yǔ)言是指從初始狀態(tài)到指定狀態(tài)的語(yǔ)言，而右語(yǔ)言是指從指定狀態(tài)到接受狀態(tài)的語(yǔ)言。K-模擬為左右語(yǔ)言的計(jì)算提供了一個(gè)高效的算法，本文研究了基于K-模擬的左右語(yǔ)言的Kripke 結(jié)構(gòu)，B(u)chi 自動(dòng)機(jī)以及廣義B(u)chi 自動(dòng)機(jī)的優(yōu)化方法。
　　 應(yīng)對(duì)模型檢測(cè)中“狀態(tài)爆炸”問(wèn)題的一個(gè)自然的方法是對(duì)系統(tǒng)進(jìn)行分解，通

5、過(guò)驗(yàn)證各子系統(tǒng)上的性質(zhì)，然后根據(jù)這些性質(zhì)推導(dǎo)出系統(tǒng)的性質(zhì)。在驗(yàn)證各子系統(tǒng)的性質(zhì)時(shí)一般需要考慮其環(huán)境的影響，Pnueli 提出的假設(shè)/確保方法就是組合驗(yàn)證的一個(gè)成功的方法。但是該方法實(shí)現(xiàn)的瓶頸是存在模擬的計(jì)算，為此，本文研究了應(yīng)用廣義B(u)chi 自動(dòng)機(jī)的公平模擬替代存在模擬的組合驗(yàn)證以消除這一實(shí)現(xiàn)瓶頸。
　　 盡管模型檢測(cè)取得了很大的進(jìn)步，但是對(duì)于大系統(tǒng)的驗(yàn)證能力依然有限。在眾多的狀態(tài)減少和壓縮技術(shù)中，抽象技術(shù)是最有效的方法之