Forgetting Event Order in Higher-Dimensional Automata

TL;DR

This paper develops an order-independent semantics for higher-dimensional automata using interval ipomsets, resolving representational artifacts and aligning HDAs with other concurrency models.

Contribution

It introduces an order-free semantic framework for HDAs based on interval ipomsets, unifying categorical and combinatorial perspectives.

Findings

Traditional ST traces correspond to interval ipomsets.

Categorical isomorphism between presheaf and combinatorial presentations.

Order-free bisimulation characterized via ipomset isomorphism.

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 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.