A logic for true concurrency
P. Baldan, S. Crafa
Dipartimento di Matematica Pura e Applicata, Università di Padova, Italy
Abstract:
We propose a logic for true concurrency whose formulae predicate about
events in computations and their causal dependencies. The induced
logical equivalence is hereditary history preserving bisimilarity, and
fragments of the logic can be identified which correspond to other
true concurrent behavioural equivalences in the literature: step,
pomset and history preserving bisimilarity. Standard Hennessy-Milner
logic and thus (interleaving) bisimilarity are also recovered as a
fragment. We believe that this contributes to a rational presentation
of the true concurrent spectrum and to a deeper understanding of the
relations between the involved behavioural equivalences.