Institution框架下的结构化标记共变-逆变模拟

2016-03-17黄振华

计算机应用与软件 2016年2期

关键词：精化结构化框架

黄振华

(南京航空航天大学计算机科学与技术学院　江苏南京 210016)

Institution框架下的结构化标记共变-逆变模拟

黄振华

(南京航空航天大学计算机科学与技术学院江苏南京 210016)

摘要结构化标记共变-逆变模拟是共变-逆变模拟的一种扩充，在处理转换系统的模拟关系时考虑了标记本身的结构。结构化标记模态转换系统间的模态精化与结构化标记共变-逆变模拟之间存在诸多相似之处，为了在更抽象层次上研究两者的关系，引入Institution框架。基于该框架，讨论结构化标记模态转换系统间的模态精化与结构化标记共变-逆变模拟之间的关系，并证明前者到后者存在Institution态射。结果表明，相比结构化标记模态转换系统中模态精化关系，结构化标记共变-逆变模拟具有更强的表达能力。

关键词Institution结构化标记模态转换系统共变-逆变模拟

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引言

在进程代数研究领域，转换系统作为重要的语义模型应用广泛，其中最常见的是带标记的转换系统LTS(Label Transition System)[1]，它可用于描述一般的并发系统的行为。模态转换系统MTS(Modal Transition System)[2，3]本质上是一种LTS，其将转换分成了两种类型：可能转换和必然转换。实际上，一般的LTS也可以看作是可能转换与必然转换一致的MTS。不少的研究扩充了MTS概念，文献[4]介绍了几种定量模态转换系统(Quantitative MTS)、时序模态转换系统(Timing MTS)、加权模态转换系统(Weighted MTS)和概率模态转换系统(Probabilistic MTS)等。这些MTS的最大特点在于，转化标记上附加了定量信息。最近，Bauer等人提出结构化标记模态转换系统LSMTS(Label-Structured MTS)[5，6]，对带有定量信息的MTS进行了一般性研究。

Fábregas等人提出了LTS之间的共变-逆变模拟[7，8]，其将动作集划分为共变动作集、逆变动作集与互变动作集，并将模态逻辑语言 HML与动作的类型联系在一起，建立了共变-逆变模拟的模态逻辑特征。采用共变-逆变模拟考查精化关系时，对于不同的动作集，在模拟关系中的处理方式也不一样。基于共变-逆变模拟的LTS与基于模态精化的MTS之间存在诸多相似之处，Aceto等人对两者之间的联系做了讨论[9，10]，并给出了它们之间的相互转换关系。

然而，基于共变-逆变模拟的LTS并未考虑标记自身所带有的结构，因此，本文引入了结构化标记转换系统LSTS(Label- Structured Transition System)和结构化标记共变-逆变模拟LSCCS(Label-Structured Covariant-Contravariant Simulation)，并在Institution框架下讨论了LSMTS与LSCCS之间的联系。

1Institution与Institution态射

在计算机理论和数理逻辑的研究中，由于处理的问题不同，通常所采用的逻辑系统也不一样。常见的逻辑系统包括一阶逻辑、高阶逻辑、Horn子句、类型论、等式逻辑、时序逻辑、模态逻辑和无穷逻辑等。目前尚且没有哪一种逻辑系统适用于所有问题。然而，一个十分自然的问题是：能否建立一个一般性的框架，用来刻画从一个逻辑系统到另一个逻辑系统的转换，并描述各种逻辑系统之间的关系。基于这种考虑，Goguen和Burstall提出了Institution和Institution态射[10]。Institution为不同的形式系统提供了一个统一的组织方式，一阶逻辑、等式逻辑、命题逻辑、三值一阶逻辑和函数式程序逻辑等已经被证明是Institution[15]。

对于一个逻辑系统而言，其Institution包括四个基本组成部分：符号集、代数(或模型)、逻辑语句以及该模型和语句之间的满足关系。与经典逻辑系统和模型论相比，Institution框架侧重于考查由符号集的改变而带来的影响。在建立软件规范和设计软件系统的过程中，有些情况下需要考虑从一个符号集转变到另一个符号集，这一过程就是所谓的符号态射。典型的符号态射包括符号重命名、添加一些符号或将一些符号变为仅内部可见等，任何的符号态射均会引起模型和语句发生相应的变化。直观上，语法(符号、语句)和语义(模型)的转换方向是正好相反，不仅如此，两者变化过程中还必须保持其满足关系不发生改变，即：可满足关系不随符号的改变而发生改变，这是一个逻辑系统满足Institution的重要条件。

