Document Open Access Logo

Bisimulations and Modal Logics for Higher Dimensional Automata

Authors Safa Zouari , Rob van Glabbeek , Krzysztof Ziemiański

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2026.49.pdf
  • Filesize: 1.01 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Modal and temporal logics
Keywords
  • higher-dimensional automata
  • bisimilarity
  • history-preserving bisimulation
  • modal logic
  • concurrency theory

Metrics

Abstract

Higher-Dimensional Automata (HDAs) provide a geometric model of true concurrency. While hereditary history-preserving (hhp) bisimilarity is the finest behavioural equivalence in van Glabbeek’s spectrum, no modal logic has previously characterised it on HDAs. We introduce several new intermediate equivalences that sit strictly between ST- and hhp-bisimilarity. We show how separating similarity and subsumption of paths leads to a clean formulation of these equivalences, and we present a modal logic that characterises hhp-bisimilarity. Natural fragments characterise ST-bisimilarity and the intermediate notions.

Cite As Get BibTex

Safa Zouari, Rob van Glabbeek, and Krzysztof Ziemiański. Bisimulations and Modal Logics for Higher Dimensional Automata. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 49:1-49:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CONCUR.2026.49

Author Details

Safa Zouari
  • Norwegian University of Science and Technology Gjøvik, Norway
Rob van Glabbeek
  • School of Informatics, University of Edinburgh, Scotland
  • School of Computer Science and Engineering, University of New South Wales, Sydney, Australia
Krzysztof Ziemiański
  • Institute of Mathematics, University of Warsaw, Poland

Funding

  • Zouari, Safa: Supported by a PhD fellowship at the Department of Information Security and Communication Technology (IIK), Norwegian University of Science and Technology (NTNU).
  • van Glabbeek, Rob: Supported by Royal Society Wolfson Fellowship RSWF\R1\221008.

