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

• 作者: 张严 李苏婷
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: GSOS 结构化操作语义(SOS) 进程演算 共变-异变模拟 可靠性 完备性
• 年，卷（期）: 2020,（1）
• 所属期刊栏目: 计算机科学理论
• 页码范围: 51-58
• 页数: 8页
• 分类号: TP301
• 字数: 11330字
• 语种: 中文
• DOI: 10.11896/jsjkx.181102026

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李苏婷	南京航空航天大学计算机科学与技术学院	2	0	0.0	0.0
2	张严	南京林业大学信息科学技术学院	2	0	0.0	0.0