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

鄧鵬輝，張晉津

(南京航空航天大學計算機科學與技術學院，江蘇南京 210016)

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

鄧鵬輝，張晉津

(南京航空航天大學計算機科學與技術學院，江蘇南京 210016)

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

進程代數;must-testing語義;精化關系;遞歸算子;最大前同余

0 引言

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

遞歸算子是規范理論中重要而且是基礎性的算子，但文獻［8］在處理同余性時對此未加考慮。文中基于Hennessy等提出的CLT，研究環境、遞歸進程的展開與進程轉換之間的內在聯系，在此基礎上考察CLT含遞歸算子的最大前同余關系。

1 預備知識

本節將給出文中使用的一些符號和基本概念，簡單介紹CLT的語法及其結構化操作語義規則。

定義1［8］:CLT的項由BNF范式定義如下:

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

其中，X∈Var，a∈Act。

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

各個算子簡單介紹如下:0表示“死”進程，不能執行任何動作;1表示成功的記號，被處理成一個不執行任何動作的進程;a.t只能執行a動作，之后t才能執行;t1+t2表示外部不確定選擇，通過與外界環境的交互選擇執行t1或者t2，當執行t1(t2)，t2(t1)被自動拋棄;t1⊕t2表示內部不確定選擇，與t1+t2的不同之處在于由系統內部選擇執行t1或者t2，而與外界環境無關;recX.t表示遞歸項。

下面給出變元X在項t中約束出現的遞歸定義:

(2)如果X≡Y，或者X在t中約束出現，那么X 在recX.t中約束出現。如果不是約束出現，則稱它是自由出現。若X在t中自由出現，則稱X是t的自由變元。

約定1:與通常做法一樣，文中假設對任意兩個遞歸項recX.t1、recY.t2，有X≠Y并且對任何給定的進程t而言，任何變元不會在t中既有自由出現又有約束出現。顯然，這兩個約定均可通過對遞歸變元適當換名得以實現。

給定項t，它的自由變元的集合(記為FV(t))及子項的集合按通常方式定義，如果FV(t)=?，它就被稱為進程，一般用符號p、q和r表示。t1≡t2表示兩個表達式t1和t2語法相同。

定義2(環境):一個環境CX～就是一個項，該項所含自由變元在n-元組=(X1，X2，…，Xn)中，元組中的變元互不相同且n≥0。給定進程n-元組=(p1，p2，…，pn)，將同時把中每個Xi替換為pi而形成的項 記 為{p1/X1，p2/X2，…/} (簡 記 為{)。

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

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

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

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

由圖1中R6可知，由于遞歸算子的存在，進程的一步轉換所到達的子進程結構可能比其自身結構更復雜，因此，結構歸納法一般不適用。所以，考慮根據證明樹的深度進行歸納證明。

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

定義4(證明樹):一個文字χ的證明是一棵良基的(well-founded)向上分叉的樹，樹的每個節點都標記為文字，并且滿足下面兩個條件:

(1)根被標記為χ;

(2)如果?、φ分別是節點p、q的標記且q是p的子節點，則存在SOS規則的例化R，使得R≡。

為了描述進程的行為，測試語義引進了進程的復合結構p‖q，其操作語義規則如圖2所示［8］。

具有如下形式的轉換序列稱為p‖r的一條計算路徑。

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

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

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

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

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

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

2 CLT的最大前同余關系

在進程代數描述的并發系統中，進程之間的等價關系(或精化關系)的同余(congurence)(或前同余)性是組合推理的基礎，同時也是模塊化設計的必要條件。

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

(1)拋棄+算子;

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

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

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

r1?+r2與r1?r2類似定義。

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

3 結束語

在進程代數理論發展中，提出了許多刻畫進程語義的概念［11-17］。為了刻畫無限的進程行為，文中基于CLT語義，研究環境、遞歸進程的展開與進程轉換之間的內在聯系，給出了一步轉換背后的模式以及含遞歸算子的進程間的關系集，并證明就是包含于的最大前同余關系。

文中的研究只是相關領域的一部分，針對不同問題還有許多值得研究的方向，如: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">網絡出版時間

時間:2016-08-23

國家自然科學基金資助項目(11426136，60973045);江蘇省高校自然科學基金(13KJB520012)

鄧鵬輝(1986-)，男，碩士研究生，研究方向為進程代數、計算機科學中的邏輯學等;張晉津，講師，博士，研究方向為形式化方式、計算機科學中的邏輯學等。

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