黃 振 華

(南京航空航天大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院　江蘇 南京 210016)

?

Institution框架下的結(jié)構(gòu)化標(biāo)記共變-逆變模擬

黃 振 華

(南京航空航天大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院江蘇 南京 210016)

摘要結(jié)構(gòu)化標(biāo)記共變-逆變模擬是共變-逆變模擬的一種擴(kuò)充，在處理轉(zhuǎn)換系統(tǒng)的模擬關(guān)系時(shí)考慮了標(biāo)記本身的結(jié)構(gòu)。結(jié)構(gòu)化標(biāo)記模態(tài)轉(zhuǎn)換系統(tǒng)間的模態(tài)精化與結(jié)構(gòu)化標(biāo)記共變-逆變模擬之間存在諸多相似之處，為了在更抽象層次上研究?jī)烧叩年P(guān)系，引入Institution框架?；谠摽蚣?，討論結(jié)構(gòu)化標(biāo)記模態(tài)轉(zhuǎn)換系統(tǒng)間的模態(tài)精化與結(jié)構(gòu)化標(biāo)記共變-逆變模擬之間的關(guān)系，并證明前者到后者存在Institution態(tài)射。結(jié)果表明，相比結(jié)構(gòu)化標(biāo)記模態(tài)轉(zhuǎn)換系統(tǒng)中模態(tài)精化關(guān)系，結(jié)構(gòu)化標(biāo)記共變-逆變模擬具有更強(qiáng)的表達(dá)能力。

關(guān)鍵詞Institution結(jié)構(gòu)化標(biāo)記模態(tài)轉(zhuǎn)換系統(tǒng)共變-逆變模擬

LABEL-STRUCTURED COVARIANT-CONTRAVARIANT SIMULATION IN INSTITUTION FRAMEWORK

Huang Zhenhua

(School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,Jiangsu,China)

AbstractThe label-structured covariant-contravariant simulation is an expansion of covariant-contravariant simulation,which considers the structure of labels themselves in dealing with the simulation relation of transition systems. There are many similarities between the modal refinement in label-structured modal transition systems and the label-structured covariant-contravariant simulation. In order to gain more insight into the relationship between them at a more abstract level,the Institutions framework is introduced. Based on that framework,we discuss the relationship between modal refinement in label-structured modal transition systems and label-structured covariant-contravariant simulation,and prove that there exists an Institution morphism from the former to the latter. This result indicate that label-structured covariant-contravariant simulation is more expressive than modal refinement relationship in label-structured modal transition systems.

KeywordsInstitutionLabel-structuredModal transition systemCovariant-contravariant simulation

0引言

在進(jìn)程代數(shù)研究領(lǐng)域，轉(zhuǎn)換系統(tǒng)作為重要的語(yǔ)義模型應(yīng)用廣泛，其中最常見的是帶標(biāo)記的轉(zhuǎn)換系統(tǒng)LTS(Label Transition System)[1]，它可用于描述一般的并發(fā)系統(tǒng)的行為。模態(tài)轉(zhuǎn)換系統(tǒng)MTS(Modal Transition System)[2，3]本質(zhì)上是一種LTS，其將轉(zhuǎn)換分成了兩種類型：可能轉(zhuǎn)換和必然轉(zhuǎn)換。實(shí)際上，一般的LTS也可以看作是可能轉(zhuǎn)換與必然轉(zhuǎn)換一致的MTS。不少的研究擴(kuò)充了MTS概念，文獻(xiàn)[4]介紹了幾種定量模態(tài)轉(zhuǎn)換系統(tǒng)(Quantitative MTS)、時(shí)序模態(tài)轉(zhuǎn)換系統(tǒng)(Timing MTS)、加權(quán)模態(tài)轉(zhuǎn)換系統(tǒng)(Weighted MTS)和概率模態(tài)轉(zhuǎn)換系統(tǒng)(Probabilistic MTS)等。這些MTS的最大特點(diǎn)在于，轉(zhuǎn)化標(biāo)記上附加了定量信息。最近，Bauer等人提出結(jié)構(gòu)化標(biāo)記模態(tài)轉(zhuǎn)換系統(tǒng)LSMTS(Label-Structured MTS)[5，6]，對(duì)帶有定量信息的MTS進(jìn)行了一般性研究。

