首页 > 期刊 > 自然科学与工程技术 > 信息科技 > 电子信息科学综合 > 计算机科学 > GSOS算子下共变G异变模拟的公理刻画 【正文】

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

李苏婷; 张严 南京航空航天大学计算机科学与技术学院; 南京211106; 南京林业大学信息科学技术学院; 南京210037
  • gsos
  • 进程演算
  • 可靠性
  • 完备性

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

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

投稿咨询 免费咨询 杂志订阅

我们提供的服务

服务流程: 确定期刊 支付定金 完成服务 支付尾款 在线咨询