CLT含遞歸算子的最大前同余性

鄧鵬輝，張晉津

(南京航空航天大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇南京 210016)

CLT含遞歸算子的最大前同余性

鄧鵬輝，張晉津

(南京航空航天大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇南京 210016)

進(jìn)程之間的等價(jià)關(guān)系或精化關(guān)系的同余或前同余性(congruence或precongruence)是組合式推理和模塊化設(shè)計(jì)驗(yàn)證的理論基礎(chǔ)。針對(duì)面向Web Service的進(jìn)程演算，Bernardi和Hennessy提出了Client-Must-Testing(CLT)語(yǔ)義及相關(guān)的測(cè)試前序ㄈ用于描述進(jìn)程的精化關(guān)系，并對(duì)包含于的最大前同余關(guān)系+進(jìn)行了研究。遞歸算子是規(guī)范理論中重要而且是基礎(chǔ)性的算子，Bernardi和Hennessy對(duì)包含于的最大前同余關(guān)系的研究中未涉及遞歸算子，因此不能描述進(jìn)程的無(wú)限行為。文中研究了CLT誘導(dǎo)出的精化關(guān)系在包含遞歸算子情形下的前同余性。在討論了環(huán)境(context)、遞歸進(jìn)程以及一步轉(zhuǎn)換內(nèi)在聯(lián)系的基礎(chǔ)上，給出包含于的最大前同余關(guān)系。

進(jìn)程代數(shù);must-testing語(yǔ)義;精化關(guān)系;遞歸算子;最大前同余

0 引言

在進(jìn)程代數(shù)理論中，Nicola和Hennessy早期提出三種測(cè)試語(yǔ)義(may，must，may＆must)用來(lái)描述精化關(guān)系，基于被測(cè)試進(jìn)程與環(huán)境間的相互作用誘導(dǎo)出的計(jì)算路徑序列，分析其行為［1-3］。近幾年，Barbanera等提出面向網(wǎng)絡(luò)服務(wù)器的必須測(cè)試?yán)碚摚?-7］;Bernardi和Hennessy提出了面向網(wǎng)絡(luò)服務(wù)器的Client Must Testing(CLT)語(yǔ)義用于描述精化關(guān)系［8］。它介紹了兩種子行為關(guān)系:服務(wù)器(server)和客戶(client)，并描述了它們之間的相互作用，并且它們的語(yǔ)義定義一致，都可以看成是進(jìn)程。

遞歸算子是規(guī)范理論中重要而且是基礎(chǔ)性的算子，但文獻(xiàn)［8］在處理同余性時(shí)對(duì)此未加考慮。文中基于Hennessy等提出的CLT，研究環(huán)境、遞歸進(jìn)程的展開(kāi)與進(jìn)程轉(zhuǎn)換之間的內(nèi)在聯(lián)系，在此基礎(chǔ)上考察CLT含遞歸算子的最大前同余關(guān)系。

1 預(yù)備知識(shí)

本節(jié)將給出文中使用的一些符號(hào)和基本概念，簡(jiǎn)單介紹CLT的語(yǔ)法及其結(jié)構(gòu)化操作語(yǔ)義規(guī)則。

定義1［8］:CLT的項(xiàng)由BNF范式定義如下:

t::=0|1|a.t|t+t|t⊕t|X|recX.t

其中，X∈Var，a∈Act。

為了書(shū)寫(xiě)方便，在不引起歧義的情況下，將a.t記為at。

各個(gè)算子簡(jiǎn)單介紹如下:0表示“死”進(jìn)程，不能執(zhí)行任何動(dòng)作;1表示成功的記號(hào)，被處理成一個(gè)不執(zhí)行任何動(dòng)作的進(jìn)程;a.t只能執(zhí)行a動(dòng)作，之后t才能執(zhí)行;t1+t2表示外部不確定選擇，通過(guò)與外界環(huán)境的交互選擇執(zhí)行t1或者t2，當(dāng)執(zhí)行t1(t2)，t2(t1)被自動(dòng)拋棄;t1⊕t2表示內(nèi)部不確定選擇，與t1+t2的不同之處在于由系統(tǒng)內(nèi)部選擇執(zhí)行t1或者t2，而與外界環(huán)境無(wú)關(guān);recX.t表示遞歸項(xiàng)。

下面給出變?cè)猉在項(xiàng)t中約束出現(xiàn)的遞歸定義:

