Forgetting Event Order in Higher-Dimensional Automata

TL;DR

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

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.

Figures (6)

• Figure 1: Example of conclist maps $(f,\varepsilon):U \to V$ (on the left) and $(g,\zeta):V \to W$ (on the right).
• Figure 2: Illustration of $(g,\zeta)\circ(f,\varepsilon):U \to W$, the composition of the conclist maps of Fig \ref{['fig: exam of conclist maps']}.
• Figure 3: Precubical set $X$ with two 2-dimensional cells
• Figure 4: Interval ipomsets (below) with their corresponding interval representations (above). An event with a dot on the left (resp. on the right) is an element of a source (resp. target) interface. Full arrows indicate precedence order.
• Figure 5: HDA $\mathcal{X}$ on the left with its symmetrizer $S\mathcal{X}$ on the left.

Theorems & Definitions (63)

• Definition 2.1: Concurrency list
• Definition 2.2
• Definition 2.3: Concurrency set
• Definition 2.4
• Lemma 2.5
• proof
• Definition 2.6
• Lemma 2.7
• proof
• Lemma 2.8