南京航空航天大學(xué)計算機科學(xué)與技術(shù)學(xué)院 鄧鵬輝 張晉津

?

CLT樹型指稱語義的研究

南京航空航天大學(xué)計算機科學(xué)與技術(shù)學(xué)院 鄧鵬輝 張晉津

【摘要】在面向服務(wù)器的進程代數(shù)理論中，為了描述服務(wù)器和客戶之間的并發(fā)行為，Bernardi 和 Hennessy等人提出了client must-testing（CLT）語義，service must-testing(SVR)語義用于描述進程的精化關(guān)系,并對SVR的前綴封閉集以及樹型指稱語義進行了的研究。但關(guān)于CLT語義的指稱語義并未涉及，本文將基于此語義，通過建立標(biāo)準(zhǔn)型的方法，對此語義的樹型指稱語義進行研究。

【關(guān)鍵詞】進程代數(shù)；并發(fā)行為；must-testing語義；指稱語義；標(biāo)準(zhǔn)型

0 引言

在進程代數(shù)理論中，Nicola和Hennessy早期提出三種測試語義(may,must,may&must)用來描述精化關(guān)系，基于被測試進程與環(huán)境間的相互作用誘導(dǎo)出的計算路徑序列，分析其行為[1]。近幾年，Barbanera, Liguoro, Castagna等人提出面向網(wǎng)絡(luò)服務(wù)器的必須測試理論[2]，Bernardi和Hennessy提出了面向網(wǎng)絡(luò)服務(wù)器的CLT語義以及SVR語義用于描述精化關(guān)系[3]。它介紹了兩種子行為關(guān)系:服務(wù)器（server）和客戶(client)，并描述了它們之間的相互作用。在進程代數(shù)理論中指稱語義[4]是一個與操作語義[5]類似地描述，而文獻[3]在處理CLT語義時對此并未涉及。本文基于Hennessy等人提出的CLT語義，將通過建立進程的標(biāo)準(zhǔn)型，研究與此語義具有完全抽象性的樹形指稱語義。

1 預(yù)備知識

本節(jié)簡單介紹CLT的語法及其結(jié)構(gòu)化操作語義規(guī)則，CLT測試前序的語法以及語義定義，以及飽和集的概念。關(guān)于CLT的更多詳細介紹可以參考文獻[2][3]。本文所使用的符號都是常用符號，其基本含義與Milner在文獻[3][7]中使用的意義一致。

定義1[3]CLT的項（進程）由BNF范式定義如下：

表1 CLT結(jié)構(gòu)操作語義規(guī)則

則稱

則稱Д是S-set。

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

證明：參考文獻[6]引理2.33。

2 有限接收樹集（FAT）

本節(jié)將給出CLT語義的樹型指針模型成為有限接收樹集（finite acceptance tree FAT），以及進程是如何指稱到該FAT中的。

2.1 FAT的基本概念

FAT可以看成是一種帶標(biāo)記的有根樹。

定義8：（FAT）FAT是帶根節(jié)點的有限接收樹的集合,并且它的分支標(biāo)記為Act的動作集，節(jié)點標(biāo)記為Act*的子集以及{0,1,2}的子集，并且滿足R1，R2，R3，R4。

R1 對任意的動作a，樹中任意節(jié)點最多只有一個標(biāo)記為a的后繼分支。

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

R4 對任意節(jié)點n，如果M（n）=1或者M（n）=2，那么他就是葉節(jié)點。

2.2 FAT上的指稱

接下來我們介紹進程是如何指稱到FAT中的。給定樹t? FAT，L（t）表示樹t的所有節(jié)點組成的集合，或者說樹t通過的路徑的集合。我們給出CLT的各個算子在FAT中的指稱。

定義9：CLT的各個算子在FAT中的指稱按如下方式定義：

（1）0FAT，F(xiàn)AT

他們表示同一顆樹，該樹只有一個節(jié)點，沒有分支并且滿足如下要求：

（2）1FAT

它表示的樹也只有1個節(jié)點，沒有分支，與0FAT不同之處是M（t）=1，F(xiàn)L(t)=。

（3）aFAT.

（4）+FAT

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

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

3 完全抽象性

3.1 FAT的精化關(guān)系

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

定義13（FAT的精化關(guān)系）：對任意的t1，t2FAT，sAct，如果t use s使得下面三個條件成立：

那么稱t1是t2的精化，記作t1t2。

3.2 完全抽象性

證明 參考文獻[3]定理7.10。

證明 我們按p的結(jié)構(gòu)歸納易證。

證明 根據(jù)s的長度以對p分情形討論納易證。

證明 對p分情形討論納易證。

證明 由引理4，引理5，定義3及定義12易證。

證明 由前面分析易證。

4 結(jié)束語

本文基于CLT語義，提出FAT的概念，以及FAT的精化關(guān)系。通過建立標(biāo)準(zhǔn)型的方法，證明標(biāo)準(zhǔn)型它的指稱FAT具有完全抽象性，從而得出CLT與它的指稱FAT具有完全抽象性。

本文的研究工作只是相關(guān)領(lǐng)域的一部分，針對不同問題還有許多值得研究的方向，如：本文只討論了進程的有限行為，可以在此基礎(chǔ)上加入遞歸算子，用以刻畫無限的行為。該語義中含遞歸算子的最大前同余性，方程唯一解和最大解等等研究領(lǐng)域都未涉及。

參考文獻

[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－），男，江西鷹潭人，南京航空航天大學(xué)計算機科學(xué)與技術(shù)學(xué)院研究生，研究方向：進程代數(shù)、計算機科學(xué)中的邏輯學(xué)等。

張晉津（1981－），男，山西曲沃人，博士，講師，研究方向：形式化方式、計算機科學(xué)中的邏輯學(xué)等。

作者簡介：

基金項目：國家自然科學(xué)基金11426136，60973045；江蘇省高校自然科學(xué)基金13KJB520012。