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