Contextual equivalences in configuration structures and reversibility

•A definition of strong back-and-forth barbed congruence on RCCS is proposed.•This relation relies on some choices of context and barbs for RCCS, two notions that do not yet have a canonical definition.•Configuration structures are shown to be models for reversibility in which we can interpret RCCS.•Hereditary history preserving bisimulation is a classical equivalence on configuration structures, that we prove to correspond to the strong barbed back-and-forth.

Contextual equivalences equate terms that have the same observable behavior 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 defines 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.