Conceitos Básicos
The languages recognized by higher-dimensional automata are precisely the rational subsumption-closed sets of finite interval pomsets.
Resumo
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.