Characterising spectra of equivalences for event structures, logically

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.