關(guān)于并發(fā)系統(tǒng)分支互模擬關(guān)系發(fā)散性保持的研究①

廖文琪, 柳欣欣

1(中國科學(xué)院 軟件研究所計(jì)算機(jī)科學(xué)國家重點(diǎn)實(shí)驗(yàn)室, 北京 100190)2(中國科學(xué)院大學(xué), 北京 100190)

關(guān)于并發(fā)系統(tǒng)分支互模擬關(guān)系發(fā)散性保持的研究①

廖文琪1,2, 柳欣欣1

1(中國科學(xué)院 軟件研究所計(jì)算機(jī)科學(xué)國家重點(diǎn)實(shí)驗(yàn)室, 北京 100190)2(中國科學(xué)院大學(xué), 北京 100190)

帶發(fā)散性說明的分支互模擬是van Glabbeek和Weijland提出的一個(gè)概念, 并被用來定義等價(jià)關(guān)系≈bΔ. 該等價(jià)關(guān)系應(yīng)該是最弱的一個(gè)發(fā)散性保持的并且滿足分支互模擬性質(zhì)的等價(jià)關(guān)系. 然而在概念提出時(shí)并沒有提供這些重要性質(zhì)的證明, 并且我們認(rèn)為在原定義的基礎(chǔ)上這個(gè)證明是不顯然的. 本文通過co-induction的手段利用染色跡的概念定義了著色完全跡等價(jià), 并證明該等價(jià)關(guān)系是最弱的一個(gè)保持發(fā)散的并且滿足分支互模擬性質(zhì)的等價(jià)關(guān)系. 然后我們證明了著色完全跡等價(jià)關(guān)系和是相同的, 因而補(bǔ)充了van Glabbeek和Weijland的工作, 即證明了≈bΔ是最弱的一個(gè)保持發(fā)散的并且是滿足分支互模擬性質(zhì)的等價(jià)關(guān)系.

分支互模擬等價(jià)關(guān)系; 發(fā)散性; 發(fā)散性保持; co-induction定義; 染色跡

軟件系統(tǒng)對(duì)社會(huì)的各個(gè)方面起著重要的作用. 很多軟件有著非常復(fù)雜的結(jié)構(gòu). 因而軟件的生產(chǎn)需要理論上的支持以構(gòu)建可靠的軟件系統(tǒng)[1]. 通過建立給定程序以及程序的計(jì)算環(huán)境所組成的軟件系統(tǒng)抽象模型和程序的性質(zhì)規(guī)約之間的某種等價(jià)關(guān)系比如互模擬是驗(yàn)證程序正確性的有效方法[2,3].

并發(fā)理論的基本問題是兩個(gè)并發(fā)系統(tǒng)在什么時(shí)候可以看作是相等. 在提出通信系統(tǒng)演算(CCS)[4]的時(shí)候, Robin Milner就提出了所謂的觀察等價(jià), 之后Park在對(duì)標(biāo)號(hào)遷移系統(tǒng)的研究中采用co-induction的方式定義了互模擬等價(jià)關(guān)系[5], Park不但給出了互模擬關(guān)系的嚴(yán)格定義, 而且為證明互模擬等價(jià)關(guān)系提供了重要的方法.

在并發(fā)系統(tǒng)中, 發(fā)散性是一個(gè)重要的性質(zhì), 它通常涉及的是一個(gè)進(jìn)程有無窮多個(gè)內(nèi)部動(dòng)作, 不能同外界環(huán)境交互. 對(duì)于一個(gè)等價(jià)關(guān)系≡, 如果P和Q具有P≡Q時(shí),P是發(fā)散的當(dāng)且僅當(dāng)Q也是發(fā)散的, 則稱≡是發(fā)散性保持的[6]. 發(fā)散性是對(duì)進(jìn)程內(nèi)部性質(zhì)的約束,涉及到程序的終止性和進(jìn)程的前進(jìn)屬性, 因此利用等價(jià)關(guān)系驗(yàn)證程序正確性時(shí), 等價(jià)關(guān)系的發(fā)散性保持是非常重要的性質(zhì).

