Document Open Access Logo

Revisiting True Concurrency Bisimilarities: On the Role of Backward Ready Multisets and Why They Are Not Enough for HPB and HHPB

Authors Andrea Esposito , Marco Bernardo

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2026.33.pdf
  • Filesize: 0.97 MB
  • 17 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
Keywords
  • True Concurrency
  • Bisimilarity
  • Configuration Structures
  • Modal Logic

Metrics

Abstract

Bisimilarities over stable configuration structures can be divided into three families. In the first one - including interleaving, step, pomset, and forward-reverse bisimilarities - no isomorphism is required between the events matched during the bisimulation game. In the second one - including weak history-preserving, weak history-preserving pomset, and weak hereditary history-preserving bisimilarities - a labeling- and causality-preserving isomorphism is required between matched events, which is specific to each pair of configurations related by the bisimulation relation and hence can vary for a matched event from pair to pair. In the third one - including history-preserving and hereditary history-preserving bisimilarities - a single isomorphism is built incrementally, which is therefore fixed for all matched events. We revisit true concurrency bisimilarities by introducing variants that additionally check that the backward ready multisets of related configurations coincide. While the distinguishing power of the bisimilarities of the second and third families does not change, the power of the revised bisimilarities of the first family is equal to that of the bisimilarities of the second family. The latter bisimilarities can thus be characterized by replacing variable isomorphisms with simply counting incoming transitions. In contrast, backward ready multisets are not enough to characterize the third family in the simultaneous presence of autoconcurrency and non-local conflicts. We show that a further check for the existence of diamond and half-diamond substructures is necessary in that case to achieve the same distinguishing power as incremental isomorphisms.

Cite As Get BibTex

Andrea Esposito and Marco Bernardo. Revisiting True Concurrency Bisimilarities: On the Role of Backward Ready Multisets and Why They Are Not Enough for HPB and HHPB. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 33:1-33:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CONCUR.2026.33

Author Details

Andrea Esposito
  • Dipartimento di Scienze Pure e Applicate, Università di Urbino, Italy
Marco Bernardo
  • Dipartimento di Scienze Pure e Applicate, Università di Urbino, Italy

Funding

This research has been supported by the PRIN 2020 project NiRvAna - Noninterference and Reversibility Analysis in Private Blockchains.