Fábregas等人提出了LTS之間的共變-逆變模擬[7，8]，其將動(dòng)作集劃分為共變動(dòng)作集、逆變動(dòng)作集與互變動(dòng)作集，并將模態(tài)邏輯語(yǔ)言 HML與動(dòng)作的類型聯(lián)系在一起，建立了共變-逆變模擬的模態(tài)邏輯特征。采用共變-逆變模擬考查精化關(guān)系時(shí)，對(duì)于不同的動(dòng)作集，在模擬關(guān)系中的處理方式也不一樣?；诠沧?逆變模擬的LTS與基于模態(tài)精化的MTS之間存在諸多相似之處，Aceto等人對(duì)兩者之間的聯(lián)系做了討論[9，10]，并給出了它們之間的相互轉(zhuǎn)換關(guān)系。

然而，基于共變-逆變模擬的LTS并未考慮標(biāo)記自身所帶有的結(jié)構(gòu)，因此，本文引入了結(jié)構(gòu)化標(biāo)記轉(zhuǎn)換系統(tǒng)LSTS(Label- Structured Transition System)和結(jié)構(gòu)化標(biāo)記共變-逆變模擬LSCCS(Label-Structured Covariant-Contravariant Simulation)，并在Institution框架下討論了LSMTS與LSCCS之間的聯(lián)系。

1Institution與Institution態(tài)射

在計(jì)算機(jī)理論和數(shù)理邏輯的研究中，由于處理的問(wèn)題不同，通常所采用的邏輯系統(tǒng)也不一樣。常見的邏輯系統(tǒng)包括一階邏輯、高階邏輯、Horn子句、類型論、等式邏輯、時(shí)序邏輯、模態(tài)邏輯和無(wú)窮邏輯等。目前尚且沒(méi)有哪一種邏輯系統(tǒng)適用于所有問(wèn)題。然而，一個(gè)十分自然的問(wèn)題是：能否建立一個(gè)一般性的框架，用來(lái)刻畫從一個(gè)邏輯系統(tǒng)到另一個(gè)邏輯系統(tǒng)的轉(zhuǎn)換，并描述各種邏輯系統(tǒng)之間的關(guān)系。基于這種考慮，Goguen和Burstall提出了Institution和Institution態(tài)射[10]。Institution為不同的形式系統(tǒng)提供了一個(gè)統(tǒng)一的組織方式，一階邏輯、等式邏輯、命題邏輯、三值一階邏輯和函數(shù)式程序邏輯等已經(jīng)被證明是Institution[15]。

對(duì)于一個(gè)邏輯系統(tǒng)而言，其Institution包括四個(gè)基本組成部分：符號(hào)集、代數(shù)(或模型)、邏輯語(yǔ)句以及該模型和語(yǔ)句之間的滿足關(guān)系。與經(jīng)典邏輯系統(tǒng)和模型論相比，Institution框架側(cè)重于考查由符號(hào)集的改變而帶來(lái)的影響。在建立軟件規(guī)范和設(shè)計(jì)軟件系統(tǒng)的過(guò)程中，有些情況下需要考慮從一個(gè)符號(hào)集轉(zhuǎn)變到另一個(gè)符號(hào)集，這一過(guò)程就是所謂的符號(hào)態(tài)射。典型的符號(hào)態(tài)射包括符號(hào)重命名、添加一些符號(hào)或?qū)⒁恍┓?hào)變?yōu)閮H內(nèi)部可見等，任何的符號(hào)態(tài)射均會(huì)引起模型和語(yǔ)句發(fā)生相應(yīng)的變化。直觀上，語(yǔ)法(符號(hào)、語(yǔ)句)和語(yǔ)義(模型)的轉(zhuǎn)換方向是正好相反，不僅如此，兩者變化過(guò)程中還必須保持其滿足關(guān)系不發(fā)生改變，即：可滿足關(guān)系不隨符號(hào)的改變而發(fā)生改變，這是一個(gè)邏輯系統(tǒng)滿足Institution的重要條件。

