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

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

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

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

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

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

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