黃 振 華

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

?

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

黃 振 華

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

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

關(guān)鍵詞Institution結(jié)構(gòu)化標記模態(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引言

在進程代數(shù)研究領(lǐng)域，轉(zhuǎn)換系統(tǒng)作為重要的語義模型應(yīng)用廣泛，其中最常見的是帶標記的轉(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)換。實際上，一般的LTS也可以看作是可能轉(zhuǎn)換與必然轉(zhuǎn)換一致的MTS。不少的研究擴充了MTS概念，文獻[4]介紹了幾種定量模態(tài)轉(zhuǎn)換系統(tǒng)(Quantitative MTS)、時序模態(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的最大特點在于，轉(zhuǎn)化標記上附加了定量信息。最近，Bauer等人提出結(jié)構(gòu)化標記模態(tài)轉(zhuǎn)換系統(tǒng)LSMTS(Label-Structured MTS)[5，6]，對帶有定量信息的MTS進行了一般性研究。

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

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

1Institution與Institution態(tài)射

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

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

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

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

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

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

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

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

2LSMTS和LSCCS

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

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

圖1　一個平凡的LSMTS

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

圖2　自動售貨機LSMTS

圖3　加權(quán)模態(tài)自動機

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

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

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

圖4　自動售貨機LSCCS

文獻[5]給出了基于模態(tài)精化的MTS與基于共變-逆變模擬的LTS之間的相互轉(zhuǎn)換關(guān)系，在這種轉(zhuǎn)換下，轉(zhuǎn)換之前與轉(zhuǎn)換之后的系統(tǒng)性質(zhì)是保持的。與之類似，下面給出一個從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)系，當且僅當R-1是C(Q)和C(P)之間的結(jié)構(gòu)化標記共變-逆變關(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。

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

按照公式φ的結(jié)構(gòu)復(fù)雜度歸納證明，對于φ=tt、φ=ff、φ=φ1∧φ2和φ=φ1∧φ2這些情形，結(jié)論很容易證明，證明過程略。接下來考慮公式φ中含有模態(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)(ψ)；因為′具有完備性，所以，再根據(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ψ；因為具有完備性，所以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的定義，對于Modmts(f)(M′,s)中任意滿足[k]?[l]的，均有Modmts(f)(M′,p)mtsψ；因為具有完備性，所以kl，根據(jù)函數(shù)f:K→K′滿足條件可知，f(k)′f(l)，因此[f(k)]?[f(l)]；根據(jù)Modmts(f)的定義，由歸納假設(shè)可得，對于(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。

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

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

定理2與定理3說明了定義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é)語

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

中圖分類號TP301.2

文獻標識碼A

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

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