Hereditary History-Preserving Bisimilarity: Characterizations via Backward Ready Multisets
Marco Bernardo, Andrea Esposito, Claudio A. Mezzina
TL;DR
This work introduces two complementary characterizations of hereditary history-preserving bisimilarity (HHPB) for true-concurrency models: a denotational characterization over stable configuration structures and an operational one via a reversible process calculus. Both approaches augment forward-reverse bisimilarity with backward ready multiset (brm) equality, enabling a lighter, multiset-based view that still distinguishes autoconcurrency and autocausation under the absence of non-local conflicts. The paper also relates these notions to event-identifier logic PU14 and develops a brm-forward-reverse bisimilarity for processes, including a corresponding backward-ready-multiset logic and a denotational mapping to stable configuration structures using proof terms. Under the locality condition for conflicts, the two views align, providing a cohesive framework for reasoning about reversible true concurrency and paving the way for further logical and axiomatic insights and potential verification techniques. Finally, it outlines directions to extend these results beyond the locality restriction and to deepen connections with related logics and formalisms in true concurrency and reversibility.
Abstract
We devise two complementary characterizations of hereditary history-preserving bisimilarity (HHPB): a denotational one, based on stable configuration structures, and an operational one, formulated in a reversible process calculus. Our characterizations rely on forward-reverse bisimilarity augmented with backward ready multiset equality. This shifts the emphasis from uniquely identifying events, as done in previous characterizations, to counting occurrences of identically labeled events associated with incoming transitions, which yields a more lightweight behavioral equivalence than HHPB. We show that our characterizations correctly distinguish between autoconcurrency and autocausation, but are valid only in the absence of non-local conflicts. We then study the logical foundations of these characterizations by relating event identifier logic, which captures the classical view of HHPB, and backward ready multiset logic, developed for our new equivalence.