ntyft/ntyxt算子下共变-异变模拟的前同余性

• 作者: 张严 李苏婷
• 来源期刊: 计算机技术与发展
• 学科: 工学
• 关键词: 结构化操作语义 共变-异变模拟 ntyft/ntyxt CC-ntyft/ntyxt 前同余性 分层 归约
• 年，卷（期）: 2019,（9）
• 所属期刊栏目: 智能、算法、系统工程
• 页码范围: 40-44,134
• 页数: 6页
• 分类号: TP301
• 字数: 6224字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-629X.2019.09.008

摘要

进程代数是刻画并发与交互式反应系统行为的重要模型之一,进程间的(互)模拟关系及其公理化以及结构化操作语义(structural operational semantics,SOS)理论是其重要的两个研究方向.共变-异变模拟(covariant-contravariant simulation,CC-模拟)是(互)模拟关系概念的推广,它对动作进行区分,表达了状态的行为数目越多但并不一定越好的事实.行为关系的(前)同余性质在支持其形式规范的模块化构建和公理系统的推理方面具有重要意义.(前)同余性的证明需要根据进程代数语言中算子的SOS规则逐个验证.为了避免(前)同余性证明的重复劳动,学术界提出了多种类型的SOS规则的框架形式.ntyft/ntyxt规则形式是目前具有代表性的SOS规则框架形式之一.文中基于ntyft/ntyxt规则形式,提出了能满足CC-模拟前同余性的最大ntyft/ntyxt子类CC-ntyft/ntyxt规则形式,并证明了CC-模拟相对CC-ntyft/ntyxt算子的前同余性.

作者信息

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