We present a logical characterisation of the equivalences in the spectrum for labelled Prime Event Structures (PESs) and use it for also studying how such spectrum changes when restricting to subclasses of event structures. We first show that a minor modification of the logic characterising hereditary history preserving bisimilarity induces PES isomorphism as logical equivalence. Then, we distill fragments of the logic that characterise all the equivalences in the aforementioned spectrum. In particular, we single out logics for interleaving/step/pomset trace equivalences and weak (pomset) history preserving bisimilarity, which were missing. Finally, we apply our logical characterisation to investigate how the spectrum simplifies when we restrict to subclasses of event structures: Coherence Spaces, where causality is absent, and Elementary Event Structures, where instead conflicts are not allowed. Inclusions between behavioural equivalences are proved by providing encodings between the corresponding sublogics, whereas the non-inclusion between equivalences is witnessed by using distinguishing formulae, i.e., by providing structures which are identified by an equivalence and distinguished by a formula in the logics of the other equivalence.
Characterising Spectra of Equivalences for Event Structures, Logically
Tommaso Padoan;
2022-01-01
Abstract
We present a logical characterisation of the equivalences in the spectrum for labelled Prime Event Structures (PESs) and use it for also studying how such spectrum changes when restricting to subclasses of event structures. We first show that a minor modification of the logic characterising hereditary history preserving bisimilarity induces PES isomorphism as logical equivalence. Then, we distill fragments of the logic that characterise all the equivalences in the aforementioned spectrum. In particular, we single out logics for interleaving/step/pomset trace equivalences and weak (pomset) history preserving bisimilarity, which were missing. Finally, we apply our logical characterisation to investigate how the spectrum simplifies when we restrict to subclasses of event structures: Coherence Spaces, where causality is absent, and Elementary Event Structures, where instead conflicts are not allowed. Inclusions between behavioural equivalences are proved by providing encodings between the corresponding sublogics, whereas the non-inclusion between equivalences is witnessed by using distinguishing formulae, i.e., by providing structures which are identified by an equivalence and distinguished by a formula in the logics of the other equivalence.File | Dimensione | Formato | |
---|---|---|---|
IC-2022-CharacterisingSpectraEquivalencesES.pdf
Accesso chiuso
Tipologia:
Documento in Versione Editoriale
Licenza:
Copyright Editore
Dimensione
672.44 kB
Formato
Adobe PDF
|
672.44 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
IC-2022-CharacterisingSpectraEquivalencesES-Post_print.pdf
Open Access dal 04/03/2023
Tipologia:
Bozza finale post-referaggio (post-print)
Licenza:
Creative commons
Dimensione
1.23 MB
Formato
Adobe PDF
|
1.23 MB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.