ntyft/ntyxt算子下共变-异变模拟的前同余性
2019-09-28李苏婷
李苏婷，张 严
(1.南京航空航天大学 计算机科学与技术学院，江苏 南京 211106；2.南京林业大学 信息科学技术学院，江苏 南京 210037)
0 引 言
进程代数[1-3]是反应式系统的原型规范语言，它们通过进程项来描述反应式系统的规范及实现，实现是否满足规范则由行为等价或者模拟关系来刻画。经典模拟关系[4]主要针对具有被动行为的反应式系统间精化关系的刻画，它要求规范的被动行为必须被实现模拟。然而，对于具有主动行为的系统(如输入/输出自动机[5-6]中的输出行为)，为了保证实现的安全性，它的输出行为必须是规范所允许的。因此，Fábregas等[7]将动作划分为共变、异变和互变三种类型，对经典(互)模拟概念进行推广[8-9]，提出了共变-异变模拟(covariant-contravariant simulation，CC-模拟)。直观上讲，共变动作表示系统的被动行为，其执行受环境控制，规范中共变动作所标记的转换必须在实现中被模拟；异变行为代表了系统本身控制下的主动行为，实现中异变动作所标记的转换必须在规范中被允许；互变行为的要求反映了经典的互模拟思想。文献[10-12]详述了CC-模拟提出的动机。
众所周知，行为关系的(前)同余性质在支持形式规范的模块化构建和公理系统的推理方面具有重要意义，它的证明需要根据进程代数语言中算子的结构化操作语义(structural operational semantics，SOS)[13]规则逐个开展[1,10,14]。为了避免(前)同余性证明中的重复劳动，学术界提出了多种类型的SOS规则的框架形式，其中ntyft/ntyxt是最具代表性之一。Groote[15]首次给出它的定义，证明了互模拟关系在良基且可分层的转换系统规范(transition system specification，TSS)[16]上的同余性。Fokkink[17]将ntyft/ntyxt形式约简到Ntree形式，论证了上述同余性定理中良基条件的非必要性。Bol等[18]利用分层和归约技术证明了非良基条件下ntyft/ntyxt规则形式的TSS关于互模拟的同余性。借鉴Bol等[18]的方法，文中探讨了CC-模拟在ntyft/ntyxt规则形式的TSS上的前同余性。
1 预备知识
进程代数一般通过一组SOS规则对进程项的行为进行规范。通过这些规则，进程的行为被描述成一个带标记的转换系统[19]，转换系统通常用TSS来描述。本节将介绍一些预备概念。
1.1 TSS及转换模型
令V是可数无限的变元集，用x,y,z等表示其中元素。令Σ为型(signature)，包含了常元0、算子以及算子对应的元数。令Actτ=Act∪{τ}为动作符号集，用a,b,c等表示其中元素，其中τ是系统内部动作，Act为外部动作集。基于Σ上的进程项的BNF范式定义为：P=0|x|f(P1,P2,…,Pl)，其中x∈V且f∈Σ是l元算子。T(Σ)表示基于Σ上的所有进程项的集合，T(Σ)表示所有闭项(不含变元的进程项)的集合，用P,Q等表示进程项。一个(闭)替换σ是V到T(Σ)(T(Σ))的函数，进程项P上的替换(记作Pσ)按常规定义。
不难发现，正TSS的支持模型是唯一存在的且是其最小模型[18](最小模型按常规定义)。但非正的TSS(即其有些规则中含否前提)则不然[18]，分层和归约技术的提出则解决了该问题。
1.2 分层技术
规则只能定义一个转换公式是成立的，但不能定义一个转换公式是不成立的。常用的分层技术确保了所有转换公式的永真性不再依赖于否转换公式，保证了转换模型的唯一性[18]。在转换模型具体性质的证明中，时常依赖稳定模型，定义如下：
定理1[18]：令S=(Σ,R)为一个TSS，转换模型→⊆T(Σ)×Actτ×T(Σ)对S是稳定的，则：
(1)→是S的模型；
(2)→是被S支持的；
(3)→是S最小模型。
定理1将隐式地帮助后续的证明，它反映了对稳定模型的要求的本质即是在寻找最小支持模型。
1.3 归约技术
对于一些不可分层但却具有重要意义的TSS(如带权限的BPAσ∈τ)[18]，归约技术则有用武之地。受良基模型[20]的启发，归约技术将一个TSS的转换模型划分成三部分：肯定为真的转换模型→true、肯定不为真的转换模型和不确定是否为真的转换模型→pos。利用这些划分好的信息进行归约得到一个新的TSS，对于一些不确定的转换公式的真假性在新的TSS中将会变得更加清晰。在新的定义中→true包含所有肯定成立的转换公式，→pos包含所有可能成立的转换公式，删除具有肯定为假的前提的规则，在其余的规则中删除肯定成立的前提，如此多次归约下去，若可以归约到一个可分层的TSS，则将获得一个唯一稳定的转换模型。
定义3[18]：令S=(Σ,R)为一TSS：
(1)True(S)=(Σ,True(R))，其中True(R)={r∈R|nprem(r)=Ø}。
(3)α是个序数，S进行α次归约后的结果记作Redα(S)，其递归定义为：
①Red0(S)=(Σ,Rclose)，Rclose表示R中规则基例化后的集合。
②Redα(S)=Reduce(S,∪β<α→true(Redβ(S)),∩β<α→pos(Redβ(S)))。
若一个TSSS可以归约到可分层的TSS，则该TSS存在唯一稳定的模型，否则不存在，称该唯一稳定的模型叫做S的相关模型，记作→S。
引理1[18]：如果一个TSSS可以归约到一个可分层的TSS，即存在序数α使得Redα(S)成为正的TSS，则S的相关模型→S=→Redα(S)=→Pos(Redα(S))。
获取TSS的相关模型是确保转换系统的相关性质能够得到可靠证明的必要前提。
2 CC-模拟
定义4：令S=(ΣS,RS)为一TSS，→S为其相关模型，二元关系R⊆T(ΣS)×T(ΣS)是动作集A⊆Actτ上的CC-模拟关系当且仅当(P,Q)∈R蕴含着对所有的a∈A满足：
其中，Ar,Al,Abi是A上的一个划分，三者互不相交，分别为共变、异变和互变动作集。PCC-模拟Q(记作P≥(Ar,Al)SQ)当且仅当存在一个CC-模拟关系R⊆T(ΣS)×T(ΣS)使得(P,Q)∈R。容易验证≥(Ar,Al)S本身是S上的最大CC-模拟关系，且是前序关系(即自反和传递)。此处定义对τ动作和普通可视动作同等看待，因此所定义出的CC-模拟是个强的模拟概念。
易验证上述概念是互模拟和模拟概念的一般化形式。若Ar=Al=Ø，则CC-模拟退化为常规的互模拟，若Al=Abi=Ø，则是常规的模拟。
为了后续同余性的证明，需要引入下面的S1⟹S2-CC-模拟的概念作为辅助。
定义5:给定S1=(ΣS1,RS1)，S2=(ΣS2,RS2)为两个TSS，二者对应的相关模型分别为→S1和→S2。二元关系R⊆T(ΣS1)×T(ΣS2)是动作集A⊆Actτ上的S1⟹S2-CC-模拟关系当且仅当(P,Q)∈R蕴含着对所有的a∈A满足：
上述概念是意图用→S2去近似→S1(因为→S1执行一个转换动作→S2也可以执行相同的转换动作)，最终→S2将等同于→S1。则易知S1⟹S2-CC-模拟就是S1上的CC-模拟。
3 CC-模拟关于CC-ntyft/ntyxt算子的前同余性
行为关系的(前)同余性在支持规范的模块化构建和公理系统的推理方面具有重要意义。下面给出(前)同余性的一般定义。
定义6：设
(1)R是一个前序关系；
(2)R对任意*i(1≤i≤n)，若*i是k元运算符，且(aj,bj)∈R(1≤j≤k)，则(*i(a1,…,ak),*i(b1,…,bk))∈R。
若将(1)改成“R是等价关系”则得到同余的概念。
(前)同余性的概念用于支持规范的模块化构建和推理。当系统具有(前)同余性时，某个项可以用与之行为等价的项进行替换，而整个系统的行为保持不变。因此，获取(前)同余性，将会帮助后续很多证明的实现，比如公理系统的可靠完备性证明中，(前)同余性通常都是必要的辅助。
由下文的例1-例4不难发现，不是所有的ntyft/ntyxt算子对CC-模拟都是保持前同余性的。因此，下面将提取出ntyft/ntyxt算子中能满足前同余性要求的算子来进行研究，并说明所获取的是能满足CC-模拟前同余性要求的ntyft/ntyxt算子的最大子集。
定义7：一个基于型Σ的ntyft规则是由一组转换公式作为前提和一个单独的公式作为后承组成的，形式如下：
其中，ak,bj,c∈Actτ且互不相同，f∈Σ是l元算子，yk,xi(1≤i≤l)∈VPk,Pj,P∈T(Σ)，K和J是(可能无限的)下标的集合。
一个规则是ntyxt形式当其符合如下形式：
其中，yk,x∈V且互不相同，ak,bj,c∈Actτ，Pk,Pj,P∈T(Σ)，K和J是(可能无限的)下标的集合。
称满足ntyft或者ntyxt形式的规则为ntyft/ntyxt规则，称利用ntyft/ntyxt规则定义的算子为ntyft/ntyxt算子。若一个TSS的所有算子都是ntyft/ntyxt算子，则称这种由ntyft/ntyxt算子构成的TSS为nTSS。
定义8：给定一nTSS中的算子f，若所有对其定义的规则都满足以下两个条件：
则称满足上述条件的ntyft/ntyxt规则为CC-ntyft/ntyxt规则，称利用CC-ntyft/ntyxt规则定义的算子为CC-ntyft/ntyxt算子。一个nTSS若其所有的算子都是CC-ntyft/ntyxt算子，那么称该nTSS为CC-nTSS。
下面的四个规则的例子将说明所做的限制条件的必要性。这些例子都是基于一nTSSS=(Σ,R)，Σ中仅包含0，+和a.()算子(三者的操作语义和CCS[1]中定义一致)以及算子();()，动作标记al∈Al，ar∈Ar。
例1：假设();()算子的定义规则只有一条，即
例2：假设算子();()对应的规则改为：
例3：继续修改();()的语义规则：
例4：将();()的语义规则更改为：
类似于例1易知，后面的三个规则定义的算子都不满足CC-模拟前同余性。此四个例子足以说明上述限制条件的必要性。下面给出所获得的CC-ntyft/ntyxt算子对CC-模拟的前同余性的证明。因此可见CC-ntyft/ntyxt算子是ntyft/ntyxt算子中能满足CC-模拟前同余性的最大子集。
在证明前同余性之前，给出下面的两条引理来帮助证明。
引理2[18]：假设一个nTSSS1归约后可分层，则存在一个良基的且归约后可分层的nTSSS2与之等价(两个TSS等价即二者具有相同的相关模型)。
引理3[18]：任何nTSS都存在一个ntyft规则形式定义的纯(pure)nTSS(纯TSS按常规定义)与之等价。
由上面的两条引理，对前同余性证明可直接基于归约后可分层且仅含ntyft规则的纯nTSS进行。
定理2(前同余性)：令S是一个CC-nTSS，假设S能够归约到一个可分层的CC-nTSS，则≥(Ar,Al)S是一个前同余关系。
证明：定理2的证明主要分为以下几步。
(1)构造关系R验证R是一个前同余关系即可得证上述定理:
(2)要验证R是一个前同余关系需要证明以下断言:假设S是一个纯CC-nTSS，且其中的规则仅符合ntyft形式，对所有的序数α≥0，R是一个：
①S⟹Pos(Redα(S))-CC-模拟；
②True(Redα(S))⟹S-CC-模拟。
证明此断言需要对①②两项同时基于序数α进行超限归纳，再分别证明①和②。
假设S=(ΣS,RS)，(P,Q)∈R，对于需验证：
验证上述的(CCR)、(CCL)条件时，因→S即→Strip(S,→s)，可借助定义1中S和Strip(S,→s)规则之间的联系，利用Strip(S,→s)中的正规则以及归约的相关性质，易构造出一闭替换σ找出匹配的Q'或者P'相应地使(CCR)、(CCL)条件成立。
对于②的证明需类似①验证True(Redα(S))⟹S-CC-模拟的(CCR)、(CCL)条件。①②的具体证明过程可类比文献[18]中lemma8.9的证明，注意区别对待动作类型即可。
(3)基于(1)(2)的证明结果，且由S是归约后可分层的，根据引理1可知
R⊆S⟹Pos(Redα(S))-CC-模拟=
≥(Ar,Al)S⊆R，即R=≥(Ar,Al)S，再根据引理2、引理3，则定理2得证。
定理2的结果，对于符合CC-nTSS形式的这类系统关于CC-模拟、模拟以及互模拟关系的前同余性或者同余性的证明可直接套用。
4 结束语
基于ntyft/ntyxt规则形式的算子对CC-模拟的前同余性进行探究，文中提出了ntyft/ntyxt算子中能够满足CC-模拟前同余性的最大子类CC-ntyft/ntyxt。ntyft/ntyxt规则形式是被广泛研究的SOS规则的框架形式之一，文中的研究成果可推广到对符合ntyft/ntyxt规则框架形式的进程代数语言判定其算子是否满足CC-模拟、模拟、互模拟的(前)同余性。在该研究的基础上，后续可基于CC-ntyft/ntyxt规则形式针对CC-模拟的公理化展开研究，从而获得一个公理系统构造的一般性方法，避免公理化过程的重复劳动。
