Forgetting Event Order in Higher-Dimensional Automata
This work provides a unified, order-free foundation for HDA semantics, resolving critical ambiguities and bridging mismatches with other concurrency models, which is significant for researchers working with true concurrency models.
The authors address the issue of artificial total order on events in Higher-Dimensional Automata (HDAs) by developing an event-order-independent semantics based on interval ipomsets. They prove that traditional ST traces correspond to these ipomsets and establish categorical isomorphism between presheaf theoretic and symmetric HDA presentations.
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 behavior, 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 critical 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.