Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2512.06959 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918236349530112 |
|---|---|
| author | Bernardo, Marco Esposito, Andrea Mezzina, Claudio A. |
| author_facet | Bernardo, Marco Esposito, Andrea Mezzina, Claudio A. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_06959 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Hereditary History-Preserving Bisimilarity: Characterizations via Backward Ready Multisets Bernardo, Marco Esposito, Andrea Mezzina, Claudio A. Logic in Computer Science 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. |
| title | Hereditary History-Preserving Bisimilarity: Characterizations via Backward Ready Multisets |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2512.06959 |