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

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

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

【學位級別】：博士

【部分圖文】：

PRS層次


本文編號：3480818