互模擬等價(jià)關(guān)系是一種觀察理論, 側(cè)重于系統(tǒng)與外部環(huán)境的交互, 著重研究的是可見的外部性質(zhì), 而對(duì)內(nèi)部動(dòng)作進(jìn)行抽象處理. 經(jīng)過內(nèi)部動(dòng)作抽象出來的互模擬等價(jià)關(guān)系常常不保持發(fā)散性, 需要添加額外的約束. 分支互模擬(branching bisimulation)[7]是由van Glabbeek和Weijlang提出的一種進(jìn)程等價(jià)關(guān)系. 研究發(fā)現(xiàn)分支互模擬關(guān)系不是發(fā)散性保持的. 因此van Glabbeek和Weijland對(duì)分支互模擬作了額外約束, 提出了帶發(fā)散性說明的分支互模擬關(guān)系(branching bisimulation with explicit divergence)[7]. 然而, 利用該概念在證明相關(guān)性質(zhì)時(shí)不夠直接, 等價(jià)關(guān)系傳遞性上的證明太過復(fù)雜[8]. 主要原因是:

① 該概念不能用單個(gè)單調(diào)函數(shù)的不動(dòng)點(diǎn)來表示;

② 需要對(duì)無限運(yùn)行序列的相關(guān)狀態(tài)的發(fā)散性進(jìn)行分類討論, 然后歸納證明.

為了解決上述問題, 我們首先使用co-induction思想同時(shí)借用染色跡概念定義了著色完全跡等價(jià)關(guān)系(coloured complete trace equivalence), 該等價(jià)關(guān)系能通過一個(gè)單調(diào)函數(shù)的不動(dòng)點(diǎn)刻畫, 之后利用刻畫函數(shù)的最大不動(dòng)點(diǎn)理論在概念的定義上證明其等價(jià)關(guān)系和發(fā)散性保持性質(zhì), 最后我們說明著色完成跡等價(jià)和帶發(fā)散性說明的分支互模擬關(guān)系是相同的. 從新概念出發(fā),利用不動(dòng)點(diǎn)理論大大降低了證明的復(fù)雜程度.

1 基本概念和符號(hào)說明

文章中主要涉及到如下幾個(gè)概念: 標(biāo)號(hào)遷移系統(tǒng)(labeled transition systems), 著色(colouring), 帶發(fā)散性說明的分支互模擬關(guān)系(branching bisimulation with explicit divergence). 本文中在證明中對(duì)分支互模擬概念沒有細(xì)節(jié)上的涉及而是通過不同進(jìn)程和系統(tǒng)狀態(tài)有同一顏色來體現(xiàn)其等價(jià)關(guān)系, 因此在這里就不給出定義, 后文中作者提出的定義也在后續(xù)的證明中給出.我們所有的研究都是在標(biāo)號(hào)遷移系統(tǒng)上進(jìn)行的, 首先給出標(biāo)號(hào)遷移系統(tǒng)[1]的定義和一些符號(hào)說明.

定義 1. 標(biāo)號(hào)遷移系統(tǒng)(labeled transition systems):一個(gè)標(biāo)號(hào)遷移系統(tǒng)是一個(gè)三元組M=＜S,A, →＞, 其中

①S為狀態(tài)集合;

②A為標(biāo)號(hào)集合;

③ →?S×（A∪τ）×S是一個(gè)有標(biāo)號(hào)的遷移關(guān)系. 其中τ是內(nèi)部動(dòng)作, 通常假設(shè)其不在集合A中, →中的一個(gè)元素（s,α,t）表示一次遷移, 記為

④M的一個(gè)有限運(yùn)行系列是指由狀態(tài)和動(dòng)作交替組成的非空有限遷移系列, 記為ρ=s0α0s1α1Λsn-1αn-1sn, 其中first(ρ)=s0, last(ρ)=sn, length(ρ) =n;

⑤M的一個(gè)無限運(yùn)行系列是指由狀態(tài)和動(dòng)作交替組成的非空無限遷移系列, 記為ρ=s0α0s1α1Λ其中first(ρ)=s0.

