A Logic with Reverse Modalities for History-preserving Bisimulations

Iain Phillips
(Imperial College London)
Irek Ulidowski
(University of Leicester)

We introduce event identifier logic (EIL) which extends Hennessy-Milner logic by the addition of (1) reverse as well as forward modalities, and (2) identifiers to keep track of events. We show that this logic corresponds to hereditary history-preserving (HH) bisimulation equivalence within a particular true-concurrency model, namely stable configuration structures. We furthermore show how natural sublogics of EIL correspond to coarser equivalences. In particular we provide logical characterisations of weak history-preserving (WH) and history-preserving (H) bisimulation. Logics corresponding to HH and H bisimulation have been given previously, but not to WH bisimulation (when autoconcurrency is allowed), as far as we are aware. We also present characteristic formulas which characterise individual structures with respect to history-preserving equivalences.

In Bas Luttik and Frank Valencia: Proceedings 18th International Workshop on Expressiveness in Concurrency (EXPRESS 2011), Aachen, Germany, 5th September 2011, Electronic Proceedings in Theoretical Computer Science 64, pp. 104–118.
Published: 20th August 2011.

ArXived at: http://dx.doi.org/10.4204/EPTCS.64.8 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org