李蘇婷，張 嚴(yán)

(1.南京航空航天大學(xué) 計算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇 南京 211106；2.南京林業(yè)大學(xué) 信息科學(xué)技術(shù)學(xué)院，江蘇 南京 210037)

0 引 言

進(jìn)程代數(shù)[1-3]是反應(yīng)式系統(tǒng)的原型規(guī)范語言，它們通過進(jìn)程項來描述反應(yīng)式系統(tǒng)的規(guī)范及實現(xiàn)，實現(xiàn)是否滿足規(guī)范則由行為等價或者模擬關(guān)系來刻畫。經(jīng)典模擬關(guān)系[4]主要針對具有被動行為的反應(yīng)式系統(tǒng)間精化關(guān)系的刻畫，它要求規(guī)范的被動行為必須被實現(xiàn)模擬。然而，對于具有主動行為的系統(tǒng)(如輸入/輸出自動機(jī)[5-6]中的輸出行為)，為了保證實現(xiàn)的安全性，它的輸出行為必須是規(guī)范所允許的。因此，F(xiàn)ábregas等[7]將動作劃分為共變、異變和互變?nèi)N類型，對經(jīng)典(互)模擬概念進(jìn)行推廣[8-9]，提出了共變-異變模擬(covariant-contravariant simulation，CC-模擬)。直觀上講，共變動作表示系統(tǒng)的被動行為，其執(zhí)行受環(huán)境控制，規(guī)范中共變動作所標(biāo)記的轉(zhuǎn)換必須在實現(xiàn)中被模擬；異變行為代表了系統(tǒng)本身控制下的主動行為，實現(xiàn)中異變動作所標(biāo)記的轉(zhuǎn)換必須在規(guī)范中被允許；互變行為的要求反映了經(jīng)典的互模擬思想。文獻(xiàn)[10-12]詳述了CC-模擬提出的動機(jī)。

眾所周知，行為關(guān)系的(前)同余性質(zhì)在支持形式規(guī)范的模塊化構(gòu)建和公理系統(tǒng)的推理方面具有重要意義，它的證明需要根據(jù)進(jìn)程代數(shù)語言中算子的結(jié)構(gòu)化操作語義(structural operational semantics，SOS)[13]規(guī)則逐個開展[1,10,14]。為了避免(前)同余性證明中的重復(fù)勞動，學(xué)術(shù)界提出了多種類型的SOS規(guī)則的框架形式，其中ntyft/ntyxt是最具代表性之一。Groote[15]首次給出它的定義，證明了互模擬關(guān)系在良基且可分層的轉(zhuǎn)換系統(tǒng)規(guī)范(transition system specification，TSS)[16]上的同余性。Fokkink[17]將ntyft/ntyxt形式約簡到Ntree形式，論證了上述同余性定理中良基條件的非必要性。Bol等[18]利用分層和歸約技術(shù)證明了非良基條件下ntyft/ntyxt規(guī)則形式的TSS關(guān)于互模擬的同余性。借鑒Bol等[18]的方法，文中探討了CC-模擬在ntyft/ntyxt規(guī)則形式的TSS上的前同余性。

1 預(yù)備知識

進(jìn)程代數(shù)一般通過一組SOS規(guī)則對進(jìn)程項的行為進(jìn)行規(guī)范。通過這些規(guī)則，進(jìn)程的行為被描述成一個帶標(biāo)記的轉(zhuǎn)換系統(tǒng)[19]，轉(zhuǎn)換系統(tǒng)通常用TSS來描述。本節(jié)將介紹一些預(yù)備概念。

1.1 TSS及轉(zhuǎn)換模型

令V是可數(shù)無限的變元集，用x,y,z等表示其中元素。令Σ為型(signature)，包含了常元0、算子以及算子對應(yīng)的元數(shù)。令A(yù)ctτ=Act∪{τ}為動作符號集，用a,b,c等表示其中元素，其中τ是系統(tǒng)內(nèi)部動作，Act為外部動作集。基于Σ上的進(jìn)程項的BNF范式定義為：P=0|x|f(P1,P2,…,Pl)，其中x∈V且f∈Σ是l元算子。T(Σ)表示基于Σ上的所有進(jìn)程項的集合，T(Σ)表示所有閉項(不含變元的進(jìn)程項)的集合，用P,Q等表示進(jìn)程項。一個(閉)替換σ是V到T(Σ)(T(Σ))的函數(shù)，進(jìn)程項P上的替換(記作Pσ)按常規(guī)定義。

