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

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

关键词:
  • gsos  
  • 进程演算  
  • 可靠性  
  • 完备性  
作者:
李苏婷; 张严
单位:
南京航空航天大学计算机科学与技术学院; 南京211106; 南京林业大学信息科学技术学院; 南京210037
刊名:
计算机科学

注:因版权方要求,不能公开全文,如需全文,请咨询杂志社

期刊名称:计算机科学

计算机科学杂志紧跟学术前沿,紧贴读者,国内刊号为:50-1075/TP。坚持指导性与实用性相结合的原则,创办于1974年,杂志在全国同类期刊中发行数量名列前茅。