CLT樹(shù)型指稱語(yǔ)義的研究

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

?

CLT樹(shù)型指稱語(yǔ)義的研究

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

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

【關(guān)鍵詞】進(jìn)程代數(shù)；并發(fā)行為；must-testing語(yǔ)義；指稱語(yǔ)義；標(biāo)準(zhǔ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]。近幾年，Barbanera, Liguoro, Castagna等人提出面向網(wǎng)絡(luò)服務(wù)器的必須測(cè)試?yán)碚揫2]，Bernardi和Hennessy提出了面向網(wǎng)絡(luò)服務(wù)器的CLT語(yǔ)義以及SVR語(yǔ)義用于描述精化關(guān)系[3]。它介紹了兩種子行為關(guān)系:服務(wù)器（server）和客戶(client)，并描述了它們之間的相互作用。在進(jìn)程代數(shù)理論中指稱語(yǔ)義[4]是一個(gè)與操作語(yǔ)義[5]類似地描述，而文獻(xiàn)[3]在處理CLT語(yǔ)義時(shí)對(duì)此并未涉及。本文基于Hennessy等人提出的CLT語(yǔ)義，將通過(guò)建立進(jìn)程的標(biāo)準(zhǔn)型，研究與此語(yǔ)義具有完全抽象性的樹(shù)形指稱語(yǔ)義。

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

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

定義1[3]CLT的項(xiàng)（進(jìn)程）由BNF范式定義如下：

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

則稱

則稱Д是S-set。

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

證明：參考文獻(xiàn)[6]引理2.33。

2 有限接收樹(shù)集（FAT）

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

2.1 FAT的基本概念

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

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

R1 對(duì)任意的動(dòng)作a，樹(shù)中任意節(jié)點(diǎn)最多只有一個(gè)標(biāo)記為a的后繼分支。

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

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

2.2 FAT上的指稱

接下來(lái)我們介紹進(jìn)程是如何指稱到FAT中的。給定樹(shù)t? FAT，L（t）表示樹(shù)t的所有節(jié)點(diǎn)組成的集合，或者說(shuō)樹(shù)t通過(guò)的路徑的集合。我們給出CLT的各個(gè)算子在FAT中的指稱。

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

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

他們表示同一顆樹(shù)，該樹(shù)只有一個(gè)節(jié)點(diǎn)，沒(méi)有分支并且滿足如下要求：

（2）1FAT

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

（3）aFAT.

（4）+FAT

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

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

3 完全抽象性

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

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

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

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

3.2 完全抽象性

證明 參考文獻(xiàn)[3]定理7.10。

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

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

證明 對(duì)p分情形討論納易證。

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

證明 由前面分析易證。

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

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

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

參考文獻(xiàn)

[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é)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院研究生，研究方向：進(jìn)程代數(shù)、計(jì)算機(jī)科學(xué)中的邏輯學(xué)等。

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

作者簡(jiǎn)介：

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