下面將介紹Institution與Institution態(tài)射等基本概念，更詳盡的介紹可參考文獻(xiàn)[12-14]。本文假定讀者熟知范疇、函子和自然變換等范疇論基本概念。本文所采用的記號(hào)與Mac Lane所著的[16]相一致。在下文中，Set表示集合范疇，Cat表示范疇的范疇，|C|表示范疇C中對(duì)象的集合。

定義1[10]Institution是一個(gè)四元組(Sign,Sen,Mod,)，其中，Sign是一個(gè)范疇，其對(duì)象稱為符號(hào)集；Sen:Sign→Set是一個(gè)函子，將符號(hào)集Σ映射到一個(gè)Σ-語(yǔ)句集Sen(Σ)；Mod:Sign→Catop是一個(gè)函子，其將符號(hào)集Σ映射到Σ-模型與Σ-模型態(tài)射組成的范疇Mod(Σ)；表示集合{Σ|Σ∈|Sign|}，其中Σ?|Mod(Σ)|×Sen(Σ)，稱作Σ-滿足關(guān)系。對(duì)于Sign中任意態(tài)射f:Σ→Σ′，M′∈|Mod(Σ′)|和φ∈Sen(Σ)，如下條件成立：

M′Σ′Sen(f)(φ)?Mod(f)(M′)Σφ。

Institution僅能描述一個(gè)邏輯系統(tǒng)的基本要素，要刻畫從一個(gè)邏輯系統(tǒng)到另一個(gè)邏輯系統(tǒng)的轉(zhuǎn)換，就需要引入Institution之間的態(tài)射。從一個(gè)Institution到另一個(gè)Institution的態(tài)射有多種不同的定義方式，其中Institution態(tài)射和Institution余態(tài)射是最常見的兩種[2]。前者適用于從一個(gè)復(fù)雜的Institution映射到一個(gè)相對(duì)簡(jiǎn)單的Institution，而后者通常與前者相反。本文僅涉及Institution態(tài)射。

定義2[11]給定Institution=(Sign,Sen,Mod,)和′=(Sign′,Sen′,Mod′,′)，從到′的Institution 態(tài)射包括三部分：函子Φ:Sign→Sign′、自然變換β:Mod?Mod′°Φ和自然變換α:Sen′°Φ?Sen。并且，對(duì)于任意Σ∈|Sign|、M∈|Mod(Σ)|和φ∈Sen′(Φ(Σ))，如下條件成立：

MΣαΣ(φ′)?βΣ(M)。

2LSMTS和LSCCS

本節(jié)首先介紹標(biāo)記集及其相關(guān)性質(zhì)，在此基礎(chǔ)上，介紹結(jié)構(gòu)化標(biāo)記模態(tài)轉(zhuǎn)換系統(tǒng)(LSMTS)及其模態(tài)精化，并給出了幾個(gè)例子。然后，將標(biāo)記集運(yùn)用到標(biāo)記轉(zhuǎn)換系統(tǒng)中，引入結(jié)構(gòu)化標(biāo)記轉(zhuǎn)換系統(tǒng)，并將共變-逆變模擬[6]進(jìn)行擴(kuò)充，引入結(jié)構(gòu)化標(biāo)記共變-逆變模擬(LSCCS)。最后，給出了一個(gè)從LSMTS到LSCCS的轉(zhuǎn)換。

下文將使用圖來(lái)表示LSMTS，并約定虛線表示可能轉(zhuǎn)換，實(shí)線表示必然轉(zhuǎn)換，如果兩個(gè)狀態(tài)之間同時(shí)存在必然轉(zhuǎn)換和可能轉(zhuǎn)換且標(biāo)記相同，則僅畫出必然轉(zhuǎn)換。下文中例1—例3均源自于文獻(xiàn)[5]。

圖1　一個(gè)平凡的LSMTS

