Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Dependence and Independence for Reversible Process Calculi

Clément Aubert, Iain Phillips, Irek Ulidowski

TL;DR

This work offers for the first time separate definitions of dependence relation and independence relation, and proves the canonicity of these relations and provides additional tools to study the relationships between e.g., concurrency and causality on transitions and events.

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.

Dependence and Independence for Reversible Process Calculi

TL;DR

This work offers for the first time separate definitions of dependence relation and independence relation, and proves the canonicity of these relations and provides additional tools to study the relationships between e.g., concurrency and causality on transitions and events.

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.

Paper Structure

This paper contains 26 sections, 57 theorems, 23 equations, 7 figures.

Table of Contents

  1. Introduction
  2. Background and Related Work
  3. CCSK with Proof Labels
  4. Complementary Relations for Independence and Dependence
  5. Basics of the Axiomatic Approach
  6. Properties of CCSK and PCCSK
  7. Instantiating the Axiomatic Approach to CCSKP and CCSK
  8. Key-Based Properties of CCSK and PCCSK
  9. KP and DP Bisimulations
  10. Pinpointing the Relevant Relations
  11. Bisimulations
  12. Conclusion
  13. Section \ref{['sec:proved-lts']}: Bijection between PCCSK and CCSK
  14. \ref{['sec:ind-complem']}: Conservativity and Complementarity of the Independence and Dependence Relations
  15. Conservativity Over Concurrency of CCS with Proof Labels
  16. ...and 11 more sections

Key Result

lemma 1

For all $t: X \pr{f}[\theta] Y$, there exists $\ushortw{t}: Y \pr{b}[\theta] X$, and conversely. Furthermore, $\ushortw{\ushortw{t}} = t$.

Figures (7)

  • Figure 1: Forward and backward transition rules for $\mathsf{CCS}{\mathsf{K}}^{\mathsf{P}}$ (${\mid_{\mathrm{R}}}$,${\ushortwt{\mid_{\mathrm{R}}}}$, ${+_{\mathrm{R}}}$ and ${\ushortw{+_{\mathrm{R}}}}$ omitted).
  • Figure 2: A sample of processes reachable from $a[k] \mid (\overline{a} + b)$.
  • Figure 3: Relations on proof labels
  • Figure 4: Main properties studied by the axiomatic approach. In the tables above, an LTSI satisfies Property if the condition on the right holds.
  • Figure 5: LTSI for $a. (b \mid c.d)$ in \ref{['conc-tran-clo']}.
  • ...and 2 more figures

Theorems & Definitions (140)

  • definition 1: (Co-)names, labels and keys
  • definition 2: Operators
  • definition 3: Proof labels
  • definition 5: LTS for $\mathsf{CCS}{\mathsf{K}}$ with proof labels Aub22aubert2023c
  • definition 6: Transitions
  • definition 7: Standard and reachable processes
  • lemma 1: Loop Lemma
  • definition 9: Relations on proof labels
  • remark 1
  • proposition 1
  • ...and 130 more