Reversible Barbed Congruence on Configuration Structures

TL;DR

This paper introduces a reversible process algebra to define a strong back-and-forth barbed congruence, which characterizes hereditary history preserving bisimulation (HHPB) on configuration structures, offering a new contextual perspective.

Contribution

It establishes a reversible process algebra framework that characterizes HHPB through a back-and-forth barbed congruence, linking operational and denotational semantics.

Findings

Back-and-forth barbed congruence is equivalent to HHPB.

Reversible process algebra provides a new way to characterize process equivalences.

The approach offers a contextual characterization of HHPB.

Abstract

A standard contextual equivalence for process algebras is strong barbed congruence. Configuration structures are a denotational semantics for processes in which one can 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 using a reversible process algebra and show that the relation induced by the back and forth congruence is equivalent to HHPB, providing a contextual characterization of HHPB.