DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2026.49

Bisimulations and Modal Logics for Higher Dimensional Automata

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

Published in: LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{zouari_et_al:LIPIcs.CONCUR.2026.49,
  author =	{Zouari, Safa and van Glabbeek, Rob and Ziemia\'{n}ski, Krzysztof},
  title =	{{Bisimulations and Modal Logics for Higher Dimensional Automata}},
  booktitle =	{37th International Conference on Concurrency Theory (CONCUR 2026)},
  pages =	{49:1--49:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-447-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{391},
  editor =	{Sokolova, Ana and Totzke, Patrick},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.49},
  URN =		{urn:nbn:de:0030-drops-273809},
  doi =		{10.4230/LIPIcs.CONCUR.2026.49},
  annote =	{Keywords: higher-dimensional automata, bisimilarity, history-preserving bisimulation, modal logic, concurrency theory}
}

Document

DOI: 10.4230/LIPIcs.LICS.2026.84

Forgetting Event Order in Higher-Dimensional Automata

Authors: Safa Zouari

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract

Higher-dimensional automata (HDAs) provide a geometric model of true concurrency, yet their standard formulation encodes an artificial total order on events. This representational artifact causes a fundamental mismatch between the combinatorial structure of HDAs and their observable behaviour, leading to logical asymmetries and complicating the application of categorical tools. In this paper, we resolve this tension by developing a semantics for HDAs that is independent of event order, based on interval ipomsets (partially ordered multisets with interfaces) that preserve only precedence and concurrency. We prove that for any HDA, the traditional ST–trace of an execution path corresponds precisely to its associated interval ipomset. On the structural side, we show that the presheaf-theoretic presentation with an unordered base and the combinatorial presentation of symmetric HDAs are categorically isomorphic. Finally, by characterizing ST- and hereditary history-preserving (hhp) bisimulation via ipomset isomorphism, we provide a unified, order-free foundation for HDA semantics. Our results resolve several ambiguities in the literature: they provide the necessary path-category structure to canonically apply the Open Maps framework, eliminate representational artifacts in temporal and modal logics, and bridge systematic mismatches between HDAs and other models of concurrency such as Petri nets.

Cite as

Safa Zouari. Forgetting Event Order in Higher-Dimensional Automata. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 84:1-84:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{zouari:LIPIcs.LICS.2026.84,
  author =	{Zouari, Safa},
  title =	{{Forgetting Event Order in Higher-Dimensional Automata}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{84:1--84:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.84},
  URN =		{urn:nbn:de:0030-drops-268711},
  doi =		{10.4230/LIPIcs.LICS.2026.84},
  annote =	{Keywords: higher-dimensional automata, true concurrency, pomsets with interfaces, interval pomsets, pomsets, presheaf semantics, bisimulation, event order, ST-trace}
}

Search Results

Documents authored by Zouari, Safa

Bisimulations and Modal Logics for Higher Dimensional Automata

Abstract

Cite as

Forgetting Event Order in Higher-Dimensional Automata

Abstract

Cite as

Thanks for your feedback!

Could not send message