無限狀態(tài)系統(tǒng)上分支互模擬等價驗證.pdf

1、等價驗證是自動驗證領(lǐng)域的主流方法之一，另一個主流方法是模型檢測。等價驗證研究的重點是互模擬等價驗證?；ツM等價驗證起始于上世紀(jì)80年代。互模擬等價驗證研究關(guān)注的模型大都是無限狀態(tài)系統(tǒng)，大部分無限狀態(tài)系統(tǒng)都可以在一個一般的框架—進(jìn)程重寫系統(tǒng)(Process Rewrite System,PRS)中定義。從上世紀(jì)80年代開始，有大量進(jìn)程重寫系統(tǒng)上互模擬等價驗證的工作。這些工作表明在進(jìn)程重寫系統(tǒng)上進(jìn)行弱互模擬等價驗證是非常困難的，主要體現(xiàn)在兩

2、個方面：其一,在絕大部分無限狀態(tài)系統(tǒng)上，如進(jìn)程重寫系統(tǒng)中BPA或BPP之上的模型，弱互模擬等價驗證是不可判定的；其二,在非?；镜臒o限狀態(tài)系統(tǒng)—BPA和BPP上，弱互模擬等價驗證的判定性至今仍然是公開的。與此同時，弱互模擬等價的一個加細(xì)版本—分支互模擬等價最近被證明在賦范BPA和賦范BPP上都是可判定的。分支互模擬等價與弱互模擬等價的區(qū)別是前者區(qū)分了改變狀態(tài)的內(nèi)部動作和不改變狀態(tài)的內(nèi)部動作，并且要求只有不改變狀態(tài)的內(nèi)部動作才可以忽略。從

3、自動驗證角度看，分支互模擬等價是比弱互模擬等價更恰當(dāng)?shù)牡葍r關(guān)系。本文的研究聚焦在進(jìn)程重寫系統(tǒng)上分支互模擬等價驗證問題上，關(guān)注的是這類問題的可判定性，算法及復(fù)雜性，主要貢獻(xiàn)有以下幾個方面。
　　BPA和BPP等價驗證下界。通過構(gòu)造從EXPTIME-完備問題Hit-or-Run博弈到賦范BPA上的分支互模擬博弈的一個歸約，本文證明了賦范BPA上的分支互模擬等價驗證有EXPTIME-難下界。這與目前賦范BPA分支互模擬等價驗證最好的上界

4、是匹配的，同時也與弱互模擬等價驗證目前最好的下界一致。另外，通過構(gòu)造量詞化可滿足性問題到賦范BPP上的分支互模擬博弈的一個歸約，本文證明了賦范BPP上的分支互模擬等價驗證是PSPACE-難的。這與BPP上弱互模擬等價驗證的目前最好的下界一致。此外，本文同時證明了這兩個下界對介于分支互模擬與弱互模擬之間的所有等價關(guān)系在對應(yīng)的模型上也是成立的。
　　賦范BPA分支互模擬正則性復(fù)雜性。本文證明了賦范BPA上分支互模擬正則性的復(fù)雜性介于P

5、SPACE和EXPTIME之間。為了證明上界，我們利用賦范BPA上的分支互模擬等價判定的指數(shù)時間算法，設(shè)計了一個指數(shù)時間算法判定一個給定的賦范BPA進(jìn)程是否是分支互模擬正則；為了證明下界，我們構(gòu)造了一個從量詞化可滿足性問題的歸約。本文同時證明了，PSPACE-難下界對于弱互模擬正則性也成立。
　　進(jìn)程重寫系統(tǒng)上分支互模擬等價驗證的不可判定性。通過構(gòu)造一個從Post字對應(yīng)問題到賦范進(jìn)程代數(shù)上分支互模擬博弈的歸約，本文證明了分支互模擬

6、驗證在賦范進(jìn)程代數(shù)上是不可判定的。另外，本文將Mayr關(guān)于單計數(shù)器網(wǎng)上的弱互模擬等價不可判定的結(jié)論推廣到了分支互模擬等價驗證上。此外，本文說明了這兩個歸約對介于分支互模擬等價與弱互模擬等價之間所有等價關(guān)系都是成立的。根據(jù)進(jìn)程重寫系統(tǒng)的表達(dá)能力分層，分支互模擬等價驗證在進(jìn)程重寫系統(tǒng)分層中存在一條明顯的可判定界線。
　　下推系統(tǒng)上分支互模擬等價驗證的高階不可判定性。本文證明了在下推系統(tǒng)上分支互模擬等價驗證是高階不可判定的。更具體的講，