  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.