一般情況下, 我們可以通過連接已有的運(yùn)行系列,狀態(tài)和動(dòng)作形成新的運(yùn)行系列.

存在多步τ遷移時(shí), 可以通過一些標(biāo)準(zhǔn)符號(hào)進(jìn)行簡略表示:s?s,表示存在一個(gè)以s,s,分別作為起始狀態(tài)和結(jié)束狀態(tài)的有窮運(yùn)行系列, 其中所有的動(dòng)作均為τ.

結(jié)束了對(duì)標(biāo)號(hào)遷移系統(tǒng)的定義和相關(guān)符號(hào)的說明之后, 接下來給出van Glabbeek在刻畫發(fā)散性保持性質(zhì)中使用到的染色跡概念[8], 從定義著色(Colouring)開始.

定義 2. 著色(Colouring):M=＜S,A, →＞是一個(gè)標(biāo)號(hào)遷移系統(tǒng)(LTS),M的著色是一個(gè)在狀態(tài)集合S上的等價(jià)關(guān)系; 給定一個(gè)著色C和一個(gè)狀態(tài)s∈S,s的一個(gè)顏色C（s）是一個(gè)包含s的等價(jià)類. 其中

① 一個(gè)C-coloured運(yùn)行是指由顏色和動(dòng)作交替組成的一個(gè)非空有限系列, 以一種顏色起始, 終止于一種顏色;

② 一個(gè)著色C導(dǎo)出一個(gè)從M的有限運(yùn)行系列集合到C-coloured運(yùn)行系列集合的映射, 記為, 在運(yùn)行系列長度上的歸納定義如下:

記（σ）為有限運(yùn)行系列σ的C-coloured運(yùn)行系列;

③ρ是標(biāo)號(hào)遷移系統(tǒng)M的一個(gè)無限運(yùn)行系列,（ρ）為ρ的所有有限運(yùn)行前綴的C-coloured運(yùn)行系列組成的集合, 記為的一個(gè)有限運(yùn)行前綴};

④ 對(duì)s∈S, 稱s關(guān)于著色C發(fā)散, 若存在一個(gè)以s為起始狀態(tài)的無限運(yùn)行系列記為s?C; 我們稱ρ是一個(gè)發(fā)散運(yùn)行系列, 當(dāng)ρ中所有的動(dòng)作均為τ且ρ所有的狀態(tài)均為顏色C（s）時(shí).

引理 1.M=＜S,A, →＞是一個(gè)標(biāo)號(hào)遷移系統(tǒng)(LTS),C為M的一個(gè)著色,ρ是一個(gè)有窮運(yùn)行.

① 對(duì)s∈S, 若（ρ）=C（s）, 則ρ中的所有動(dòng)作均為τ且ρ所有狀態(tài)的顏色為C（s）;

② 對(duì)t,t,∈S, 若則存在且時(shí)有時(shí)有

證明: 使用歸納法證明, 在ρ長度上進(jìn)行歸納證明可完成①的證明. 在證明①為真的基礎(chǔ)上,ρ長度上進(jìn)行歸納證明可得到②.

在完成對(duì)基本概念的準(zhǔn)備和記號(hào)的說明后, 我們給出van Glabbeek提出的帶發(fā)散性說明的分支互模擬關(guān)系[7].

定義 3. 帶發(fā)散性說明的分支互模擬關(guān)系(branching bisimultiaon with explicit divergence):M=＜S,A, →＞是一個(gè)標(biāo)號(hào)遷移系統(tǒng)(LTS),C為M的一個(gè)著色.

① 著色C是一致的(consistent), 如果對(duì)任意C（s）=C（t）, 其中s,t∈S, 若存在一個(gè)以s為起始的有窮運(yùn)行系列σ, 則必然存在一個(gè)以t為起始的有窮運(yùn)行ρ且有

② 著色C是發(fā)散性保持的(divergence preserving), 如果對(duì)任意C（s）=C（t）, 其中s,t∈S, 若s?C, 則t?C.