不難發(fā)現(xiàn)，正TSS的支持模型是唯一存在的且是其最小模型[18](最小模型按常規(guī)定義)。但非正的TSS(即其有些規(guī)則中含否前提)則不然[18]，分層和歸約技術(shù)的提出則解決了該問題。

1.2 分層技術(shù)

規(guī)則只能定義一個轉(zhuǎn)換公式是成立的，但不能定義一個轉(zhuǎn)換公式是不成立的。常用的分層技術(shù)確保了所有轉(zhuǎn)換公式的永真性不再依賴于否轉(zhuǎn)換公式，保證了轉(zhuǎn)換模型的唯一性[18]。在轉(zhuǎn)換模型具體性質(zhì)的證明中，時常依賴穩(wěn)定模型，定義如下：

定理1[18]：令S=(Σ,R)為一個TSS，轉(zhuǎn)換模型→?T(Σ)×Actτ×T(Σ)對S是穩(wěn)定的，則：

(1)→是S的模型；

(2)→是被S支持的；

(3)→是S最小模型。

定理1將隱式地幫助后續(xù)的證明，它反映了對穩(wěn)定模型的要求的本質(zhì)即是在尋找最小支持模型。

1.3 歸約技術(shù)

對于一些不可分層但卻具有重要意義的TSS(如帶權(quán)限的BPAσ∈τ)[18]，歸約技術(shù)則有用武之地。受良基模型[20]的啟發(fā)，歸約技術(shù)將一個TSS的轉(zhuǎn)換模型劃分成三部分：肯定為真的轉(zhuǎn)換模型→true、肯定不為真的轉(zhuǎn)換模型和不確定是否為真的轉(zhuǎn)換模型→pos。利用這些劃分好的信息進(jìn)行歸約得到一個新的TSS，對于一些不確定的轉(zhuǎn)換公式的真假性在新的TSS中將會變得更加清晰。在新的定義中→true包含所有肯定成立的轉(zhuǎn)換公式，→pos包含所有可能成立的轉(zhuǎn)換公式，刪除具有肯定為假的前提的規(guī)則，在其余的規(guī)則中刪除肯定成立的前提，如此多次歸約下去，若可以歸約到一個可分層的TSS，則將獲得一個唯一穩(wěn)定的轉(zhuǎn)換模型。

定義3[18]：令S=(Σ,R)為一TSS：

(1)True(S)=(Σ,True(R))，其中True(R)={r∈R|nprem(r)=?}。

(3)α是個序數(shù)，S進(jìn)行α次歸約后的結(jié)果記作Redα(S)，其遞歸定義為：

①Red0(S)=(Σ,Rclose)，Rclose表示R中規(guī)則基例化后的集合。

②Redα(S)=Reduce(S,∪β<α→true(Redβ(S)),∩β<α→pos(Redβ(S)))。

若一個TSSS可以歸約到可分層的TSS，則該TSS存在唯一穩(wěn)定的模型，否則不存在，稱該唯一穩(wěn)定的模型叫做S的相關(guān)模型，記作→S。

引理1[18]：如果一個TSSS可以歸約到一個可分層的TSS，即存在序數(shù)α使得Redα(S)成為正的TSS，則S的相關(guān)模型→S=→Redα(S)=→Pos(Redα(S))。

獲取TSS的相關(guān)模型是確保轉(zhuǎn)換系統(tǒng)的相關(guān)性質(zhì)能夠得到可靠證明的必要前提。

2 CC-模擬

定義4：令S=(ΣS,RS)為一TSS，→S為其相關(guān)模型，二元關(guān)系R?T(ΣS)×T(ΣS)是動作集A?Actτ上的CC-模擬關(guān)系當(dāng)且僅當(dāng)(P,Q)∈R蘊(yùn)含著對所有的a∈A滿足：

其中，Ar,Al,Abi是A上的一個劃分，三者互不相交，分別為共變、異變和互變動作集。PCC-模擬Q(記作P≥(Ar,Al)SQ)當(dāng)且僅當(dāng)存在一個CC-模擬關(guān)系R?T(ΣS)×T(ΣS)使得(P,Q)∈R。容易驗證≥(Ar,Al)S本身是S上的最大CC-模擬關(guān)系，且是前序關(guān)系(即自反和傳遞)。此處定義對τ動作和普通可視動作同等看待，因此所定義出的CC-模擬是個強(qiáng)的模擬概念。

