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

摘要

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