[1]李苏婷,张 严.ntyft/ntyxt 算子下共变-异变模拟的前同余性[J].计算机技术与发展,2019,29(09):40-44.[doi:10. 3969 / j. issn. 1673-629X. 2019. 09. 008]
　LI Su-ting,ZHANG Yan.Precongrunence of Covariant-contravariant Simulation under ntyft/ntyxt Operators[J].,2019,29(09):40-44.[doi:10. 3969 / j. issn. 1673-629X. 2019. 09. 008]
点击复制

ntyft/ntyxt 算子下共变-异变模拟的前同余性()
分享到：

《计算机技术与发展》[ISSN:1006-6977/CN:61-1281/TN]

卷:
29
期数:
2019年09期
页码:
40-44
栏目:
智能、算法、系统工程
出版日期:
2019-09-10

文章信息/Info

Title:
Precongrunence of Covariant-contravariant Simulation under ntyft/ntyxt Operators
文章编号:
1673-629X(2019)09-0040-05
作者:
李苏婷1 ; 张 严2
1. 南京航空航天大学 计算机科学与技术学院,江苏 南京 211106; 2. 南京林业大学 信息科学技术学院,江苏 南京 210037
Author(s):
LI Su-ting1 ; ZHANG Yan2
1. School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China; 2. School of Information Science and Technology,Nanjing Forestry University,Nanjing 210037,China
关键词:
结构化操作语义; 共变-异变模拟; ntyft/ ntyxt; CC-ntyft/ ntyxt; 前同余性; 分层; 归约
Keywords:
structural operational semantics;  covariant-contravariant simulation;  ntyft/ntyxt;  CC-ntyft/ntyxt;  precongruence;  stratification; reduction
分类号:
TP301
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 算子的前同余性。
Abstract:
Process algebra is one of the important methods for characterizing the behavior of concurrent and interactive reaction systems.The (bi) simulation relationships and their axiomatization and structural operational semantics (SOS) theory are two important research directions of process algebra. As a generalization of the concept of (bi) simulation,covariant-contravariant simulation (CC-simulation) distinguishes actions and expresses the fact that“the larger the number of behaviors,the better” are not necessarily right. The (pre)congruence of the behavioral relationships is important in supporting the modular construction of formal specifications and the reasoning of axiomatic systems. Normally,a proof of (pre)congruence needs to be verified one by one according to the SOS rules of the operators in the process algebraic language. In order to avoid duplication of labor in (pre)congruence proofs,a variety of types of SOS rules has been proposed. Among them,the ntyft/ ntyxt rule format is the representative one. Based on the ntyft/ntyxt rule format,we propose its largest subclass,CC-ntyft/ntyxt rule format,which satisfies the precongruence of CC-imulation.
更新日期/Last Update: 2019-09-10