(2)如果X≡Y，或者X在t中約束出現(xiàn)，那么X 在recX.t中約束出現(xiàn)。如果不是約束出現(xiàn)，則稱它是自由出現(xiàn)。若X在t中自由出現(xiàn)，則稱X是t的自由變?cè)?/p>

約定1:與通常做法一樣，文中假設(shè)對(duì)任意兩個(gè)遞歸項(xiàng)recX.t1、recY.t2，有X≠Y并且對(duì)任何給定的進(jìn)程t而言，任何變?cè)粫?huì)在t中既有自由出現(xiàn)又有約束出現(xiàn)。顯然，這兩個(gè)約定均可通過(guò)對(duì)遞歸變?cè)m當(dāng)換名得以實(shí)現(xiàn)。

給定項(xiàng)t，它的自由變?cè)募?記為FV(t))及子項(xiàng)的集合按通常方式定義，如果FV(t)=?，它就被稱為進(jìn)程，一般用符號(hào)p、q和r表示。t1≡t2表示兩個(gè)表達(dá)式t1和t2語(yǔ)法相同。

定義2(環(huán)境):一個(gè)環(huán)境CX～就是一個(gè)項(xiàng)，該項(xiàng)所含自由變?cè)趎-元組=(X1，X2，…，Xn)中，元組中的變?cè)ゲ幌嗤襫≥0。給定進(jìn)程n-元組=(p1，p2，…，pn)，將同時(shí)把中每個(gè)Xi替換為pi而形成的項(xiàng) 記 為{p1/X1，p2/X2，…/} (簡(jiǎn) 記 為{)。

定義3［2］(擴(kuò)展的標(biāo)記轉(zhuǎn)換系統(tǒng)):擴(kuò)展的標(biāo)記轉(zhuǎn)換系統(tǒng)(Extended Labelled Transition System，ELTS)是一個(gè)4元組 ＜P，Act，→，a＞，轉(zhuǎn)換關(guān)系，a由圖1中的結(jié)構(gòu)化操作語(yǔ)義規(guī)則(Structural Operational Semantics，SOS)［8-9］按通常的方式?jīng)Q定，其中P為所有進(jìn)程形成的集合，a∈Act，α∈Act√。表示存在q使得pq。表示p(a )*(a)*q，此處(a)* 是a的自反傳遞閉包。p?asq表示pq。p表示對(duì)任意的q，q不 成 立。q 表 示 存 在 轉(zhuǎn) 換 序 列，其中s=a1a2…an，并且這個(gè)轉(zhuǎn)換序列中的任何狀態(tài)p＇都滿足p＇。類(lèi)似地，針對(duì)關(guān)系a，可以定義類(lèi)似的記號(hào)，此外不再贅述。

如果存在無(wú)限序列p a p1a p2a…，則稱p發(fā)散，記為p?;否則稱p收斂，記為p?。

上述SOS規(guī)則直觀、含義顯然，需要指出的一點(diǎn)是，遞歸算子操作語(yǔ)義通常按如下方式定義:

例如，Milner在CCS中采用上述方式定義遞歸。一般來(lái)講，兩者定義差別不大，文中選用的規(guī)則較常規(guī)定義方式僅多了一步內(nèi)部轉(zhuǎn)換。但是，關(guān)于recX.X卻截然不同，常規(guī)定義中，該進(jìn)程表示“死”進(jìn)程，既不能執(zhí)行任何動(dòng)作序列，也不能執(zhí)行內(nèi)動(dòng)作。然而在文中，由R6可知recX.Xa recX.X，所以該進(jìn)程表示一個(gè)發(fā)散進(jìn)程，記為Θ。該進(jìn)程在后續(xù)證明中將多次使用。

由圖1中R6可知，由于遞歸算子的存在，進(jìn)程的一步轉(zhuǎn)換所到達(dá)的子進(jìn)程結(jié)構(gòu)可能比其自身結(jié)構(gòu)更復(fù)雜，因此，結(jié)構(gòu)歸納法一般不適用。所以，考慮根據(jù)證明樹(shù)的深度進(jìn)行歸納證明。

將形如p →—α q或者p a q的表達(dá)式稱為文字，其中，p、q是進(jìn)程，α∈Act√，一般用?、φ、χ等表示。由圖1可知，CLT的SOS規(guī)則最多只含有一個(gè)前提條件，因此給出其證明樹(shù)的定義。

