遗传历史保持互模拟：基于后向就绪多重集的特征刻画
Hereditary History-Preserving Bisimilarity: Characterizations via Backward Ready Multisets
Marco Bernardo, Andrea Esposito, Claudio A. Mezzina
AI 速览：作者提出用后向就绪多重集相等增强前向后向互模拟，从而在稳定配置结构和可逆进程演算中给出遗传历史保持互模拟（HHPB）的两种互补刻画。
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.