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

Precongrunence of Covariant-contravariant Simulation under ntyft/ntyxt Operators

作　　者：李苏婷 张严 LI Su-ting;ZHANG Yan(School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics, Nanjing 211106,China;School of Information Science and Technology,Nanjing Forestry University,Nanjing 210037,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,江苏南京211106 [2]南京林业大学信息科学技术学院,江苏南京210037

出　　处：《计算机技术与发展》2019年第9期40-44,134,共6页Computer Technology and Development

基　　金：国家自然科学基金(61602249);江苏省普通高校自然科学研究资助项目(17KJB520012)

摘　　要：进程代数是刻画并发与交互式反应系统行为的重要模型之一,进程间的(互)模拟关系及其公理化以及结构化操作语义(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算子的前同余性。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-simulation.

关 键 词：结构化操作语义 共变-异变模拟 ntyft/ntyxt CC-ntyft/ntyxt 前同余性 分层 归约 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]