定義4(證明樹(shù)):一個(gè)文字χ的證明是一棵良基的(well-founded)向上分叉的樹(shù)，樹(shù)的每個(gè)節(jié)點(diǎn)都標(biāo)記為文字，并且滿足下面兩個(gè)條件:

(1)根被標(biāo)記為χ;

(2)如果?、φ分別是節(jié)點(diǎn)p、q的標(biāo)記且q是p的子節(jié)點(diǎn)，則存在SOS規(guī)則的例化R，使得R≡。

為了描述進(jìn)程的行為，測(cè)試語(yǔ)義引進(jìn)了進(jìn)程的復(fù)合結(jié)構(gòu)p‖q，其操作語(yǔ)義規(guī)則如圖2所示［8］。

具有如下形式的轉(zhuǎn)換序列稱為p‖r的一條計(jì)算路徑。

p‖r=p0‖r0→p1‖r1→…→pk‖rk→…

如果它是無(wú)限的或者它的最終狀態(tài)pn‖rn滿足pn‖，則稱它是極大的;如果存在0≤k＜ω滿足，則稱它是成功的。

定義5［8］:如果p‖r的所有極大計(jì)算路徑都是成功的，則稱p必然滿足r，記為p must r。

定義6［8］(有用進(jìn)程):給定進(jìn)程r，如果存在進(jìn)程p使得p must r，則稱r是有用進(jìn)程。用Uclt表示所有有用進(jìn)程形成的集合。

定義7［8］(測(cè)試前序):對(duì)任意的進(jìn)程p，如果存在p must r1蘊(yùn)含p must r2，則稱r1是r2的精化，記為r1r2。

如果r1r2并且r2r1，則稱r1，r2精化相等，記為r

2 CLT的最大前同余關(guān)系

在進(jìn)程代數(shù)描述的并發(fā)系統(tǒng)中，進(jìn)程之間的等價(jià)關(guān)系(或精化關(guān)系)的同余(congurence)(或前同余)性是組合推理的基礎(chǔ)，同時(shí)也是模塊化設(shè)計(jì)的必要條件。

定義8(前同余性):對(duì)任意進(jìn)程r1、r2，環(huán)境及進(jìn)程之間的精化關(guān)系，如果r1r2使得CX{ p /X}CX{ q /X}，則稱具有前同余性。

(1)拋棄+算子;

Milner在文獻(xiàn)［10］中處理弱互模擬(weak-bisimulation)的等價(jià)關(guān)系≈時(shí)，遇到類(lèi)似的問(wèn)題，≈關(guān)于+算子不具有同余性。Milner給出了包含于≈的觀測(cè)同余(observation-congurent)關(guān)系=。

Hennessy等在文獻(xiàn)［8］中對(duì)最大前同余性進(jìn)行了研究，但他們只考慮了有限的進(jìn)程行為。為了刻畫(huà)無(wú)限的進(jìn)程行為，文中引入遞歸算子recX.t，將對(duì)包含遞歸算子的最大前同余關(guān)系進(jìn)行研究。首先定義包含于二元關(guān)系集，接著研究環(huán)境、進(jìn)程以及一步轉(zhuǎn)換三者之間的關(guān)系，最后證明關(guān)系就是包含于CLT的最大前同余關(guān)系。

(2)對(duì)任意進(jìn)程r1、r2，若r1r2，則存在a∈Act使得r1+a.1r2+a.1(其中a不在r1、r2中出現(xiàn))。

r1?+r2與r1?r2類(lèi)似定義。

容易驗(yàn)證如果r1+a.1r2+a.1，那么r1+b.1r2+b.1(其中a，b不在r1，r2中出現(xiàn))。所以將條件(2)中的存在改成任意是等價(jià)的定義。

3 結(jié)束語(yǔ)

在進(jìn)程代數(shù)理論發(fā)展中，提出了許多刻畫(huà)進(jìn)程語(yǔ)義的概念［11-17］。為了刻畫(huà)無(wú)限的進(jìn)程行為，文中基于CLT語(yǔ)義，研究環(huán)境、遞歸進(jìn)程的展開(kāi)與進(jìn)程轉(zhuǎn)換之間的內(nèi)在聯(lián)系，給出了一步轉(zhuǎn)換背后的模式以及含遞歸算子的進(jìn)程間的關(guān)系集，并證明就是包含于的最大前同余關(guān)系。

