CLT树型指称语义的研究

南京航空航天大学计算机科学与技术学院 邓鹏辉 张晋津



CLT树型指称语义的研究

南京航空航天大学计算机科学与技术学院 邓鹏辉 张晋津

【摘要】在面向服务器的进程代数理论中，为了描述服务器和客户之间的并发行为，Bernardi 和 Hennessy等人提出了client must-testing（CLT）语义，service must-testing(SVR)语义用于描述进程的精化关系,并对SVR的前缀封闭集以及树型指称语义进行了的研究。但关于CLT语义的指称语义并未涉及，本文将基于此语义，通过建立标准型的方法，对此语义的树型指称语义进行研究。

【关键词】进程代数；并发行为；must-testing语义；指称语义；标准型

0 引言

在进程代数理论中，Nicola和Hennessy早期提出三种测试语义(may,must,may&must)用来描述精化关系，基于被测试进程与环境间的相互作用诱导出的计算路径序列，分析其行为[1]。近几年，Barbanera, Liguoro, Castagna等人提出面向网络服务器的必须测试理论[2]，Bernardi和Hennessy提出了面向网络服务器的CLT语义以及SVR语义用于描述精化关系[3]。它介绍了两种子行为关系:服务器（server）和客户(client)，并描述了它们之间的相互作用。在进程代数理论中指称语义[4]是一个与操作语义[5]类似地描述，而文献[3]在处理CLT语义时对此并未涉及。本文基于Hennessy等人提出的CLT语义，将通过建立进程的标准型，研究与此语义具有完全抽象性的树形指称语义。

1 预备知识

本节简单介绍CLT的语法及其结构化操作语义规则，CLT测试前序的语法以及语义定义，以及饱和集的概念。关于CLT的更多详细介绍可以参考文献[2][3]。本文所使用的符号都是常用符号，其基本含义与Milner在文献[3][7]中使用的意义一致。

定义1[3]CLT的项（进程）由BNF范式定义如下：

表1 CLT结构操作语义规则

则称

则称Д是S-set。

引理2：C(ß)是包含ß的最小饱和集。

证明：参考文献[6]引理2.33。

2 有限接收树集（FAT）

本节将给出CLT语义的树型指针模型成为有限接收树集（finite acceptance tree FAT），以及进程是如何指称到该FAT中的。

2.1 FAT的基本概念

FAT可以看成是一种带标记的有根树。

定义8：（FAT）FAT是带根节点的有限接收树的集合,并且它的分支标记为Act的动作集，节点标记为Act*的子集以及{0,1,2}的子集，并且满足R1，R2，R3，R4。

R1 对任意的动作a，树中任意节点最多只有一个标记为a的后继分支。

R3 Acc(n)是一个S（n）-Set。

R4 对任意节点n，如果M（n）=1或者M（n）=2，那么他就是叶节点。

2.2 FAT上的指称

接下来我们介绍进程是如何指称到FAT中的。给定树tÎ FAT，L（t）表示树t的所有节点组成的集合，或者说树t通过的路径的集合。我们给出CLT的各个算子在FAT中的指称。

定义9：CLT的各个算子在FAT中的指称按如下方式定义：

（1）0FAT，FAT

他们表示同一颗树，该树只有一个节点，没有分支并且满足如下要求：

（2）1FAT

它表示的树也只有1个节点，没有分支，与0FAT不同之处是M（t）=1，FL(t)=。

（3）aFAT.

（4）+FAT

如果t1，t2FAT，那么t1+FATt2满足如下要求：

如果t1，t2FAT，那么t1FATt2表示的树满足如下要求：

3 完全抽象性

3.1 FAT的精化关系

1) 如果M(t(s))=1或者M(t(s))=2，那么t(s)UT；

定义13（FAT的精化关系）：对任意的t1，t2FAT，sAct，如果t use s使得下面三个条件成立：

那么称t1是t2的精化，记作t1t2。

3.2 完全抽象性

证明 参考文献[3]定理7.10。

证明 我们按p的结构归纳易证。

证明 根据s的长度以对p分情形讨论纳易证。

证明 对p分情形讨论纳易证。

证明 由引理4，引理5，定义3及定义12易证。

证明 由前面分析易证。

4 结束语

本文基于CLT语义，提出FAT的概念，以及FAT的精化关系。通过建立标准型的方法，证明标准型它的指称FAT具有完全抽象性，从而得出CLT与它的指称FAT具有完全抽象性。

本文的研究工作只是相关领域的一部分，针对不同问题还有许多值得研究的方向，如：本文只讨论了进程的有限行为，可以在此基础上加入递归算子，用以刻画无限的行为。该语义中含递归算子的最大前同余性，方程唯一解和最大解等等研究领域都未涉及。

参考文献

[1]Nicola D,Hennessy M.Testing equivalences for processes[J].ELSEVIER,1983,34(1-2):83-133.

[2]Castagna G,Gelbert N，Padovani L.A theory of contracts for web services [J].ACM Trans.,2009,31(5):1-61.

[3]Bernardi G,Hennessy M.Mutually testing processes[J]. ACM,2015,11(2:1):1-23.

[4]Tofts C,Birtwistle G.A Denotational Semantics for a Process Based Simulation Language[J].ACM Transactions on Modeling and Computer Simulation, Vol.8, No.3,July 1998, Pages 281–304.

[5]Aceto L,Fokkink W,Verhoesf C.Structural operational semantics[J]. J.A.Bergstra, A.Ponse, S.A.Smolka, Handbook of process Algebra, Elsevier Science,2001:197-292.

[6]Hennessy M.Algebraic Theory of Processes[J].MIT Press,1988,1-272.

[7]Milner R.Communication and Concurrency[J]. Prentice Hall,1989,1-260.

邓鹏辉（1986－），男，江西鹰潭人，南京航空航天大学计算机科学与技术学院研究生，研究方向：进程代数、计算机科学中的逻辑学等。

张晋津（1981－），男，山西曲沃人，博士，讲师，研究方向：形式化方式、计算机科学中的逻辑学等。

作者简介：

基金项目：国家自然科学基金11426136，60973045；江苏省高校自然科学基金13KJB520012。