← 研踪 PaperTrailarXiv:2512.06959 · v2
Hereditary History-Preserving Bisimilarity: Characterizations via Backward Ready Multisets
首次提交 2025-12-08 02:43
版本更新 2026-10-30 00:05
雷达观测 2026-10-30 13:28
摘要
We devise two complementary characterizations of hereditary history-preserving bisimilarity (HHPB): a denotational one, over stable configuration structures, and an operational one, in a reversible process calculus. Our characterizations rely on forward-reverse bisimilarity (FRB) augmented with backward ready multiset equality, which is able to distinguish between autoconcurrency and autocausation. With respect to previous work, we thus shift the emphasis from uniquely identifying events, as done in other characterizations, to counting occurrences of identically labeled events associated with incoming transitions. This yields a more lightweight behavioral equivalence than HHPB: our bisimulations are still binary relations instead of ternary ones and do not need to incrementally build any labeling- and causality-preserving bijection for occurred events. We show that our characterizations are valid in the absence of non-local autoconflicts. We then study the logical foundations of these characterizations by relating event identifier logic, which captures HHPB, and backward ready multiset logic, developed for our extension of FRB.
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v2 · 2026-10-30 00:05 · 最新观测版本
Hereditary History-Preserving Bisimilarity: Characterizations via Backward Ready Multisets
We devise two complementary characterizations of hereditary history-preserving bisimilarity (HHPB): a denotational one, over stable configuration structures, and an operational one, in a reversible process calculus. Our characterizations rely on forward-reverse bisimilarity (FRB) augmented with backward ready multiset equality, which is able to distinguish between autoconcurrency and autocausation. With respect to previous work, we thus shift the emphasis from uniquely identifying events, as done in other characterizations, to counting occurrences of identically labeled events associated with incoming transitions. This yields a more lightweight behavioral equivalence than HHPB: our bisimulations are still binary relations instead of ternary ones and do not need to incrementally build any labeling- and causality-preserving bijection for occurred events. We show that our characterizations are valid in the absence of non-local autoconflicts. We then study the logical foundations of these characterizations by relating event identifier logic, which captures HHPB, and backward ready multiset logic, developed for our extension of FRB.
查看此版本解读 →查看此版本原文 ↗