Hereditary History-Preserving Bisimilarity: Characterizations via Backward Ready Multisets
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _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 |