RT Journal Article
T1 Graphical representation of covariant-contravariant modal formulae
A1 Aceto, Luca
A1 Fábregas Alfaro, Ignacio
A1 Frutos Escrig, David De
A1 Ingolfsdottir, Anna
A1 Palomino Tarjuelo, Miguel
AB 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.
PB EPTCS
SN 2075-2180
YR 2011
FD 2011
LK https://hdl.handle.net/20.500.14352/43751
UL https://hdl.handle.net/20.500.14352/43751
LA eng
NO Aceto, L., Fábregas Alfaro, I., Frutos Escrig, D. et al. «Graphical representation of covariant-contravariant modal formulae». Electronic Proceedings in Theoretical Computer Science, vol. 64, agosto de 2011, pp. 1-15. arXiv.org, https://doi.org/10.4204/EPTCS.64.1.
NO Proceedings 18th International Workshop on Expressiveness in Concurrency (EXPRESS 2011), Aachen, Germany, 5th September 2011
NO Comunidad de Madrid
NO Ministerio de Ciencia, Innovación y Universidades (España)
NO Ministerio de Educación, Formación Profesional y Deportes (España)
NO Universidad Complutense de Madrid 
NO Icelandic Research Fund
DS Docta Complutense
RD 2 may 2025