對(duì)s,t∈S, 如果存在一個(gè)一致的且是發(fā)散性保持的著色C, 使得C（s）=C（t）, 則稱s和t是帶發(fā)散性說明的分支互模擬等價(jià)關(guān)系, 記為

我們希望定義4給出的關(guān)系是一個(gè)等價(jià)關(guān)系, 并且具有分支互模擬性質(zhì), 并且是保持發(fā)散性, 并且是具備所有以上性質(zhì)的最弱的那個(gè)等價(jià)關(guān)系. 但在概念提出時(shí)[7]并沒有提供這些事實(shí)的證明, 后續(xù)的研究[8]也只有部分證明(證明了它是一種等價(jià)關(guān)系). 在下面章節(jié)中, 我們將定義一個(gè)等價(jià)關(guān)系, 并且證明這個(gè)等價(jià)關(guān)系具有上述性質(zhì), 最后證明這個(gè)等價(jià)關(guān)系和定義4給出的是相同的.

2 概念的提出及性質(zhì)證明

2.1 染色跡完全等價(jià)

本節(jié)我們將定義一個(gè)新的等價(jià)關(guān)系, 該等價(jià)關(guān)系利用染色跡(colour trace)概念使用co-induction的方式完成對(duì)一致性和發(fā)散性保持的刻畫, 定義著色完全跡等價(jià)關(guān)系, 并證明這個(gè)關(guān)系是最弱的同時(shí)發(fā)散性保持和分支互模擬性質(zhì)的等價(jià)關(guān)系.

定義 4. 著色完全跡等價(jià)關(guān)系(coloured complete trace equivalence):M=＜S,A, →＞是一個(gè)標(biāo)號(hào)遷移系統(tǒng)(LTS),C為M的一個(gè)著色.C是完全跡一致的(complete trace consistent), 如果對(duì)任意C（s）=C（t）, 其中s,t∈S, 蘊(yùn)含著

① 若存在一個(gè)以s為起始的有窮運(yùn)行系列σ, 則必然存在一個(gè)以t為起始的有窮運(yùn)行ρ且有

② 若存在一個(gè)以s為起始的無窮運(yùn)行系列σ, 則必然存在一個(gè)以t為起始的無窮運(yùn)行ρ且有

對(duì)s,t∈S, 如存在一個(gè)完全跡一致的著色C, 使得C（s）=C（t）, 則稱s和t是著色完全跡等價(jià)關(guān)系, 記為s≈cct.

2.2 ≈cc的性質(zhì)說明

為幫助完成對(duì)≈cc性質(zhì)的研究, 引入函數(shù), 其定義如下:

定義 5.M=＜S,A, →＞是一個(gè)標(biāo)號(hào)遷移系統(tǒng)(LTS),C為M的一個(gè)著色. 函數(shù)(C)是定義在狀態(tài)集合S上的二元關(guān)系, 對(duì)當(dāng)且僅當(dāng)滿足下列兩個(gè)性質(zhì):

引理 2.

②C是完全跡一致的當(dāng)且僅當(dāng){（s,t）|s,t∈S,C（s）=C（t）}?（C）成立

證明: 引理中①和②的證明可以在定義4和定義5中直接推導(dǎo)獲得. ③的證明可以轉(zhuǎn)化為證明: 存在在狀態(tài)集合S上的兩個(gè)等價(jià)關(guān)系≡1, ≡2且有≡1?≡2, 則有(≡1)?(≡2). 該單調(diào)性的證明從函數(shù)定義出發(fā)不難獲得.

定理 1.M=＜S,A, →＞是一個(gè)標(biāo)號(hào)遷移系統(tǒng)(LTS),則≈cc是在狀態(tài)集合S上的等價(jià)關(guān)系, 同時(shí)≈cc是一個(gè)完全跡一致的著色并且是M中完全跡一致著色刻畫的等價(jià)關(guān)系中最粗粒度的那個(gè).

證明: 令｛≡i｝i∈I為在狀態(tài)集合S上的等價(jià)關(guān)系的集合, 根據(jù)集合知識(shí)我們可以得到下面幾個(gè)事實(shí):

① ∩｛≡i|i∈I｝是在集合S上的等價(jià)關(guān)系;

