進(jìn)程重寫(xiě)系統(tǒng)的有限性問(wèn)題研究.pdf

1、近年來(lái),無(wú)限狀態(tài)系統(tǒng)的驗(yàn)證成為了一個(gè)十分熱門(mén)的研究領(lǐng)域。其中研究的重要問(wèn)題不僅僅有對(duì)系統(tǒng)間等價(jià)的判定,還包括對(duì)系統(tǒng)和特定有限系統(tǒng)的等價(jià)性和系統(tǒng)的有限性判定。有限性問(wèn)題所研究的是,給定一個(gè)系統(tǒng),是否存在一個(gè)有限狀態(tài)系統(tǒng)與之關(guān)于某個(gè)給定的等價(jià)關(guān)系相等。
　　通常在研究系統(tǒng)間等價(jià)性判定的同時(shí)一起研究其對(duì)應(yīng)的有限性問(wèn)題是對(duì)我們大有裨益的。有限性問(wèn)題在模型檢測(cè)和程序分析的領(lǐng)域都扮演了非常重要的角色。在實(shí)際應(yīng)用中,如果存在一個(gè)可行的方法,能檢

2、測(cè)一個(gè)正則系統(tǒng)與一個(gè)有限系統(tǒng)的等價(jià)性,那么我們就可以這個(gè)過(guò)程來(lái)檢測(cè)一個(gè)系統(tǒng)與有限系統(tǒng)的等價(jià)性,假設(shè)我們可以檢測(cè)系統(tǒng)的有限性,即正則性。
　　該問(wèn)題十分依賴于我們選擇研究的等價(jià)關(guān)系。我們通常會(huì)使用互模擬等價(jià)的概念,它是一種語(yǔ)義上的觀測(cè)等價(jià)。它和語(yǔ)言等價(jià)相比更有區(qū)分性,同時(shí)為我們提供了強(qiáng)大的計(jì)算可行性和一個(gè)優(yōu)美的博弈論描述。對(duì)于強(qiáng)互模擬關(guān)系,我們通過(guò)研究得到了大量關(guān)于它的可判定性和計(jì)算復(fù)雜性結(jié)論。然而,類似于弱互模擬和分支互模擬關(guān)系的

3、互模擬關(guān)系,在定義中考慮了系統(tǒng)內(nèi)部的不可見(jiàn)動(dòng)作。不可見(jiàn)動(dòng)作的引入,既為等價(jià)關(guān)系提供了更精確的描述,也為它的判定帶來(lái)了更大的難度。
　　驗(yàn)證問(wèn)題的研究,大多數(shù)都是在進(jìn)程重寫(xiě)系統(tǒng)中的范圍內(nèi)進(jìn)行的。這是一個(gè)包含了很多無(wú)限狀態(tài)系統(tǒng)的一般的模型。比如基本進(jìn)程代數(shù)(BPA),基本并發(fā)進(jìn)程(BPP),下推自動(dòng)機(jī)(PDA),Petri網(wǎng)(P N)和進(jìn)程代數(shù)(PA)。
　　在本文中,我們對(duì)現(xiàn)階段進(jìn)程重寫(xiě)系統(tǒng)中的有限性問(wèn)題的研究做了總結(jié)。我們羅

4、列了現(xiàn)有的結(jié)論,并分析了一些一般性的技術(shù)。更進(jìn)一步的,我們給出了一個(gè)關(guān)于Petri網(wǎng)關(guān)于分支互模擬的有限性的不可判定性的推論。
　　本文的主要貢獻(xiàn)是解決了完全正規(guī)化的進(jìn)程代數(shù)的關(guān)于弱互模擬和分支互模擬的有限性問(wèn)題。其中完全正規(guī)化是對(duì)于進(jìn)程系統(tǒng)輸入規(guī)則的一個(gè)限制。在文中,我們證明了完全正規(guī)化進(jìn)程代數(shù)無(wú)限性的一個(gè)等價(jià)條件。我們給出了判定這個(gè)條件的算法。它的時(shí)間復(fù)雜度為O(n3+mn),其中n是轉(zhuǎn)換規(guī)則的條數(shù),m是最長(zhǎng)規(guī)則的長(zhǎng)度。進(jìn)程代

5、數(shù)是一個(gè)一般的上下文無(wú)關(guān)模型,所以這個(gè)算法對(duì)完全正規(guī)化的基本進(jìn)程代數(shù)和基本并發(fā)進(jìn)程都是適用的。
　　另外,本文中還討論了正規(guī)化的基本并發(fā)進(jìn)程關(guān)于分支互模擬的有限性,以及完全正規(guī)化的Petri網(wǎng)關(guān)于弱互模擬和分支互模擬的有限性問(wèn)題。本文中討論了一些有用的引理和證明思路。
　　最后,本文還涉及了進(jìn)程重寫(xiě)系統(tǒng)有限性問(wèn)題的不可判定性和計(jì)算復(fù)雜性下界的證明。我們羅列了一些問(wèn)題和猜想,作為未來(lái)的工作。
　　總的來(lái)說(shuō),本文為一個(gè)具有