黄 振 华

(南京航空航天大学计算机科学与技术学院　江苏 南京 210016)



Institution框架下的结构化标记共变-逆变模拟

黄 振 华

(南京航空航天大学计算机科学与技术学院江苏 南京 210016)

摘要结构化标记共变-逆变模拟是共变-逆变模拟的一种扩充，在处理转换系统的模拟关系时考虑了标记本身的结构。结构化标记模态转换系统间的模态精化与结构化标记共变-逆变模拟之间存在诸多相似之处，为了在更抽象层次上研究两者的关系，引入Institution框架。基于该框架，讨论结构化标记模态转换系统间的模态精化与结构化标记共变-逆变模拟之间的关系，并证明前者到后者存在Institution态射。结果表明，相比结构化标记模态转换系统中模态精化关系，结构化标记共变-逆变模拟具有更强的表达能力。

关键词Institution结构化标记模态转换系统共变-逆变模拟

LABEL-STRUCTURED COVARIANT-CONTRAVARIANT SIMULATION IN INSTITUTION FRAMEWORK

Huang Zhenhua

(School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,Jiangsu,China)

AbstractThe label-structured covariant-contravariant simulation is an expansion of covariant-contravariant simulation,which considers the structure of labels themselves in dealing with the simulation relation of transition systems. There are many similarities between the modal refinement in label-structured modal transition systems and the label-structured covariant-contravariant simulation. In order to gain more insight into the relationship between them at a more abstract level,the Institutions framework is introduced. Based on that framework,we discuss the relationship between modal refinement in label-structured modal transition systems and label-structured covariant-contravariant simulation,and prove that there exists an Institution morphism from the former to the latter. This result indicate that label-structured covariant-contravariant simulation is more expressive than modal refinement relationship in label-structured modal transition systems.

KeywordsInstitutionLabel-structuredModal transition systemCovariant-contravariant simulation

0引言

在进程代数研究领域，转换系统作为重要的语义模型应用广泛，其中最常见的是带标记的转换系统LTS(Label Transition System)[1]，它可用于描述一般的并发系统的行为。模态转换系统MTS(Modal Transition System)[2，3]本质上是一种LTS，其将转换分成了两种类型：可能转换和必然转换。实际上，一般的LTS也可以看作是可能转换与必然转换一致的MTS。不少的研究扩充了MTS概念，文献[4]介绍了几种定量模态转换系统(Quantitative MTS)、时序模态转换系统(Timing MTS)、加权模态转换系统(Weighted MTS)和概率模态转换系统(Probabilistic MTS)等。这些MTS的最大特点在于，转化标记上附加了定量信息。最近，Bauer等人提出结构化标记模态转换系统LSMTS(Label-Structured MTS)[5，6]，对带有定量信息的MTS进行了一般性研究。……