在經(jīng)典的模態(tài)轉(zhuǎn)換系統(tǒng)中，模態(tài)精化過(guò)程就是去除一些可能轉(zhuǎn)換和(或)將一些可能轉(zhuǎn)換轉(zhuǎn)變?yōu)楸厝晦D(zhuǎn)換的過(guò)程；而在LSMTS中，模態(tài)精化還需要考慮標(biāo)記本身的精化關(guān)系。

圖2　自動(dòng)售貨機(jī)LSMTS

圖3　加權(quán)模態(tài)自動(dòng)機(jī)

LTS可以看作是可能轉(zhuǎn)換與必然轉(zhuǎn)換一致的MTS，是進(jìn)程代數(shù)研究中最重要的語(yǔ)義模型之一，可以描述并發(fā)系統(tǒng)的行為。下面回顧一下LTS中的共變-逆變模擬[5，6]。共變-逆變模擬將動(dòng)作集劃分成三塊，即共變動(dòng)作集、逆變動(dòng)作集和互變動(dòng)作集，對(duì)于不同的動(dòng)作集，在模擬關(guān)系中的處理方式不一樣。

定義6[5]令P和Q是動(dòng)作集A上的兩個(gè)LTS，初始狀態(tài)分別為p0和q0，{Ar,Al,Abi}是A上的一個(gè)劃分(其中Ar，Al，Abi允許為空集)。R?P×Q是P和Q之間的共變-逆變模擬關(guān)系當(dāng)且僅當(dāng)(p0,q0)∈R且對(duì)于任意的(p,q)∈R，如下條件成立：

采用共變-逆變模擬考查精化關(guān)系時(shí)，規(guī)范中共變動(dòng)作所標(biāo)記的轉(zhuǎn)換必須在實(shí)現(xiàn)中被模擬；實(shí)現(xiàn)中逆變動(dòng)作所標(biāo)記的轉(zhuǎn)換必須在規(guī)范中被允許；而互變動(dòng)作所標(biāo)記的轉(zhuǎn)換必須滿足互模擬中的向前向后條件。本文將上述概念按如下方式推廣到LSTS上。

圖4　自動(dòng)售貨機(jī)LSCCS

文獻(xiàn)[5]給出了基于模態(tài)精化的MTS與基于共變-逆變模擬的LTS之間的相互轉(zhuǎn)換關(guān)系，在這種轉(zhuǎn)換下，轉(zhuǎn)換之前與轉(zhuǎn)換之后的系統(tǒng)性質(zhì)是保持的。與之類似，下面給出一個(gè)從LSMTS到LSCCS的轉(zhuǎn)換C。

{<⊥′,k>|k∈Kr∪Kl∪{⊥′}}。

根據(jù)LSMTS和LSCCS的定義及如上的轉(zhuǎn)換C，有如下性質(zhì)成立。

定理1R?P×Q是LSMTS P和Q之間的模態(tài)精化關(guān)系，當(dāng)且僅當(dāng)R-1是C(Q)和C(P)之間的結(jié)構(gòu)化標(biāo)記共變-逆變關(guān)系。

3Institution框架下的LSMTS和LSCCS

本節(jié)將在Institution框架下討論LSMTS與LSCCS之間的關(guān)系，并證明前者到后者存在Institution態(tài)射。

(1) f(K)=K′；

φ::=tt|ff|φ1∧φ2|φ1∨φ2|ψ|[k]ψ，其中k∈K{⊥}；

-Modmts(f)(M,m)與(M,m)的狀態(tài)集相同，且初始狀態(tài)相同；

-Modmts(f)(H)=H。

證明容易驗(yàn)證，Signmts是范疇，Modmts和Senmts是函子。所以，為證明mts是一個(gè)Institution，只需對(duì)Signmts中的態(tài)射f:(K,)→(K′,′)，(M′,s)∈|Modmts(K′,′)|和φ∈Senmts(K,)，證明如下條件成立即可：