② 對(duì)所有i∈I, ∩｛≡i|i∈I｝?≡i均成立;

③ 如果≡是狀態(tài)集合S上的等價(jià)關(guān)系且對(duì)所有i∈I, 均有≡?≡i, 則≡?∩｛≡i|i∈I｝;

⑥ 如果≡是在狀態(tài)集合S上的等價(jià)關(guān)系并且對(duì)所有i∈I均有≡i?≡, 則有

令ε為狀態(tài)集合S上的等價(jià)關(guān)系的集合, 則由上述事實(shí)可知ε的任意子集在關(guān)系?中既有最大下確界也有最小上確界, 因此（ε,?）是一個(gè)完全格. 又由引理2可知函數(shù)是在該完全格中的單調(diào)函數(shù), 則根據(jù)Knaster-Tarski不動(dòng)點(diǎn)理論[9]可知函數(shù)有最大不動(dòng)點(diǎn)FIX（）∈ε, 該不動(dòng)點(diǎn)有如下性質(zhì):

② 對(duì)任意≡∈ε, 當(dāng)≡?(≡)時(shí), 有

綜上所得定理1得證.

定理1的證明應(yīng)用到了Knaster-Tarski不動(dòng)點(diǎn)理論,證明了≈cc是一個(gè)單調(diào)函數(shù)刻畫的最大不動(dòng)點(diǎn). 這使得定理1的證明清晰而且規(guī)整. 相比較而言,因?yàn)椴荒苡蓡蝹€(gè)單調(diào)函數(shù)的最大不動(dòng)點(diǎn)進(jìn)行刻畫獲得, 使得等價(jià)關(guān)系的證明不明顯, 性質(zhì)的說明也不充分. 接下來通過一個(gè)例子來對(duì)刻畫的函數(shù)的單調(diào)性加以說明.

同樣, 我們需引入一個(gè)在ε上的函數(shù)?, 定義如下:

≡是狀態(tài)集合S上的一個(gè)二元等價(jià)關(guān)系, （s,t）∈?(≡)當(dāng)且僅當(dāng)對(duì)（s,t）∈S×S, 滿足下面兩個(gè)條件:

②s?C當(dāng)且僅當(dāng)t?C.

文獻(xiàn)[8]對(duì)≈bΔ的性質(zhì)進(jìn)行了說明, 并證明了其為一個(gè)等價(jià)性關(guān)系, 且具有發(fā)散性保持的性質(zhì), 這些結(jié)論不是通過對(duì)函數(shù)?應(yīng)用Knaster-Tarski定理得到的,因?yàn)楹瘮?shù)?不具有單調(diào)性, 下面我們給出一個(gè)反例(如圖1所示) .

圖1 函數(shù)?單調(diào)性反例

≡1和≡2是定義在狀態(tài)集合S上的等價(jià)關(guān)系且有≡1?≡2, 其中有p≡1q,p,≡1q,, 且p和p,,q和q,不具有關(guān)系≡1;p,q,p,,q,之間均有關(guān)系≡2; 根據(jù)定義可知p和q在≡1中均不發(fā)散, 有（p,q）∈?(≡1);但p在≡2中不發(fā)散,q在≡2中發(fā)散, 有（p,q）??(≡2), 故?不具有單調(diào)性.

定理 2. 如果二元等價(jià)關(guān)系≡是完全跡一致的著色, 則≡是發(fā)散性保持的.證明: ≡是一個(gè)完全跡一致的著色, 則可假設(shè)s≡t且有s?C; 根據(jù)發(fā)散的定義, 則存在一個(gè)以s為起始的無限運(yùn)行系列σ且又≡是一個(gè)完全跡一致的著色, 故存在一個(gè)以t為起始的無限運(yùn)行系列ρ且又因?yàn)閟≡t, 所以進(jìn)而得到即t?C; 所以≡是發(fā)散性保持的.

推論 1. ≈cc是發(fā)散性保持的.

證明: 由定理1可知≈cc是一個(gè)完全跡一致的著色, 結(jié)合定理2可知≈cc是發(fā)散性保持的.

