廖文琪, 柳欣欣

1(中國科學(xué)院 軟件研究所計算機科學(xué)國家重點實驗室, 北京 100190)2(中國科學(xué)院大學(xué), 北京 100190)

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

廖文琪1,2, 柳欣欣1

1(中國科學(xué)院 軟件研究所計算機科學(xué)國家重點實驗室, 北京 100190)2(中國科學(xué)院大學(xué), 北京 100190)

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

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

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

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

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

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

① 該概念不能用單個單調(diào)函數(shù)的不動點來表示;

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

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

1 基本概念和符號說明

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

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

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

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

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

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

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

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

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

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

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

① 一個C-coloured運行是指由顏色和動作交替組成的一個非空有限系列, 以一種顏色起始, 終止于一種顏色;

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

記（σ）為有限運行系列σ的C-coloured運行系列;

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

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

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

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

② 對t,t,∈S, 若則存在且時有時有

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

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

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

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

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

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

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

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

2.1 染色跡完全等價

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

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

① 若存在一個以s為起始的有窮運行系列σ, 則必然存在一個以t為起始的有窮運行ρ且有

② 若存在一個以s為起始的無窮運行系列σ, 則必然存在一個以t為起始的無窮運行ρ且有

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

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

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

定義 5.M=＜S,A, →＞是一個標(biāo)號遷移系統(tǒng)(LTS),C為M的一個著色. 函數(shù)(C)是定義在狀態(tài)集合S上的二元關(guān)系, 對當(dāng)且僅當(dāng)滿足下列兩個性質(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上的兩個等價關(guān)系≡1, ≡2且有≡1?≡2, 則有(≡1)?(≡2). 該單調(diào)性的證明從函數(shù)定義出發(fā)不難獲得.

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

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

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

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

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

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

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

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

綜上所得定理1得證.

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

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

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

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

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

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

≡1和≡2是定義在狀態(tài)集合S上的等價關(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. 如果二元等價關(guān)系≡是完全跡一致的著色, 則≡是發(fā)散性保持的.證明: ≡是一個完全跡一致的著色, 則可假設(shè)s≡t且有s?C; 根據(jù)發(fā)散的定義, 則存在一個以s為起始的無限運行系列σ且又≡是一個完全跡一致的著色, 故存在一個以t為起始的無限運行系列ρ且又因為s≡t, 所以進而得到即t?C; 所以≡是發(fā)散性保持的.

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

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

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

2.3 ≈cc和關(guān)系

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

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

證明:

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

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

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

證明:

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

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

3 結(jié)語

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

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

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

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

④ 研究了發(fā)散性保持的分支互模擬等價關(guān)系,為應(yīng)用該關(guā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;收到修改稿時間:2016-04-05

10.15888/j.cnki.csa.005431