References

  1. C. Aubert and I. Cristescu. How reversibility can solve traditional questions: The example of hereditary history-preserving bisimulation. In Proc. of the 31st Int. Conf. on Concurrency Theory (CONCUR 2020), volume 171 of LIPIcs, pages 7:1-7:23, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.7.
  2. P. Baldan and S. Crafa. A logic for true concurrency. Journal of the ACM, 61:24:1-24:36, 2014. URL: https://doi.org/10.1145/2629638.
  3. M.A. Bednarczyk. Hereditary history preserving bisimulations or what is the power of the future perfect in program logics. Technical report, Polish Academy of Sciences, Gdansk, 1991. Google Scholar
  4. M. Bernardo, A. Esposito, and C.A. Mezzina. Alternative characterizations of hereditary history-preserving bisimilarity via backward ready multisets. In Proc. of the 28th Int. Conf. on Foundations of Software Science and Computation Structures (FOSSACS 2025), volume 15691 of LNCS, pages 67-87. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-90897-2_4.
  5. M. Bernardo and S. Rossi. Reverse bisimilarity vs. forward bisimilarity. In Proc. of the 26th Int. Conf. on Foundations of Software Science and Computation Structures (FOSSACS 2023), volume 13992 of LNCS, pages 265-284. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30829-1_13.
  6. G. Boudol and I. Castellani. Concurrency and atomicity. Theoretical Computer Science, 59:25-84, 1988. URL: https://doi.org/10.1016/0304-3975(88)90096-5.
  7. S.D. Brookes, C.A.R. Hoare, and A.W. Roscoe. A theory of communicating sequential processes. Journal of the ACM, 31:560-599, 1984. URL: https://doi.org/10.1145/828.833.
  8. Ph. Darondeau and P. Degano. Causal trees. In Proc. of the 16th Int. Coll. on Automata, Languages and Programming (ICALP 1989), volume 372 of LNCS, pages 234-248. Springer, 1989. URL: https://doi.org/10.1007/BFB0035764.
  9. Ph. Darondeau and P. Degano. Causal trees: Interleaving + causality. In Proc. of the LITP Spring School on Theoretical Computer Science: Semantics of Systems of Concurrent Processes, volume 469 of LNCS, pages 239-255. Springer, 1990. URL: https://doi.org/10.1007/3-540-53479-2_10.
  10. R. De Nicola and F. Vaandrager. Three logics for branching bisimulation. Journal of the ACM, 42:458-487, 1995. URL: https://doi.org/10.1145/201019.201032.
  11. P. Degano, R. De Nicola, and U. Montanari. Observational equivalences for concurrency models. In Proc. of the 3rd IFIP Working Conf. on Formal Description of Programming Concepts, pages 105-134. North-Holland, 1986. Google Scholar
  12. H. Fecher. A completed hierarchy of true concurrent equivalences. Information Processing Letters, 89:261-265, 2004. URL: https://doi.org/10.1016/J.IPL.2003.11.008.
  13. J.L. Gischer. The equational theory of pomsets. Theoretical Computer Science, 61:199-224, 1988. URL: https://doi.org/10.1016/0304-3975(88)90124-7.
  14. R.J. van Glabbeek and U. Goltz. Refinement of actions and equivalence notions for concurrent systems. Acta Informatica, 37:229-327, 2001. URL: https://doi.org/10.1007/S002360000041.
  15. R.J. van Glabbeek and G.D. Plotkin. Configuration structures, event structures and Petri nets. Theoretical Computer Science, 410:4111-4159, 2009. URL: https://doi.org/10.1016/J.TCS.2009.06.014.
  16. R.J. van Glabbeek and F. Vaandrager. Bundle event structures and CCSP. In Proc. of the 14th Int. Conf. on Concurrency Theory (CONCUR 2003), volume 2761 of LNCS, pages 57-71. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45187-7_4.
  17. J. Grabowski. On partial languages. Fundamenta Informaticae, 4:427-498, 1981. Google Scholar
  18. M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32:137-162, 1985. URL: https://doi.org/10.1145/2455.2460.
  19. A. Joyal, M. Nielsen, and G. Winskel. Bisimulation from open maps. Information and Computation, 127:164-185, 1996. URL: https://doi.org/10.1006/INCO.1996.0057.
  20. R.M. Keller. Formal verification of parallel programs. Communications of the ACM, 19:371-384, 1976. URL: https://doi.org/10.1145/360248.360251.
  21. R. Milner. Communication and Concurrency. Prentice Hall, 1989. Google Scholar
  22. D. Park. Concurrency and automata on infinite sequences. In Proc. of the 5th GI Conf. on Theoretical Computer Science (GI-TCS 1981), volume 104 of LNCS, pages 167-183. Springer, 1981. URL: https://doi.org/10.1007/BFB0017309.
  23. I. Phillips and I. Ulidowski. Reversing algebraic process calculi. Journal of Logic and Algebraic Programming, 73:70-96, 2007. URL: https://doi.org/10.1016/J.JLAP.2006.11.002.
  24. I. Phillips and I. Ulidowski. Reversibility and models for concurrency. In Proc. of the 4th Int. Workshop on Structural Operational Semantics (SOS 2007), volume 192(1) of ENTCS, pages 93-108. Elsevier, 2007. URL: https://doi.org/10.1016/J.ENTCS.2007.08.018.
  25. I. Phillips and I. Ulidowski. A hierarchy of reverse bisimulations on stable configuration structures. Mathematical Structures in Computer Science, 22:333-372, 2012. URL: https://doi.org/10.1017/S0960129511000429.
  26. I. Phillips and I. Ulidowski. Event identifier logic. Mathematical Structures in Computer Science, 24(2):1-51, 2014. Google Scholar
  27. L. Pomello. Some equivalence notions for concurrent systems. an overview. In Advances in Petri Nets, volume 222 of LNCS, pages 381-400. Springer, 1985. URL: https://doi.org/10.1007/BFB0016222.
  28. A.M. Rabinovich and B.A. Trakhtenbrot. Behavior structures and nets. Fundamenta Informaticae, 11:357-404, 1988. Google Scholar
  29. J. Valdes, R.E. Tarjan, and E.L. Lawler. The recognition of series parallel digraphs. SIAM Journal on Computing, 11:298-313, 1982. URL: https://doi.org/10.1137/0211023.
  30. G. Winskel. Event structures. In Advances in Petri Nets, volume 255 of LNCS, pages 325-392. Springer, 1986. URL: https://doi.org/10.1007/3-540-17906-2_31.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact