协变-逆变模态公式的图形表示
Graphical representation of covariant-contravariant modal formulae
摘要：
协变-逆变模拟是标准（协变）模拟、逆变模拟和互模拟的组合。我们以前研究了它的逻辑特征的协变-逆变模态逻辑。此外，我们已经调查了这个模型之间的关系，模态转换系统，两种转换（所谓的可能和必须转换）相结合，以获得一个简单的框架来表达的概念，细化状态转换模型。在一篇经典论文中，Boudol和Larsen建立了图形方法（通过模态转换系统）和逻辑方法（基于无否定的Hennessy-Milner逻辑）之间的精确联系。他们得到了一个（图形）表示定理证明，一个公式可以表示为一项，当且仅当，它是一致的和素数。本文证明了协变-逆变模态逻辑中的公式是一致的和素的，这些公式允许通过过程的“图形”表示，模的协变-逆变模拟前序。为了获得所需的图形表示结果，我们首先限制自己的情况下，协变逆变系统没有双变的行动。双变动作可以通过编码的方式合并，该编码将每个双变动作分成其协变和逆变部分。
英文摘要：
Covariant-contravariant simulation is a combination of standard (covariant) simulation, its contravariant counterpart and bisimulation. We have previously studied its logical characterization by means of the covariant-contravariant modal logic. Moreover, we have investigated the relationships between this model and that of modal transition systems, where two kinds of transitions (the so-called may and must transitions) were combined in order to obtain a simple framework to express a notion of refinement over state-transition models. In a classic paper, Boudol and Larsen established a precise connection between the graphical approach, by means of modal transition systems, and the logical approach, based on Hennessy-Milner logic without negation, to system specification. They obtained a (graphical) representation theorem proving that a formula can be represented by a term if, and only if, it is consistent and prime. We show in this paper that the formulae from the covariant-contravariant modal logic that admit a "graphical" representation by means of processes, modulo the covariant-contravariant simulation preorder, are also the consistent and prime ones. In order to obtain the desired graphical representation result, we first restrict ourselves to the case of covariant-contravariant systems without bivariant actions. Bivariant actions can be incorporated later by means of an encoding that splits each bivariant action into its covariant and its contravariant parts.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
