Contextual equivalences in configuration structures and reversibility

TL;DR

This paper establishes a new contextual equivalence in reversible process calculi that precisely characterizes hereditary history preserving bisimulation through configuration structures.

Contribution

It introduces a strong back-and-forth barbed congruence for RCCS and proves its equivalence to HHPB, linking operational and denotational semantics.

Findings

Back-and-forth congruence characterizes HHPB

Equivalence is established between operational and denotational semantics

Provides a new tool for reasoning about reversible processes

Abstract

Contextual equivalence equate terms that have the same observable behaviour in any context. A standard contextual equivalence for CCS is the strong barbed congruence. Configuration structures are a denotational semantics for processes in which one define equivalences that are more discriminating, i.e. that distinguish the denotation of terms equated by barbed congruence. Hereditary history preserving bisimulation (HHPB) is such a relation. We define a strong back-and-forth barbed congruence on RCCS, a reversible variant of CCS. We show that the relation induced by the back-and-forth congruence on configuration structures is equivalent to HHPB, thus providing a contextual characterization of HHPB.