协变-反变仿真的等式刻画及一致性仿真语义
Equational Characterization of Covariant-Contravariant Simulation and Conformance Simulation Semantics
摘要：
协变-逆变模拟和一致性模拟是对普通模拟的推广，并试图捕捉到“行为数量越多越好”的事实。我们以前研究过它们的逻辑特征，在本文中，我们提出了公理化的前序定义的新的模拟关系和它们的诱导等价。我们的结果的兴趣在于，公理化帮助我们更好地了解新的模拟，特别是理解的作用的逆变特性和它们的相互作用与协变的;此外，公理化为我们提供了一个强大的工具（代数）证明相应的语义的结果。但从元理论的角度来看，我们也认为我们的结果很有趣：协变-逆变模拟等价在没有既表现出协变又表现出逆变行为的行为时确实是基础可公理化的，但是每当我们一起有那种行为以及协变或逆变行为时就变得不可公理化，为我们提供了一个新的微妙的例子，狭窄的边界分离公理化和非公理化语义。我们希望通过研究这些例子，我们将能够开发一个一般的理论分离公理化和非公理化语义。
英文摘要：
Covariant-contravariant simulation and conformance simulation generalize plain simulation and try to capture the fact that it is not always the case that "the larger the number of behaviors, the better". We have previously studied their logical characterizations and in this paper we present the axiomatizations of the preorders defined by the new simulation relations and their induced equivalences. The interest of our results lies in the fact that the axiomatizations help us to know the new simulations better, understanding in particular the role of the contravariant characteristics and their interplay with the covariant ones; moreover, the axiomatizations provide us with a powerful tool to (algebraically) prove results of the corresponding semantics. But we also consider our results interesting from a metatheoretical point of view: the fact that the covariant-contravariant simulation equivalence is indeed ground axiomatizable when there is no action that exhibits both a covariant and a contravariant behaviour, but becomes non-axiomatizable whenever we have together actions of that kind and either covariant or contravariant actions, offers us a new subtle example of the narrow border separating axiomatizable and non-axiomatizable semantics. We expect that by studying these examples we will be able to develop a general theory separating axiomatizable and non-axiomatizable semantics.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
