Graphical representation of covariant-contravariant modal formulae
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 betwee...
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2011-08-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1108.4464v1 |
| _version_ | 1818117800362770432 |
|---|---|
| author | Miguel Palomino Anna Ingólfsdóttir David de Frutos-Escrig Ignacio Fábregas Luca Aceto |
| author_facet | Miguel Palomino Anna Ingólfsdóttir David de Frutos-Escrig Ignacio Fábregas Luca Aceto |
| author_sort | Miguel Palomino |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-11T04:44:10Z |
| format | Article |
| id | doaj.art-2b0aaeb35c28479cb78bc7243f2418d6 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-11T04:44:10Z |
| publishDate | 2011-08-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-2b0aaeb35c28479cb78bc7243f2418d62022-12-22T01:20:33ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802011-08-0164Proc. EXPRESS 201111510.4204/EPTCS.64.1Graphical representation of covariant-contravariant modal formulaeMiguel PalominoAnna IngólfsdóttirDavid de Frutos-EscrigIgnacio FábregasLuca AcetoCovariant-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.http://arxiv.org/pdf/1108.4464v1 |
| spellingShingle | Miguel Palomino Anna Ingólfsdóttir David de Frutos-Escrig Ignacio Fábregas Luca Aceto Graphical representation of covariant-contravariant modal formulae Electronic Proceedings in Theoretical Computer Science |
| title | Graphical representation of covariant-contravariant modal formulae |
| title_full | Graphical representation of covariant-contravariant modal formulae |
| title_fullStr | Graphical representation of covariant-contravariant modal formulae |
| title_full_unstemmed | Graphical representation of covariant-contravariant modal formulae |
| title_short | Graphical representation of covariant-contravariant modal formulae |
| title_sort | graphical representation of covariant contravariant modal formulae |
| url | http://arxiv.org/pdf/1108.4464v1 |
| work_keys_str_mv | AT miguelpalomino graphicalrepresentationofcovariantcontravariantmodalformulae AT annaingolfsdottir graphicalrepresentationofcovariantcontravariantmodalformulae AT daviddefrutosescrig graphicalrepresentationofcovariantcontravariantmodalformulae AT ignaciofabregas graphicalrepresentationofcovariantcontravariantmodalformulae AT lucaaceto graphicalrepresentationofcovariantcontravariantmodalformulae |