進程重寫系統(tǒng)的有限性問題研究.pdf

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

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

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

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

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