A Logic for True Concurrency

TL;DR

This paper introduces a new logic for true concurrency that captures various behavioral equivalences, including hereditary history preserving bisimilarity, and extends to infinite computations with fixpoint operators.

Contribution

It presents a unified logical framework for true concurrency, encompassing multiple behavioral equivalences and extending to infinite behaviors with fixpoints.

Findings

Logical equivalence matches hereditary history preserving bisimilarity.

Fragments correspond to step, pomset, and history preserving bisimilarities.

Extension with fixpoints describes properties of infinite computations.

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, is also recovered as a fragment. We also propose an extension of the logic with fixpoint operators, thus allowing to describe causal and concurrency properties of infinite computations. We believe that this work contributes to a rational presentation of the true concurrent spectrum and to a deeper understanding of the relations between the involved behavioural equivalences.