文中的研究只是相關(guān)領(lǐng)域的一部分，針對(duì)不同問(wèn)題還有許多值得研究的方向，如:mutually must-testing semantic(P2P)的含遞歸算子的最大前同余性，CLT、P2P方程唯一解和最大解等等。

［1］ DeNicola R，Hennessy M.Testing equivalences for processes ［J］.ELSEVIER，1983，34(1-2):83-133.

［2］ Hennessy M.Algebraic theory of processes［M］.［s.l.］:MIT Press，1988.

［3］ DeNicola R，Hennessy M.Ccs without tau’s［M］//LNCS.Berlin:Springer，1987:138-152.

［4］ Castagna G，Gesbert N，Padovani L.A theory of contracts for web services［J］.ACM SIGPLAN Notices，2008，31(5):261-272.

［5］ Barbanera F，De’Liguoro U.Two notions of sub-behaviour for session-based client/server systems［C］//Proc of PPDP.New York:ACM，2010:155-164.

［6］ Laneve C，Padovani L.The must preorder revisited［M］// CONCUR 2007-concurrency theory.Berlin:Springer，2007: 212-225.

［7］ Padovani L.Contract-based discovery of web services modulo simple orchestrators［J］.Theoretical Computer Science，2010，411(37):3328-3347.

［8］ Bernardi G，Hennessy M.Mutually testing processes［J］.Logical Methods in Computer Science，2015，11(2):61-75.

［9］ Plotkin G.A structural approach to operational semantics［R］. Aarhus:Aarhus University，1981.

［10］Milner R.Communication and concurrency［M］.［s.l.］:Prentice Hall，1989.

［11］Keller R M.Formal verification of parallel programs［J］.Communications of ACM，1976，19(7):371-384.

［12］van Glabbeek R J.The linear time-branching time［M］.Berlin:Springer，1990:278-297.

［13］Hoare C A R.Communicating sequential process［J］.Communications of the ACM，1978，21(8):666-677.

［14］Milner R.An algebraic definition of simulation between programs［C］//Proc of the 2nd international joint conference on artificial intelligence.San Francisco:Morgan Kaufmann Publisher，1971:481-489.

［15］Park D.Concurrency and automata on infinite sequences［M］. Berlin:Springer，1981:167-183.

［16］Bloom B，Istrail S，Meyer A R.Bisimulation can’t be traced ［J］.Journal of ACM，1995，42(1):232-268.

［17］Lrsen K G，Skou A.Bisimulation through probabilistic testing ［J］.Information and Computation，1991，94(1):84-94.

Largest Precongurence with Recursive Operator in CLT

DENG Peng-hui，ZHANG Jin-jin
(School of Computer Science and Technology，Nanjing University of Aeronautics and Astronautics，Nanjing 210016，China)

Process algebra aims to provide algebraic theories for concurrent communication system，where the notions of behavioral equivalence and refinement play central roles.In particular，congruence or precongruence of behavioral relations provide theoretical foundation for compositional reasoning and modular designing and verifying.In order to capture the concurrent behavior of the server and the client，Bernardi and Hennessy present a Web Service-oriented semantic CLT(Client Must Testing).They studied the largest precongurence contained in the refinement relationinduced by CLT without considering recursive.Recursive operator is important and fundamental in specification theory.Bernardi and Hennessy have studied the largest precongurence contained in.However，infinite processes cannot be expressed in such framework due to lacking recursive operator.Based on the exploring relationship among contexts，recursive processes and one step transition，a characterization for the largest precongurence contained inin the presence of recursive operator is presented.

process algebra;must-testing semantic;refinement;recursive operator;largest precongurence

TP301

A

1673-629X(2016)09-0143-06

10.3969/j.issn.1673-629X.2016.09.032

2015-12-08

2016-04-05< class="emphasis_bold">網(wǎng)絡(luò)出版時(shí)間

時(shí)間:2016-08-23

國(guó)家自然科學(xué)基金資助項(xiàng)目(11426136，60973045);江蘇省高校自然科學(xué)基金(13KJB520012)

鄧鵬輝(1986-)，男，碩士研究生，研究方向?yàn)檫M(jìn)程代數(shù)、計(jì)算機(jī)科學(xué)中的邏輯學(xué)等;張晉津，講師，博士，研究方向?yàn)樾问交绞健⒂?jì)算機(jī)科學(xué)中的邏輯學(xué)等。

http://www.cnki.net/kcms/detail/61.1450.TP.20160823.1359.052.html