至此, 我們對(duì)≈cc的性質(zhì)進(jìn)行了全面的說明, 證明了≈cc是一個(gè)等價(jià)關(guān)系, 當(dāng)著色時(shí)使用的是分支互模擬關(guān)系時(shí), ≈cc是分支互模擬等價(jià)關(guān)系, 具有發(fā)散性保持的特性, 同時(shí)也是具備所有以上性質(zhì)的最弱的那個(gè)等價(jià)關(guān)系.

2.3 ≈cc和關(guān)系

由上節(jié)對(duì)≈cc性質(zhì)的描述我們知道, ≈cc是最粗粒度的具有發(fā)散性保持的分支互模擬等價(jià)關(guān)系.同樣是最弱的帶發(fā)散性保持的分支互模擬等價(jià)關(guān)系[7-8]. 那么和≈cc之間的有什么關(guān)系, 本節(jié)將對(duì)其進(jìn)行完整的闡述.

定理 3.M=＜S,A, →＞是一個(gè)標(biāo)號(hào)遷移系統(tǒng)(LTS),≡是在狀態(tài)集合S上的二元等價(jià)關(guān)系, 則≡?(≡)當(dāng)且僅當(dāng)≡是一致的且是發(fā)散性保持的.

證明:

上述定理告訴我們定義3和定義4中獲得的兩個(gè)關(guān)系的條件是相同的, 得到的等價(jià)應(yīng)該也是相同的,即將在定理4中給出完善的證明. 這不禁讓人疑問: 兩個(gè)定義給定的條件是可以互推得到的, 關(guān)系也是相同的, 為什么刻畫該關(guān)系的函數(shù)會(huì)在單調(diào)性上有不同的表現(xiàn). 比較兩個(gè)定義的條件發(fā)現(xiàn), 兩種定義都分為兩個(gè)部分, 第一部分是對(duì)有限運(yùn)行系列的一致性的要求, 兩種定義此部分完全相同, 區(qū)別在第二部分對(duì)無限系列的發(fā)散性保持上的約束. 定義3只對(duì)無限系列相關(guān)狀態(tài)的發(fā)散性保持做了要求, 對(duì)其有限子系列的一致性并沒有說明, 而定義4對(duì)無窮運(yùn)行系列中的相關(guān)狀態(tài)的發(fā)散性和一致性都給出了明確的說明. 從這個(gè)角度上看定義4的條件比定義3更強(qiáng), 這個(gè)說法沒有問題, 但事實(shí)是對(duì)發(fā)散性保持的說明本身其實(shí)蘊(yùn)含著從相關(guān)狀態(tài)起始的無限系列的有限子系列具有一致性, 但需要進(jìn)一步的說明. 定義4不能使用單個(gè)單調(diào)函數(shù)進(jìn)行刻畫獲得最大不動(dòng)點(diǎn)性質(zhì), 但使用兩個(gè)函數(shù)可以完成對(duì)其該性質(zhì)的闡述.

定理 4.M=＜S,A, →＞是一個(gè)標(biāo)號(hào)遷移系統(tǒng)(LTS).則

② ≈bΔ是在狀態(tài)集合S上的二元等價(jià)關(guān)系, 同時(shí)具有一致性和發(fā)散性保持特性, 并且是標(biāo)號(hào)遷移系統(tǒng)M中最弱的帶發(fā)散性保持的等價(jià)關(guān)系.

證明:

① 由定理2可知≈cc是發(fā)散性保持的, 并且是一致的, 根據(jù)定義3, 有任意s,t∈S, 如果則存在一個(gè)等價(jià)關(guān)系≡, ≡是一致的并且是發(fā)散性保持的且有s≡t, 由定理3可知≡?(≡), 運(yùn)用引理2可知≡是完全跡一致的, 故s≈cct, 即綜上

② 由定理1可知≈cc是在狀態(tài)集合S上的等價(jià)關(guān)系, 由于所以也是在狀態(tài)集合S上的等價(jià)關(guān)系, 同時(shí)在定理8中我們對(duì)≈cc的最弱等價(jià)性進(jìn)行了證明, 同樣也可以遷移到上.