下面将介绍Institution与Institution态射等基本概念，更详尽的介绍可参考文献[12-14]。本文假定读者熟知范畴、函子和自然变换等范畴论基本概念。本文所采用的记号与Mac Lane所著的[16]相一致。在下文中，Set表示集合范畴，Cat表示范畴的范畴，|C|表示范畴C中对象的集合。

定义1[10]Institution是一个四元组(Sign,Sen,Mod,)，其中，Sign是一个范畴，其对象称为符号集；Sen:Sign→Set是一个函子，将符号集Σ映射到一个Σ-语句集Sen(Σ)；Mod:Sign→Catop是一个函子，其将符号集Σ映射到Σ-模型与Σ-模型态射组成的范畴Mod(Σ)；表示集合{Σ|Σ∈|Sign|}，其中Σ⊆|Mod(Σ)|×Sen(Σ)，称作Σ-满足关系。对于Sign中任意态射f:Σ→Σ′，M′∈|Mod(Σ′)|和φ∈Sen(Σ)，如下条件成立：

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

Institution仅能描述一个逻辑系统的基本要素，要刻画从一个逻辑系统到另一个逻辑系统的转换，就需要引入Institution之间的态射。从一个Institution到另一个Institution的态射有多种不同的定义方式，其中Institution态射和Institution余态射是最常见的两种[2]。前者适用于从一个复杂的Institution映射到一个相对简单的Institution，而后者通常与前者相反。本文仅涉及Institution态射。

定义2[11]给定Institution=(Sign,Sen,Mod,)和′=(Sign′,Sen′,Mod′,′)，从到′的Institution 态射包括三部分：函子Φ:Sign→Sign′、自然变换β:Mod⟹Mod′°Φ和自然变换α:Sen′°Φ⟹Sen。并且，对于任意Σ∈|Sign|、M∈|Mod(Σ)|和φ∈Sen′(Φ(Σ))，如下条件成立：

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

2LSMTS和LSCCS

本节首先介绍标记集及其相关性质，在此基础上，介绍结构化标记模态转换系统(LSMTS)及其模态精化，并给出了几个例子。然后，将标记集运用到标记转换系统中，引入结构化标记转换系统，并将共变-逆变模拟[6]进行扩充，引入结构化标记共变-逆变模拟(LSCCS)。最后，给出了一个从LSMTS到LSCCS的转换。

下文将使用图来表示LSMTS，并约定虚线表示可能转换，实线表示必然转换，如果两个状态之间同时存在必然转换和可能转换且标记相同，则仅画出必然转换。下文中例1—例3均源自于文献[5]。

图1　一个平凡的LSMTS

在经典的模态转换系统中，模态精化过程就是去除一些可能转换和(或)将一些可能转换转变为必然转换的过程；而在LSMTS中，模态精化还需要考虑标记本身的精化关系。

图2　自动售货机LSMTS

图3　加权模态自动机

LTS可以看作是可能转换与必然转换一致的MTS，是进程代数研究中最重要的语义模型之一，可以描述并发系统的行为。下面回顾一下LTS中的共变-逆变模拟[5，6]。共变-逆变模拟将动作集划分成三块，即共变动作集、逆变动作集和互变动作集，对于不同的动作集，在模拟关系中的处理方式不一样。

定义6[5]令P和Q是动作集A上的两个LTS，初始状态分别为p0和q0，{Ar,Al,Abi}是A上的一个划分(其中Ar，Al，Abi允许为空集)。R⊆P×Q是P和Q之间的共变-逆变模拟关系当且仅当(p0,q0)∈R且对于任意的(p,q)∈R，如下条件成立：

采用共变-逆变模拟考查精化关系时，规范中共变动作所标记的转换必须在实现中被模拟；实现中逆变动作所标记的转换必须在规范中被允许；而互变动作所标记的转换必须满足互模拟中的向前向后条件。本文将上述概念按如下方式推广到LSTS上。

图4　自动售货机LSCCS

文献[5]给出了基于模态精化的MTS与基于共变-逆变模拟的LTS之间的相互转换关系，在这种转换下，转换之前与转换之后的系统性质是保持的。与之类似，下面给出一个从LSMTS到LSCCS的转换C。

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

根据LSMTS和LSCCS的定义及如上的转换C，有如下性质成立。

