Closure and Decision Properties for Higher-Dimensional Automata

TL;DR

This work advances higher-dimensional automata by adapting a pumping lemma to ipomset languages and proving that regular ipomset languages are closed under intersection while inclusion is decidable. It introduces ST-automata as a bridge to ordinary word automata, establishing a translation that preserves essential properties and enabling decidability results for regular languages. The paper also analyzes determinism and ambiguity, showing decidability of determinism but the existence of regular languages with unbounded ambiguity, and provides a complete one-letter language characterization via ultimately periodic functions. To address complement, it defines width-bounded complements that preserve regularity, while plain complements may fail closure properties. Overall, the results give a robust automata-theoretic toolkit for HDAs and open questions on recognizability and weighted or timed extensions.

Abstract

We report some further developments regarding the language theory of higher-dimensional automata (HDAs). Regular languages of HDAs are sets of finite interval partially ordered multisets (pomsets) with interfaces. We show a pumping lemma which allows us to expose a class of non-regular languages. Concerning decision and closure properties, we show that inclusion of regular languages is decidable (hence is emptiness), and that intersections of regular languages are again regular. On the other hand, complements of regular languages are not always regular. We introduce a width-bounded complement and show that width-bounded complements of regular languages are again regular. We also study determinism and ambiguity. We show that it is decidable whether a regular language is accepted by a deterministic HDA and that there exists regular languages with unbounded ambiguity. Finally, we characterize one-letter deterministic languages in terms of utlimately periodic functions.

Figures (9)

• Figure 1: Petri net and HDA models distinguishing interleaving (left) from non-interleaving (right) concurrency. Left: models for $a. b+ b. a$; right: models for $a\mathrel{\|} b$.
• Figure 2: Activity intervals of events (top) and corresponding ipomsets (bottom), cf. Example \ref{['ex:subsu']}. Full arrows indicate precedence order; dashed arrows indicate event order; bullets indicate interfaces.
• Figure 3: Gluing and parallel composition of ipomsets.
• Figure 4: Ipomset of size $3.5$ and two of its step decompositions.
• Figure 5: A two-dimensional HDA $X$ on $\Sigma=\{a, b\}$, see Example \ref{['ex:hda']}.

Theorems & Definitions (79)

• Lemma 1: DBLP:journals/corr/abs-2210-08298
• Lemma 2
• proof
• Lemma 3: DBLP:conf/concur/FahrenbergJSZ22
• Theorem 4: DBLP:journals/corr/abs-2210-08298
• Remark 5
• Lemma 6
• Lemma 7: DBLP:journals/corr/abs-2210-08298
• Lemma 8
• proof