按照公式φ的結(jié)構(gòu)復(fù)雜度歸納證明，對(duì)于φ=tt、φ=ff、φ=φ1∧φ2和φ=φ1∧φ2這些情形，結(jié)論很容易證明，證明過(guò)程略。接下來(lái)考慮公式φ中含有模態(tài)詞的情形。

情形1φ=ψ。

(?)假設(shè)(M′,s)mtsSenmts(f)(ψ)，根據(jù)Senmts(f)的定義，(M′,s)mtsSenmts(f)(ψ)；由mts的定義可知，(M′,s)中存在，使得[l′]?[f(k)]且(M′,p)mtsSenmts(f)(ψ)；因?yàn)椤渚哂型陚湫?，所以，再根?jù)函數(shù)f:K→K′滿足的條件可知，K中一定存在l使得f(l)=l′且lk，所以，(M′,s)中存在，使得lk且(M′,p)mtsSenmts(f)(ψ)；根據(jù)Modmts(f)的定義和的可靠性，由歸納假設(shè)可得，Modmts(f)(M′,s)中存在，使得[l]?[k]且Modmts(f)(M′,p)mtsψ；最后，根據(jù)mts的定義可得，Modmts(f)(M′,s)mtsψ。

(?) 假設(shè)Modmts(f)(M′,s)mtsψ，根據(jù)mts的定義，Modmts(f)(M′,s)中存在，使得[l]?[k]且Modmts(f)(M′,p)mtsψ；因?yàn)榫哂型陚湫?，所以lk，根據(jù)函數(shù)f:K→K′滿足條件可知，f(l)′f(k)，因此[f(l)]?[f(k)]；根據(jù)Modmts(f)的定義，由歸納假設(shè)可得，(M′,s)中存在，使得[f(l)]?[f(k)]且(M′,p)mtsSenmts(f)(ψ)；根據(jù)mts的定義，(M′,s)mtsSenmts(f)(ψ)；最后，根據(jù)Senmts(f)的定義可得，(M′,s)mtsSenmts(f)(ψ)。

情形2φ=[k]ψ。

(?) 假設(shè)Modmts(f)(M′,s)mts[k]ψ；根據(jù)mts的定義，對(duì)于Modmts(f)(M′,s)中任意滿足[k]?[l]的，均有Modmts(f)(M′,p)mtsψ；因?yàn)榫哂型陚湫?，所以kl，根據(jù)函數(shù)f:K→K′滿足條件可知，f(k)′f(l)，因此[f(k)]?[f(l)]；根據(jù)Modmts(f)的定義，由歸納假設(shè)可得，對(duì)于(M′,s)中任意滿足[f(k)]?[f(l)]的，均有(M′,p)mtsSenmts(f)(ψ)；根據(jù)mts的定義，(M′,s)mts[f(k)]Senmts(f)(ψ)；最后，根據(jù)Senmts(f)的定義可得，(M′,s)mtsSenmts(f)([k]ψ)。

φ::=tt|ff|φ1∧φ2|φ1∨φ2|ψ|[k2]ψ，其中k1∈Kr∪Kbi，k2∈Kl∪Kbi。

-Modcc(f)(M,m)與(M,m)的狀態(tài)集相同，且初始狀態(tài)相同；

-Modcc(f)(H)=H。

-對(duì)于k∈Kr∪Kbi，(M,s)ccψ?存在使得[l]?[k]且(M,s′)ccψ；

類似于LSMTS Institution，本文有如下結(jié)論成立。

定理2與定理3說(shuō)明了定義9與定義10分別給出了LSMTS和LSCCS的Institution，下面將給出從mts到cc的Institution態(tài)射。

-Φ(f)(cv(k))=cv(f(k))；

-Φ(f)(ct(k))=ct(f(k))。

同樣，可按照公式φ的結(jié)構(gòu)復(fù)雜度歸納證明，略。

圖5　α和β的交換圖

4結(jié)語(yǔ)

