Dependence and Independence for Reversible Process Calculi

TL;DR

This paper develops a formal framework for reversible process calculi, defining dependence and independence relations based on enriched transition labels, and explores their implications for concurrency, causality, and bisimulation.

Contribution

It introduces separate, formally defined dependence and independence relations for reversible calculi, proving their properties and relationships within a new axiomatic approach.

Findings

Defined dependence and independence relations for reversible processes

Proved the complementarity of these relations on connected transitions

Provided a new characterization of History Preserving bisimulation for CCS

Abstract

To refine formal methods for concurrent systems, there are several ways of enriching classical operational semantics of process calculi. One can enable the auditing and undoing of past synchronisations thanks to communication keys, thus easing the study of true concurrency as a by-product. Alternatively, proof labels embed information about the origins of actions in transition labels, facilitating syntactic analysis. Enriching proof labels with keys enables a theory of the relations on transitions and on events based on their labels only. We offer for the first time separate definitions of dependence relation and independence relation, and prove their complementarity on connected transitions instead of postulating it. Leveraging the recent axiomatic approach to reversibility, we prove the canonicity of these relations and provide additional tools to study the relationships between e.g., concurrency and causality on transitions and events. Finally, we make precise the subtle relationship between bisimulations based on both forward and backward transitions, on key ordering, and on dependency preservation, providing a direct definition of History Preserving bisimulation for CCS.