定理1R⊆P×Q是LSMTS P和Q之间的模态精化关系，当且仅当R-1是C(Q)和C(P)之间的结构化标记共变-逆变关系。

3Institution框架下的LSMTS和LSCCS

本节将在Institution框架下讨论LSMTS与LSCCS之间的关系，并证明前者到后者存在Institution态射。

(1) f(K)=K′；

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

-Modmts(f)(M,m)与(M,m)的状态集相同，且初始状态相同；

-Modmts(f)(H)=H。

证明容易验证，Signmts是范畴，Modmts和Senmts是函子。所以，为证明mts是一个Institution，只需对Signmts中的态射f:(K,)→(K′,′)，(M′,s)∈|Modmts(K′,′)|和φ∈Senmts(K,)，证明如下条件成立即可：

按照公式φ的结构复杂度归纳证明，对于φ=tt、φ=ff、φ=φ1∧φ2和φ=φ1∧φ2这些情形，结论很容易证明，证明过程略。接下来考虑公式φ中含有模态词的情形。

情形1φ=ψ。

(⟹)假设(M′,s)mtsSenmts(f)(ψ)，根据Senmts(f)的定义，(M′,s)mtsSenmts(f)(ψ)；由mts的定义可知，(M′,s)中存在，使得[l′]⊆[f(k)]且(M′,p)mtsSenmts(f)(ψ)；因为′具有完备性，所以，再根据函数f:K→K′满足的条件可知，K中一定存在l使得f(l)=l′且lk，所以，(M′,s)中存在，使得lk且(M′,p)mtsSenmts(f)(ψ)；根据Modmts(f)的定义和的可靠性，由归纳假设可得，Modmts(f)(M′,s)中存在，使得[l]⊆[k]且Modmts(f)(M′,p)mtsψ；最后，根据mts的定义可得，Modmts(f)(M′,s)mtsψ。

(⟸) 假设Modmts(f)(M′,s)mtsψ，根据mts的定义，Modmts(f)(M′,s)中存在，使得[l]⊆[k]且Modmts(f)(M′,p)mtsψ；因为具有完备性，所以lk，根据函数f:K→K′满足条件可知，f(l)′f(k)，因此[f(l)]⊆[f(k)]；根据Modmts(f)的定义，由归纳假设可得，(M′,s)中存在，使得[f(l)]⊆[f(k)]且(M′,p)mtsSenmts(f)(ψ)；根据mts的定义，(M′,s)mtsSenmts(f)(ψ)；最后，根据Senmts(f)的定义可得，(M′,s)mtsSenmts(f)(ψ)。

情形2φ=[k]ψ。

(⟸) 假设Modmts(f)(M′,s)mts[k]ψ；根据mts的定义，对于Modmts(f)(M′,s)中任意满足[k]⊆[l]的，均有Modmts(f)(M′,p)mtsψ；因为具有完备性，所以kl，根据函数f:K→K′满足条件可知，f(k)′f(l)，因此[f(k)]⊆[f(l)]；根据Modmts(f)的定义，由归纳假设可得，对于(M′,s)中任意满足[f(k)]⊆[f(l)]的，均有(M′,p)mtsSenmts(f)(ψ)；根据mts的定义，(M′,s)mts[f(k)]Senmts(f)(ψ)；最后，根据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)的状态集相同，且初始状态相同；

-Modcc(f)(H)=H。

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

类似于LSMTS Institution，本文有如下结论成立。

定理2与定理3说明了定义9与定义10分别给出了LSMTS和LSCCS的Institution，下面将给出从mts到cc的Institution态射。

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

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

同样，可按照公式φ的结构复杂度归纳证明，略。

图5　α和β的交换图

4结语

本文引入了结构化标记模态转换系统间的模态精化与结构化标记共变-逆变模拟，基于Institution框架，讨论了两者之间的联系，并证明得出结构化标记模态转换系统间的模态精化Institution到结构化标记共变-逆变模拟Institution存在Institution态射。结果表明，构化标记共变-逆变模拟具有更强的表达能力和更多应用场景，而结构化标记模态转换系统间的模态精化具有更加直观的特点，可以做为构化标记共变-逆变模拟的一种特例进行研究。本文从Institution 态射的角度研究了两个系统的特点，然而，能否从Institution 余态射的角度来比较两者之间的联系，是一个值得进一步研究的问题。

参考文献

[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.