可继承历史保持双态不等价：基于逆向就绪多集的表征
计算机科学中的逻辑
2025-12-09 v1
摘要
我们构筑两种互补的可继承历史保持双态不等价（HHPB）表征：一种基于稳定配置结构的语义表征，另一种以可逆过程微积分形式化的操作表征。我们的表征依赖于前向-后向双态不等价增强，以及逆向就绪多集相等。这一转变将重点从前述表征中唯一确定事件，转向计数来自输入转换的标记相同事件的出现次数，从而实现比 HHPB 更轻量级的行为等价性。我们证明了这些表征正确地区分了自并发与自因果，但仅在无非局部冲突的情况下有效。随后我们通过关联事件标识符逻辑（捕获经典 HHPB 观点）与逆向就绪多集逻辑（用于本新等价性）来研究这些表征的逻辑基础。
引用
@article{arxiv.2512.06959,
title = {Hereditary History-Preserving Bisimilarity: Characterizations via Backward Ready Multisets},
author = {Marco Bernardo and Andrea Esposito and Claudio A. Mezzina},
journal= {arXiv preprint arXiv:2512.06959},
year = {2025}
}