GSOS算子下共变-异变模拟的公理刻画

进程的行为理论是进程演算研究的核心内容之一,其侧重于讨论进程间的行为等价和模拟关系。共变-异变模拟(Covariant-Contravariant Simulation,CC-模拟)的概念是对经典(互)模拟概念的推广,它通过区分动作类型,刻画了规范与实现对系统主动、被动和通讯动作在精化关系中的不同要求。行为关系的(前)同余性和公理刻画是进程演算代数特征的集中体现,它们对规范及实现的分析和推理至关重要。一般而言,行为关系(前)同余性的证明和公理系统的构造需要基于不同进程演算系统的结构化操作语义(Structural Operational Semantics,SOS)分别展开。为了避免这类研究工作中的重复劳动,学术界针对一般化SOS规则形式的元理论开展了研究,GSOS是其中被广泛研究的规则形式之一。文中在考量了动作类型的基础上,基于CC-模拟对GSOS规则形式做出扩充,提出了CC-GSOS规则类型,证明了CC-模拟相对于CC-GSOS算子具有前同余性,并给出了在这些算子下CC-模拟的可靠完备公理系统的一般性构造方法。

Axiomatizing Covariation-Contravariation Simulation Under GSOS Operators

The behavioral theory of processes is one of the core research contents of process calculus,which focuses on discussing behavioral equivalence or simulation relationships between processes.The Covariant-Contravariant simulation(CC-simulation)is the extension of the(bi)simulation,which distinguishes the types of actions and expresses the different requirement of active,passive and communication actions in refinement relationships between specifications and implementations.The(pre)congruence and axiomatization of behavioral relationships are the concentrated expression of the algebraic features of process calculus,which are essential for the analysis and reasoning of specifications and implementations.In general,the proof of behavioral(pre)congruence and the construction of axiomatic systems need to be based on the Structural Operational Semantics(SOS)of different process calculus systems.In order to avoid duplication of labor in these kinds of research work,the academia has carried out research on the meta-theory of the generalized SOS rule formats,and GSOS is one of the format that have been widely studied.Based on the consideration of action types,this paper extends the GSOS rule format for CC-simulation,proposes CC-GSOS rule format,and proves that the CC-simulation is a precongruent relation relative to CC-GSOS operators,gives a general method for constructing axiomatic system for CC-simulation which is sound and complete.