References

  1. Clément Aubert, Ross Horne, and Christian Johansen. Diamonds for security: A non-interleaving operational semantics for the applied π-calculus. In Proceedings of CONCUR 2022, volume 243 of LIPIcs. Schloss Dagstuhl, 2022. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.30.
  2. Clément Aubert, Ross Horne, Christian Johansen, and Sjouke Mauw. Unlinkability and history preserving bisimilarity. Computer Security, 165, 2026. URL: https://doi.org/10.1016/j.cose.2025.104819.
  3. Paolo Baldan and Silvia Crafa. Hereditary history-preserving bisimilarity: Logics and automata. In Jacques Garrigue, editor, Proc. Programming Languages and Systems (APLAS'14), volume 8858 of lncs, pages 469-488, 2014. URL: https://doi.org/10.1007/978-3-319-12736-1_25.
  4. Paolo Baldan and Silvia Crafa. A logic for true concurrency. J. ACM, 61(4):24:1-24:36, 2014. URL: https://doi.org/10.1145/2629638.
  5. Marek A. Bednarczyk. Categories of Asynchronous Systems. PhD thesis, University of Sussex, 1987. Google Scholar
  6. Marek A. Bednarczyk. Hereditary history preserving bisimulations, or what is the power of the future perfect in program logics. Technical report, Polish Academy of Sciences, 1991. Google Scholar
  7. Sergiu Bursuc, Ross Horne, Sjouke Mauw, and Semen Yurkov. Provably unlinkable smart card-based payments. In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (CCS '23), pages 1392-1406, 2023. URL: https://doi.org/10.1145/3576915.3623109.
  8. Uli Fahrenberg, Christian Johansen, Georg Struth, and Krzysztof Ziemiański. Languages of higher-dimensional automata. Math. Struct. Comput. Sci., 31(5):575-613, 2021. URL: https://doi.org/10.1017/S0960129521000293.
  9. Riccardo Focardi and Roberto Gorrieri. Classification of security properties. In Foundations of Security Analysis and Design (FOSAD 2000), volume 2171 of lncs. springer, 2001. URL: https://doi.org/10.1007/3-540-45608-2_6.
  10. Rob J. van Glabbeek. The refinement theorem for ST-bisimulation semantics. In M. Broy and C.B. Jones, editors, Proceedings IFIP TC2 Working Conference on Programming Concepts and Methods, Sea of Gallilee, Israel, April 1990, pages 27-52. North-Holland, 1990. URL: http://kilby.stanford.edu/~rvg/pub/STbisimulation.pdf.
  11. Rob J. van Glabbeek. Bisimulations for higher dimensional automata. Email message, July 7, 1991, 1991. URL: http://theory.stanford.edu/~rvg/hda.
  12. Rob J. van Glabbeek. On the expressiveness of higher dimensional automata. Theoretical Computer Science, 356(3):265-290, 2006. Expressiveness in Concurrency. URL: https://doi.org/10.1016/j.tcs.2006.02.012.
  13. Rob J. van Glabbeek and Ursula Goltz. Refinement of actions and equivalence notions for concurrent systems. Acta Informatica, 37(4):229-327, 2001. URL: https://doi.org/10.1007/S002360000041.
  14. Rob J. van Glabbeek and Gordon D. Plotkin. Configuration structures. In Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science, pages 199-209. IEEE, 1995. URL: https://doi.org/10.1109/LICS.1995.523257.
  15. Rob J. van Glabbeek and Frits W. Vaandrager. Petri net models for algebraic theories of concurrency (extended abstract). In J.W. de Bakker, A.J. Nijman, and P.C. Treleaven, editors, Proceedings PARLE, Parallel Architectures and Languages Europe, Eindhoven, The Netherlands, June 1987, Vol. II: Parallel Languages, volume 259 of lncs, pages 224-242. springer, 1987. URL: https://doi.org/10.1007/3-540-17945-3_13.
  16. Ross Horne and Sjouke Mauw. Discovering epassport vulnerabilities using bisimilarity. Logical Methods in Computer Science, 17, 2021. URL: https://doi.org/10.23638/LMCS-17(2:24)2021.
  17. Ross Horne, Sjouke Mauw, and Semen Yurkov. When privacy fails, a formula describes an attack. Theoretical Computer Science, 959, 2023. URL: https://doi.org/10.1016/j.tcs.2023.113842.
  18. Iain Phillips and Irek Ulidowski. Event identifier logic. Mathematical Structures in Computer Science, 24(2), 2014. URL: https://doi.org/10.1017/S0960129513000510.
  19. Gordon D. Plotkin and Vaughan R. Pratt. Teams can see pomsets. In Doron A. Peled, Vaughan R. Pratt, and Gerard J. Holzmann, editors, Partial Order Methods in Verification, Proceedings of a DIMACS Workshop, Princeton, New Jersey, USA, July 24-26, 1996, volume 29 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 117-128. DIMACS/AMS, 1996. URL: https://doi.org/10.1090/DIMACS/029/07.
  20. Vaughan R. Pratt. Modeling concurrency with geometry. In Proc. Principles of Programming Languages (POPL'91), pages 311-322. ACM, 1991. URL: https://doi.org/10.1145/99583.99625.
  21. Cristian Prisacariu. Modal logic over higher dimensional automata. In CONCUR, volume 6269, pages 494-508, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_34.
  22. Cristian Prisacariu. The glory of the past and geometrical concurrency, 2013. Manuscript. Google Scholar
  23. Alexander Rabinovich and Boris A Trakhtenbrot. Behavior structures and nets. Fundamenta Informaticae, 11(4):357-403, 1988. URL: https://doi.org/10.3233/FI-1988-11404.
  24. Wolfgang Reisig. Petri Nets: An Introduction, volume 4 of EATCS Monographs on Theoretical Computer Science. springer, 1985. URL: https://doi.org/10.1007/978-3-642-69968-9.
  25. Glynn Winskel. Event structures. In W. Brauer, W. Reisig, and G. Rozenberg, editors, Petri Nets: Applications and Relationships to Other Models of Concurrency, lncs, pages 325-392. springer, 1987. URL: https://doi.org/10.1007/3-540-17906-2_31.
  26. Safa Zouari, Krzysztof Ziemiański, and Uli Fahrenberg. Bisimulations and logics for higher-dimensional automata. In Chutiporn Anutariya and Marcello M. Bonsangue, editors, Theoretical Aspects of Computing (ICTAC'24), pages 132-150. springer, 2025. URL: https://doi.org/10.1007/978-3-031-77019-7_8.
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