易驗證上述概念是互模擬和模擬概念的一般化形式。若Ar=Al=?，則CC-模擬退化為常規(guī)的互模擬，若Al=Abi=?，則是常規(guī)的模擬。

為了后續(xù)同余性的證明，需要引入下面的S1?S2-CC-模擬的概念作為輔助。

定義5:給定S1=(ΣS1,RS1)，S2=(ΣS2,RS2)為兩個TSS，二者對應(yīng)的相關(guān)模型分別為→S1和→S2。二元關(guān)系R?T(ΣS1)×T(ΣS2)是動作集A?Actτ上的S1?S2-CC-模擬關(guān)系當(dāng)且僅當(dāng)(P,Q)∈R蘊(yùn)含著對所有的a∈A滿足：

上述概念是意圖用→S2去近似→S1(因為→S1執(zhí)行一個轉(zhuǎn)換動作→S2也可以執(zhí)行相同的轉(zhuǎn)換動作)，最終→S2將等同于→S1。則易知S1?S2-CC-模擬就是S1上的CC-模擬。

3 CC-模擬關(guān)于CC-ntyft/ntyxt算子的前同余性

行為關(guān)系的(前)同余性在支持規(guī)范的模塊化構(gòu)建和公理系統(tǒng)的推理方面具有重要意義。下面給出(前)同余性的一般定義。

定義6：設(shè)是一個代數(shù)結(jié)構(gòu)，R是集合S上的一個關(guān)系，如果R滿足以下條件，則R是一個前同余關(guān)系。

(1)R是一個前序關(guān)系；

(2)R對任意*i(1≤i≤n)，若*i是k元運(yùn)算符，且(aj,bj)∈R(1≤j≤k)，則(*i(a1,…,ak),*i(b1,…,bk))∈R。

若將(1)改成“R是等價關(guān)系”則得到同余的概念。

(前)同余性的概念用于支持規(guī)范的模塊化構(gòu)建和推理。當(dāng)系統(tǒng)具有(前)同余性時，某個項可以用與之行為等價的項進(jìn)行替換，而整個系統(tǒng)的行為保持不變。因此，獲取(前)同余性，將會幫助后續(xù)很多證明的實現(xiàn)，比如公理系統(tǒng)的可靠完備性證明中，(前)同余性通常都是必要的輔助。

由下文的例1-例4不難發(fā)現(xiàn)，不是所有的ntyft/ntyxt算子對CC-模擬都是保持前同余性的。因此，下面將提取出ntyft/ntyxt算子中能滿足前同余性要求的算子來進(jìn)行研究，并說明所獲取的是能滿足CC-模擬前同余性要求的ntyft/ntyxt算子的最大子集。

定義7：一個基于型Σ的ntyft規(guī)則是由一組轉(zhuǎn)換公式作為前提和一個單獨的公式作為后承組成的，形式如下：

其中，ak,bj,c∈Actτ且互不相同，f∈Σ是l元算子，yk,xi(1≤i≤l)∈VPk,Pj,P∈T(Σ)，K和J是(可能無限的)下標(biāo)的集合。

一個規(guī)則是ntyxt形式當(dāng)其符合如下形式：

其中，yk,x∈V且互不相同，ak,bj,c∈Actτ，Pk,Pj,P∈T(Σ)，K和J是(可能無限的)下標(biāo)的集合。

稱滿足ntyft或者ntyxt形式的規(guī)則為ntyft/ntyxt規(guī)則，稱利用ntyft/ntyxt規(guī)則定義的算子為ntyft/ntyxt算子。若一個TSS的所有算子都是ntyft/ntyxt算子，則稱這種由ntyft/ntyxt算子構(gòu)成的TSS為nTSS。

定義8：給定一nTSS中的算子f，若所有對其定義的規(guī)則都滿足以下兩個條件：

則稱滿足上述條件的ntyft/ntyxt規(guī)則為CC-ntyft/ntyxt規(guī)則，稱利用CC-ntyft/ntyxt規(guī)則定義的算子為CC-ntyft/ntyxt算子。一個nTSS若其所有的算子都是CC-ntyft/ntyxt算子，那么稱該nTSS為CC-nTSS。

