Hereditary History-Preserving Bisimilarity: Characterizations via Backward Ready Multisets

TL;DR

This paper introduces new characterizations of hereditary history-preserving bisimilarity using backward ready multisets, providing a lightweight and more efficient way to distinguish concurrent behaviors in reversible systems.

Contribution

It presents denotational and operational characterizations of HHPB based on backward ready multisets, shifting focus from event identification to counting event occurrences.

Findings

Characterizations distinguish autoconcurrency and autocausation.

Valid only without non-local conflicts.

Relates event identifier logic to backward ready multiset logic.

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.