Variants of Higher-Dimensional Automata

TL;DR

This work surveys and unifies several variants of higher-dimensional automata (HDAs) through a presheaf framework, addressing the rigidity of HDAs by introducing iHDAs, pHDAs, rHDA/ srHDA, ST-automata, and cone-like constructs. It shows that languages fall into two classes: those closed under subsumption (HDAs and iHDAs) and a broader class for the other variants, and it establishes a Kleene theorem for pHDAs along with a determinization result, demonstrating that partial HDAs are amenable to standard automata-theoretic techniques. The paper also builds a network of translations and adjunctions (closure/resolution, etc.) between models, enabling systematic reasoning about concurrency via ipomsets and their gluing. Overall, it provides a coherent, category-theoretic foundation for multiple HDA variants, clarifying their expressive power, language behavior, and automata-theoretic properties, with implications for Petri-net translations and concurrent system modeling.

Abstract

The theory of higher-dimensional automata (HDAs) has seen rapid progress in recent years, and first applications, notably to Petri net analysis, are starting to show. It has, however, emerged that HDAs themselves often are too strict a formalism to use and reason about. In order to solve specific problems, weaker variants of HDAs have been introduced, such as HDAs with interfaces, partial HDAs, ST-automata or even relational HDAs. In this paper we collect definitions of these and a few other variants into a coherent whole and explore their properties and translations between them. We show that with regard to languages, the spectrum of variants collapses into two classes, languages closed under subsumption and those that are not. We also show that partial HDAs admit a Kleene theorem and that, contrary to HDAs, they are determinizable.

Figures (19)

• Figure 1: Variants of HDAs together with their presheaf formulations (lax presheaves denoted $\mathrel{\tilde{\rightarrow}}$).
• Figure 2: Two ipomsets and an iconclist. Full arrows indicate precedence order, dashed arrows event order, and bullets, interfaces.
• Figure 3: Ipomset (left) and its sparse step decomposition.
• Figure 4: An iconclist map. Annotations $A$ and $B$ indicate events that have not yet started resp. terminated. Being in the target interface, $c\vcenter{\hbox{\tiny $\bullet$}}$ must be marked $A$ rather than $B$.
• Figure 5: pHDA such that $\delta_a^1 (\delta_b^1(x))$ is not defined.

Theorems & Definitions (54)

• definition 1
• definition 2
• definition 3.3(s)p/r
• definition 3.4
• definition 3.5
• definition 3.6
• lemma 1
• proof
• lemma 2
• proof