下面的四個規(guī)則的例子將說明所做的限制條件的必要性。這些例子都是基于一nTSSS=(Σ,R)，Σ中僅包含0，+和a.()算子(三者的操作語義和CCS[1]中定義一致)以及算子();()，動作標(biāo)記al∈Al，ar∈Ar。

例1：假設(shè)();()算子的定義規(guī)則只有一條，即

例2：假設(shè)算子();()對應(yīng)的規(guī)則改為：

例3：繼續(xù)修改();()的語義規(guī)則：

例4：將();()的語義規(guī)則更改為：

類似于例1易知，后面的三個規(guī)則定義的算子都不滿足CC-模擬前同余性。此四個例子足以說明上述限制條件的必要性。下面給出所獲得的CC-ntyft/ntyxt算子對CC-模擬的前同余性的證明。因此可見CC-ntyft/ntyxt算子是ntyft/ntyxt算子中能滿足CC-模擬前同余性的最大子集。

在證明前同余性之前，給出下面的兩條引理來幫助證明。

引理2[18]：假設(shè)一個nTSSS1歸約后可分層，則存在一個良基的且歸約后可分層的nTSSS2與之等價(兩個TSS等價即二者具有相同的相關(guān)模型)。

引理3[18]：任何nTSS都存在一個ntyft規(guī)則形式定義的純(pure)nTSS(純TSS按常規(guī)定義)與之等價。

由上面的兩條引理，對前同余性證明可直接基于歸約后可分層且僅含ntyft規(guī)則的純nTSS進(jìn)行。

定理2(前同余性)：令S是一個CC-nTSS，假設(shè)S能夠歸約到一個可分層的CC-nTSS，則≥(Ar,Al)S是一個前同余關(guān)系。

證明：定理2的證明主要分為以下幾步。

(1)構(gòu)造關(guān)系R驗證R是一個前同余關(guān)系即可得證上述定理:

(2)要驗證R是一個前同余關(guān)系需要證明以下斷言:假設(shè)S是一個純CC-nTSS，且其中的規(guī)則僅符合ntyft形式，對所有的序數(shù)α≥0，R是一個：

①S?Pos(Redα(S))-CC-模擬；

②True(Redα(S))?S-CC-模擬。

證明此斷言需要對①②兩項同時基于序數(shù)α進(jìn)行超限歸納，再分別證明①和②。

假設(shè)S=(ΣS,RS)，(P,Q)∈R，對于需驗證：

驗證上述的(CCR)、(CCL)條件時，因→S即→Strip(S,→s)，可借助定義1中S和Strip(S,→s)規(guī)則之間的聯(lián)系，利用Strip(S,→s)中的正規(guī)則以及歸約的相關(guān)性質(zhì)，易構(gòu)造出一閉替換σ找出匹配的Q'或者P'相應(yīng)地使(CCR)、(CCL)條件成立。

對于②的證明需類似①驗證True(Redα(S))?S-CC-模擬的(CCR)、(CCL)條件。①②的具體證明過程可類比文獻(xiàn)[18]中l(wèi)emma8.9的證明，注意區(qū)別對待動作類型即可。

(3)基于(1)(2)的證明結(jié)果，且由S是歸約后可分層的，根據(jù)引理1可知

R?S?Pos(Redα(S))-CC-模擬=

≥(Ar,Al)S?R，即R=≥(Ar,Al)S，再根據(jù)引理2、引理3，則定理2得證。

定理2的結(jié)果，對于符合CC-nTSS形式的這類系統(tǒng)關(guān)于CC-模擬、模擬以及互模擬關(guān)系的前同余性或者同余性的證明可直接套用。

4 結(jié)束語

基于ntyft/ntyxt規(guī)則形式的算子對CC-模擬的前同余性進(jìn)行探究，文中提出了ntyft/ntyxt算子中能夠滿足CC-模擬前同余性的最大子類CC-ntyft/ntyxt。ntyft/ntyxt規(guī)則形式是被廣泛研究的SOS規(guī)則的框架形式之一，文中的研究成果可推廣到對符合ntyft/ntyxt規(guī)則框架形式的進(jìn)程代數(shù)語言判定其算子是否滿足CC-模擬、模擬、互模擬的(前)同余性。在該研究的基礎(chǔ)上，后續(xù)可基于CC-ntyft/ntyxt規(guī)則形式針對CC-模擬的公理化展開研究，從而獲得一個公理系統(tǒng)構(gòu)造的一般性方法，避免公理化過程的重復(fù)勞動。