Core Concepts
The languages recognized by higher-dimensional automata are precisely the rational subsumption-closed sets of finite interval pomsets.
Abstract
The paper introduces higher-dimensional automata (HDAs) as a general geometric model for non-interleaving concurrency. HDAs consist of cells representing concurrent events, with face maps indicating when events start or terminate.
The key insights are:
Executions of HDAs are characterized by interval pomsets, which capture the precedence and event order of concurrent events.
The languages recognized by HDAs are subsumption-closed sets of interval pomsets.
The rational operations on these languages include union, gluing (serial) composition, parallel composition, and (serial) Kleene plus.
The paper proves a Kleene theorem, showing that the rational languages are precisely the regular ones (recognized by finite HDAs).
The proof involves several technical developments, including:
Modeling HDAs as presheaves on a "labelled precube" category
Introducing HDAs with interfaces to track active events
Using tools from algebraic topology, such as cylinders and (co)fibrations, to decompose HDA maps
These techniques and the Kleene theorem provide a foundational result for reasoning about concurrent systems modeled by HDAs.