基本進(jìn)程代數(shù)是進(jìn)程重寫系統(tǒng)中基礎(chǔ)的順序進(jìn)程。相比有限狀態(tài)系統(tǒng),它引入了無限狀態(tài);相比于基本并行進(jìn)程,它是順序執(zhí)行,控制能力較強(qiáng);相比于下推自動機(jī),它可以被理解為一種簡單的單狀態(tài)下推自動機(jī)。即使基本進(jìn)程代數(shù)的定義和計(jì)算結(jié)構(gòu)十分簡潔,該模型也有著一定的表達(dá)能力和廣泛的應(yīng)用。從語法的角度看,該系統(tǒng)定義的語法對應(yīng)的語言和下推自動機(jī)能接受的語言一致。從計(jì)算模型的角度看,該系統(tǒng)也能模擬很多比有限狀態(tài)機(jī)復(fù)雜的順序計(jì)算。因此對該模型的代數(shù)結(jié)構(gòu)的探索對于基本計(jì)算模型的研究有重要的意義。另一方面,自動化驗(yàn)證的核心問題之一是無限狀態(tài)系統(tǒng)的等價(jià)性驗(yàn)證問題,其他還包括了模型檢測和定理機(jī)器證明。其中,等價(jià)性驗(yàn)證可以用以判定程序?qū)崿F(xiàn)和給定的某設(shè)計(jì)規(guī)范的一致性。等價(jià)關(guān)系則根據(jù)不同的一致性要求來確定其嚴(yán)格程度。Park提出的互模擬,Milner提出的著名的觀測等價(jià)關(guān)系就是這樣一類等價(jià)關(guān)系。1987年,Baeten,Bergstra和Klop證明了一個著名的結(jié)論:強(qiáng)互模擬在基本進(jìn)程代數(shù)上是可判定的。這個結(jié)論與之前的語言等價(jià)的不可判定性,激勵了很多研究者往這個方向繼續(xù)深入研究。van Glabbeek提出的分支互模擬在一定... 

【文章來源】：上海交通大學(xué)上海市 211工程院校 985工程院校 教育部直屬院校

【文章頁數(shù)】：121 頁

【學(xué)位級別】：博士

【部分圖文】：

PRS層次


本文編號：3480818