The correctness of concurrencies in (reversible) concurrent calculi

This article designs a general principle to check the correctness of the definition of concurrency (a.k.a. independence) of events for concurrent calculi. Concurrency relations are central in process algebras, but also two-sided: they are often defined independently on composable and on coinitial transitions, and no criteria exist to assess whether they interact correctly. This article starts by examining how reversibility can provide such a correctness of concurrencies criterion, and its implications. It then defines, for the first time, a syntactical definition of concurrency for CCSK, a reversible declension of the calculus of communicating systems. To do so, according to our criterion, requires to define concurrency relations for all types of transitions along two axes: direction (forward or backward) and concomitance (coinitial or composable). Our definition is uniform thanks to proved transition systems and satisfies our sanity checks: square properties, sideways diamonds, but also the reversible checks (reverse diamonds and causal consistency). We also prove that our formalism is either equivalent to or a refinement of pre-existing definitions of concurrency for reversible systems. We conclude by discussing additional criteria and possible future works.

Automated summary

This article presents a general principle for checking the correctness of the definition of concurrency in concurrent calculi. It examines the use of reversibility in providing a criterion for assessing the correctness of concurrencies. The article introduces a syntactical definition of concurrency for CCSK and also shows the equivalence or refinement of this formalism to pre-existing definitions for reversible systems.