本文引入了結(jié)構(gòu)化標(biāo)記模態(tài)轉(zhuǎn)換系統(tǒng)間的模態(tài)精化與結(jié)構(gòu)化標(biāo)記共變-逆變模擬，基于Institution框架，討論了兩者之間的聯(lián)系，并證明得出結(jié)構(gòu)化標(biāo)記模態(tài)轉(zhuǎn)換系統(tǒng)間的模態(tài)精化Institution到結(jié)構(gòu)化標(biāo)記共變-逆變模擬Institution存在Institution態(tài)射。結(jié)果表明，構(gòu)化標(biāo)記共變-逆變模擬具有更強(qiáng)的表達(dá)能力和更多應(yīng)用場(chǎng)景，而結(jié)構(gòu)化標(biāo)記模態(tài)轉(zhuǎn)換系統(tǒng)間的模態(tài)精化具有更加直觀的特點(diǎn)，可以做為構(gòu)化標(biāo)記共變-逆變模擬的一種特例進(jìn)行研究。本文從Institution 態(tài)射的角度研究了兩個(gè)系統(tǒng)的特點(diǎn)，然而，能否從Institution 余態(tài)射的角度來(lái)比較兩者之間的聯(lián)系，是一個(gè)值得進(jìn)一步研究的問(wèn)題。

參考文獻(xiàn)

[1] Keller R M. Formal verification of parallel programs[J]. Communications of the ACM,1976,19(7): 371-384.

[2] Larsen K G,Thomsen B. A modal process logic[C] //Logic in Computer Science,1988. LICS’88.,Proceedings of the Third Annual Symposium on. IEEE,1988: 203-210.

[3] Larsen K G. Modal specifications[C]//Automatic Verification Methods for Finite State Systems. Springer Berlin Heidelberg,1990: 232-246.

[4] Larsen K G,Legay A. Quantitative Modal Transition Systems[M]//Recent Trends in Algebraic Development Techniques. Springer Berlin Heidelberg,2013.

[5] Bauer S S,Juhl L,Larsen K G,et al. Extending modal transition systems with structured labels[J]. Mathematical Structures in Computer Science,2012,22(4): 581-617.

[6] Bauer S S,Fahrenberg U,Juhl L,et al. Weighted modal transition systems[J]. Formal Methods in System Design,2013,42(2): 193-220.

[7] Fábregas I,de Frutos Escrig D,Palomino M. Non-strongly stable orders also define interesting simulation relations[M]//Algebraand Coalgebra in Computer Science. Springer Berlin Heidelberg,2009: 221-235.

[8] Fábregas I,de Frutos Escrig D,Palomino M. Logics for contravariant simulations[M]//Formal Techniques for Distributed Systems. Springer Berlin Heidelberg,2010: 224-231.

[9] Aceto L,Fábregas I,de Frutos-Escrig D,et al. On the specification of modal systems: A comparison of three frameworks[J]. Science of Computer Programming,2013,78(12): 2468-2487.

[10] Aceto L,Fábregas I,de Frutos Escrig D,et al. Relating modal refinements,covariant-contravariant simulations and partial bisimulations[M] //Fundamentals of Software Engineering. Springer Berlin Heidelberg,2012: 268-283.

[12] Goguen J A,Burstall R M. Institutions: Abstract model theory for specification and programming[J]. Journal of the ACM (JACM),1992,39(1): 95-146.

[13] Goguen J,Ro?u G. Institution morphisms[J]. Formal Aspects of Computing,2002,13(3-5): 274-307.

[14] Diaconescu R. Institution-independent model theory[M]. Springer,2008.

[15] Sannella D,Tarlecki A.Foundations of algebraic specification and formal software development[M].Springer,2012.

[16] Mac Lane S.Categories for the working mathematician[M].Springer,1998.

[17] Milner R.Communication and concurrency[M].Prentice-Hall,Inc.,1989.

中圖分類號(hào)TP301.2

文獻(xiàn)標(biāo)識(shí)碼A

DOI:10.3969/j.issn.1000-386x.2016.02.047

收稿日期：2014-09-05。國(guó)家自然科學(xué)基金項(xiàng)目(60973045)。黃振華，碩士生，主研領(lǐng)域：進(jìn)程代數(shù)。