Graphical representation of covariant-contravariant modal formulae

TL;DR

This paper extends the graphical representation framework for covariant-contravariant modal logic, showing that certain formulae can be represented by processes, thus linking logical and graphical system specifications.

Contribution

It proves that covariant-contravariant modal formulae that admit process representations are exactly the consistent and prime ones, extending graphical representation results.

Findings

Formulae with process representations are consistent and prime.

Graphical representation aligns with logical characterization.

Extension to bivariant actions via encoding is possible.

Abstract

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.