Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Kleene Theorem for Higher-Dimensional Automata

Uli Fahrenberg, Christian Johansen, Georg Struth, Krzysztof Ziemiański

TL;DR

The paper proves a Kleene theorem for higher-dimensional automata (HDAs), showing that languages recognised by finite HDAs are exactly the rational, subsumption-closed interval ipomset languages. It introduces HDAs with interfaces (iHDAs), recasts HDAs as presheaves on labelled precube categories, and develops topology-inspired tools (cylinders, resolutions, closures) and a gluing toolbox to handle serial and parallel compositions, as well as Kleene plus. Key contributions include a precise relationship between HDAs and ipomsets, a tensor product framework for parallel composition, and a constructive pathway from regular languages to rational ones through novel automata and cube-based reasoning. The results advance a unified, topology-informed approach to non-interleaving concurrency and suggest templates for Kleene theorems in other models.

Abstract

We prove a Kleene theorem for higher-dimensional automata. It states that the languages they recognise are precisely the rational subsumption-closed sets of finite interval pomsets. The rational operations on these languages include a gluing composition, for which we equip pomsets with interfaces. For our proof, we introduce higher-dimensional automata with interfaces, which are modelled as presheaves over labelled precube categories, and develop tools and techniques inspired by algebraic topology, such as cylinders and (co)fibrations. Higher-dimensional automata form a general model of non-interleaving concurrency, which subsumes many other approaches. Interval orders are used as models for concurrent and distributed systems where events extend in time. Our tools and techniques may therefore yield templates for Kleene theorems in various models and applications.

Kleene Theorem for Higher-Dimensional Automata

TL;DR

The paper proves a Kleene theorem for higher-dimensional automata (HDAs), showing that languages recognised by finite HDAs are exactly the rational, subsumption-closed interval ipomset languages. It introduces HDAs with interfaces (iHDAs), recasts HDAs as presheaves on labelled precube categories, and develops topology-inspired tools (cylinders, resolutions, closures) and a gluing toolbox to handle serial and parallel compositions, as well as Kleene plus. Key contributions include a precise relationship between HDAs and ipomsets, a tensor product framework for parallel composition, and a constructive pathway from regular languages to rational ones through novel automata and cube-based reasoning. The results advance a unified, topology-informed approach to non-interleaving concurrency and suggest templates for Kleene theorems in other models.

Abstract

We prove a Kleene theorem for higher-dimensional automata. It states that the languages they recognise are precisely the rational subsumption-closed sets of finite interval pomsets. The rational operations on these languages include a gluing composition, for which we equip pomsets with interfaces. For our proof, we introduce higher-dimensional automata with interfaces, which are modelled as presheaves over labelled precube categories, and develop tools and techniques inspired by algebraic topology, such as cylinders and (co)fibrations. Higher-dimensional automata form a general model of non-interleaving concurrency, which subsumes many other approaches. Interval orders are used as models for concurrent and distributed systems where events extend in time. Our tools and techniques may therefore yield templates for Kleene theorems in various models and applications.
Paper Structure (17 sections, 54 theorems, 90 equations, 22 figures)

This paper contains 17 sections, 54 theorems, 90 equations, 22 figures.

Table of Contents

  1. Introduction
  2. Overview
  3. Higher-dimensional automata
  4. Pomsets with interfaces
  5. Executions of higher-dimensional automata
  6. Kleene theorem
  7. Regular languages are rational
  8. Track objects and tracks
  9. Tensor product of higher-dimensional automata
  10. Higher-dimensional automata with interfaces
  11. Higher-dimensional automata with and without interfaces
  12. Cylinders
  13. Gluing toolbox
  14. Sequential composition of simple iHDAs
  15. Kleene plus
  16. ...and 2 more sections

Key Result

Lemma 3.4

For each pc-set $X$ and $x\in X[U]$ there is a unique pc-map $\iota_x:\square^U\to X$ such that $\iota_x([\emptyset|U|\emptyset])=x$. Hence there is a canonical bijection $X[U]\cong \square\text{Set}(\square^U,X)$.∎

Figures (22)

  • Figure 1: HDA with two 2-dimensional cells $x$ and $y$ modelling the parallel execution of $a$ and $(b c)^*$ on the left, an unfolded view in the middle and three accepting paths of this automaton on the right.
  • Figure 2: Three representations of a two-dimensional HDA.
  • Figure 3: Paths in an HDA
  • Figure 4: Interval ipomset of path in HDA
  • Figure 5: Conclists $1\dashrightarrow 2\dashrightarrow 3$ and $1\dashrightarrow 2\dashrightarrow \dotsc \dashrightarrow 6$ with lo-map $\partial_{\{3,4,6\}}$ and labelling function $\lambda$ into $\Sigma=\{a,b,c,d,e\}$.
  • ...and 17 more figures

Theorems & Definitions (115)

  • Example 2.1
  • Remark 2.2
  • Example 2.3
  • Example 2.4
  • Example 2.5
  • Remark 3.1
  • Example 3.2
  • Example 3.3
  • Lemma 3.4
  • Example 4.1
  • ...and 105 more