3 結(jié)語

分支互模擬關(guān)系發(fā)散性保持的研究對(duì)并發(fā)系統(tǒng)理論發(fā)展和并發(fā)程序的驗(yàn)證具有重要的意義. 盡管van Glabbeek等提出了帶發(fā)散性說明的分支互模擬概念并對(duì)其性質(zhì)進(jìn)行了一定的說明, 但我們提出了著色完全跡等價(jià)關(guān)系對(duì)分支互模擬關(guān)系的發(fā)散性保持問題進(jìn)行了研究, 從另一個(gè)角度證明了帶發(fā)散性說明的分支互模擬概念的性質(zhì), 完善了其工作. 本文的研究有以下貢獻(xiàn)和創(chuàng)新性:

① 使用co-induction方式定義了著色完全跡等價(jià)關(guān)系, 并證明了其為最弱的發(fā)散性保持的分支互模擬等價(jià)關(guān)系.

② 對(duì)刻畫帶發(fā)散性說明的分支互模擬關(guān)系的函數(shù)的單調(diào)性進(jìn)行了說明.

③ 建立了著色完全跡等價(jià)關(guān)系和帶發(fā)散性說明的分支互模擬等價(jià)關(guān)系之間的聯(lián)系, 完善帶發(fā)散性說明的分支互模擬關(guān)系的研究工作.

④ 研究了發(fā)散性保持的分支互模擬等價(jià)關(guān)系,為應(yīng)用該關(guān)系驗(yàn)證程序的正確性提供幫助.

1 張文輝.軟件系統(tǒng)行為與程序正確性.http://lcs.ios.ac. cn/～zwh/pv/pv13.pdf.

2 Liang H, Feng X, Fu M. A rely-guarantee-based simulation for verifying concurrent program transformations. ACM SIGPLAN Notices, ACM, 2012, 47(1): 455–468.

3 Liang H, Hoffmann J, Feng X, et al. Characterizing progress properties of concurrent objects via contextual refinements . CONCUR 2013–Concurrency Theory. Springer Berlin Heidelberg, 2013: 227–241.

4 Milner R. Communication and Concurrency. Prentice-Hall, Inc., 1989.

5 Park D. Concurrency and automata on infinite sequences. Gi-Conference on Theoretical Computer Science. Springer-Verlag. 1981. 167–183.

6 何超棟.CCS的基本問題研究[博士學(xué)位論文].上海:上海交通大學(xué),2011.

7 Van Glabbeek R, Weijland W. Branching time and abstraction in bisimulation semantics. Journal of the ACM, 1996.

8 Van Glabbeek R, Luttik B, Trcka N. Branching bisimilarity with explicit divergence. Fundamenta Informaticae, 2009, 93(4): 371–392.

9 Paulson LC. A Fixedpoint Approach to Implementing (co) Inductive Definitions. Springer Berlin Heidelberg, 1994.

Branching Bisimulation with Explicit Divergence in Concurrent Systems

LIAO Wen-Qi1,2, LIU Xin-Xin112
(State Key Laboratory of Computer Science Institute of Software, Chinese Academy of Sciences, Beijing 100190, China) (University of Chinese Academy of Sciences, Beijing 100190, China)

The notion of branching bisimulation with explicit divergence was introduced by van Glabbeek and Weijland. It is used to define an equivalence relation, which means to be the weakest equivalence with the property of branching bisimulation and divergence preservation. However, in that paper it only claims that ≈bΔis an equivalence with such properties without proofs, and as it turns out that the proving is not obvious. In this paper we introduce an equivalence relation called coloured complete trace equivalence, and prove that it is the weakest equivalence which has the property of branching bisimulation equivalence and is also divergence preserving. We then prove that the coloured complete trace equivalence coincides with, thus supplementing the work of van Glabbeek and Weijland.

branching bisimulation; divergence; divergence preserving; co-induction; colour trace

國家自然科學(xué)基金(NSFC-91418204)

2016-03-21;收到修改稿時(shí)間:2016-04-05

10.15888/j.cnki.csa.005431