Counter-Free Higher-Dimensional Automata for First-Order Interval-Pomset Languages

Abstract

We prove that a downward-closed language of interval pomsets over a finite alphabet and with a fixed width bound is first-order definable if and only if it is accepted by a finite counter-free higher-dimensional automaton. This establishes the converse conjectured by Erlich, Ledent and Ziemiański (CONCUR, 2026), whose algebraic characterisation identifies first-order definability with recognition by finite aperiodic categories. Given such a recognising category with aperiodicity exponent $h$ and a width bound $k$ , we effectively construct an automaton of dimension at most $k$ whose endpoint relations stabilise after $2k+h$ repetitions. The bound is uniform over all cells and endomorphism pomsets, including those with nonempty interfaces. Rather than completing an algebraic recogniser by adding faces, we use cells consisting of compatible diagrams of lower sets, with face maps given by restriction. A lattice extension criterion characterises paths between prescribed cells, and ordered interfaces allow the relevant repeated pomsets to be factored into fixed boundary pieces and an aperiodic middle factor. We also give an explicit two-dimensional example in which canonical suffix-residual completion introduces a period-two endpoint relation despite the existence of a counter-free realisation.

Note. This paper was generated entirely by AI, including MiMo, using an automated research pipeline developed by Chenghua Liu and Hanyu Li.

1 Introduction

Higher-dimensional automata describe concurrent executions by cells: a higher-dimensional cell records events that can remain active together, and its faces record their starts and terminations. Their languages consist of interval pomsets with interfaces and are closed under subsumption, so an accepted concurrent execution brings with it its sequential refinements. The language theory and Myhill–Nerode constructions of [6, 5] provide finite-state descriptions of these languages. An algebraic characterisation of first-order definability asks which of those descriptions can also avoid counting repeated executions.

For word languages, the connection between logic and the absence of counting is classical. Schützenberger’s theorem identifies star-free languages with recognition by finite monoids having no nontrivial subgroups [1]; first-order definability and suitable counter-free automata give equivalent descriptions, as developed in [2]. The concurrent setting adds geometric compatibility to these algebraic conditions. Amrane et al. [3] established the corresponding monadic second-order baseline: a language of interval pomsets is accepted by a finite HDA precisely when it is MSO-definable, has bounded width, and is closed under order refinement. The first-order fragment then asks for a finer restriction on the accepting automaton itself.

Erlich, Ledent and Ziemiański [4] identify first-order definability with recognition by finite aperiodic categories and show that counter-free HDAs give such recognisers. Their Conjecture 36 asks whether every downward-closed aperiodically recognised language has a counter-free HDA. We prove this converse and obtain an explicit stabilisation exponent. The difficulty is geometric: completing a recognising module to an HDA requires all faces of every cell, and the added faces can create periodic reachability relations. Section 5.2 of [4] exhibits this obstruction.

Our construction makes face completion part of the state space from the outset. A cell is an entire diagram of lower sets in an ordered recogniser, subject to inequalities for elementary starts and terminations. Faces are restrictions of diagrams, and joins of lower sets extend compatible boundary values. Together with the characteristic HDA associated with a pomset [6], this gives an exact criterion for a pomset-labelled path between two cells. To compare repeated executions, we factor the pomsets appearing in that criterion into fixed boundary pieces and an iterated middle piece. Ordered interfaces force every event that survives sufficiently many copies to remain in a fixed position. Aperiodicity of the recogniser then controls the whole endpoint relation. The diagram construction and this boundary factorisation are the two new ingredients.

Fix a finite alphabet $\Sigma$ and an integer $k\geq 0$ . We use the interval-pomset and HDA conventions of [4], recalled in Section 2. An ordered concurrency list, or conclist, is a finite linearly ordered set labelled by $\Sigma$ . Write $\mathcal{U}_{k}$ for the finite set of conclists of length at most $k$ , up to isomorphism, and $\mathsf{iiPoms}_{\leq k}$ for the category of interval pomsets of width at most $k$ with these interfaces. Here width is the maximum size of a precedence antichain; it is also called dimension in the HDA literature. Composition is gluing, written $P*Q$ , in execution order; for an endomorphism $P:U\to U$ , put $P^{0}=\mathrm{id}_{U}$ . First-order formulas have event variables, the binary predicates for precedence and event order, and unary predicates for each label and for the source and target interfaces. Definability is understood relative to $\mathsf{iiPoms}_{\leq k}$ . For an HDA $X$ , let

d_{X}(x,P)=\{y:\text{there is a path from $x$ to $y$ with label $P$}\}.

Counter-freeness means that a single integer $N\geq 1$ works for every cell $x$ and every endomorphism pomset $P:U\to U$ :

d_{X}(x,P^{N})=d_{X}(x,P^{N+1})\qquad(x\in X[U]).

(1)

This is a condition on the full reachability relation, including nondeterministic choices and cells which need not occur on accepting paths. On ordinary nondeterministic word automata, this endpoint-stabilisation condition is the notion called aperiodicity in [2, Definition 11.5]; we use the term counter-freeness of [4, Definition 34] throughout.

Theorem 1.1 (Counter-free realisation).

Let $L\subseteq\mathsf{iiPoms}_{\leq k}$ be downward closed under subsumption. Suppose that $L=G^{-1}(K)$ for a functor $G:\mathsf{iiPoms}_{\leq k}\to D$ into a finite category and a set $K\subseteq\operatorname{Mor}(D)$ . Suppose also that, for an integer $h\geq 1$ , every endomorphism $c$ of $D$ satisfies $c^{h}=c^{h+1}$ . Then there is a finite HDA $X$ of dimension at most $k$ with $\operatorname{Lang}(X)=L$ such that

d_{X}(x,P^{n})=d_{X}(x,P^{n+1})\qquad(n\geq 2k+h)

for every $U\in\mathcal{U}_{k}$ , every $x\in X[U]$ , and every $P\in\mathsf{iiPoms}_{\leq k}(U,U)$ . The construction is effective from the multiplication table of $D$ , the set $K$ , the object map of $G$ , and the images of elementary starters and terminators. Nonempty initial and final interfaces are allowed.

Corollary 1.2.

For a downward-closed language $L\subseteq\mathsf{iiPoms}_{\leq k}$ , the following are equivalent:

(i)
$L$ is recognised by a finite aperiodic category;
(ii)
$L$ is accepted by a finite counter-free HDA;
(iii)
$L$ is first-order definable.

The new implication is (i) $\Rightarrow$ (ii), proved below. The other implications are Theorem 33 and Proposition 35 of [4]. In particular, Theorem 1.1 proves Conjecture 36 with its stated notion of counter-freeness.

Section 2 constructs the ideal-diagram HDA. Section 3 proves recognition and the endpoint criterion, and Section 4 establishes stabilisation under iteration. Appendix A examines a canonical suffix-residual completion: an eight-cell counter-free HDA is transformed into an equivalent HDA with a period-two endpoint relation. The example explains why the choice of completion matters even when a counter-free realisation already exists.

2 From an ordered recogniser to an HDA

An interval pomset $P$ consists of a finite event set, a strict interval precedence order $<_{P}$ , an event order $\dashrightarrow_{P}$ , a labelling $\lambda_{P}:P\to\Sigma$ , and interfaces $S_{P},T_{P}$ . Source events are precedence-minimal and target events precedence-maximal. We record event order on precedence-incomparable pairs, as in [3, Section 2]: $\dashrightarrow_{P}$ is acyclic, and for distinct events exactly one of $e<_{P}f$ , $f<_{P}e$ , $e\dashrightarrow_{P}f$ , and $f\dashrightarrow_{P}e$ holds. It therefore restricts to a total order on every precedence antichain and, in particular, on every active interface. This order distinguishes positions even when concurrent events have the same label. We work up to isomorphism, retaining all this structure. The interval-order condition means that there are intervals $(s_{e},t_{e})$ such that $e<_{P}f$ precisely when $t_{e}<s_{f}$ .

A subsumption $P\sqsubseteq Q$ is a label- and interface-preserving bijection under which every precedence relation of $Q$ holds in $P$ , and the event orders agree on every pair incomparable in $P$ . Thus $P$ can have more precedence than $Q$ . Subsumption is compatible with gluing. Deleting events means taking the induced pomset and induced interfaces, unless new interfaces are specified explicitly.

Gluing $P:U\to V$ to $Q:V\to W$ identifies the corresponding ordered events of $T_{P}$ and $S_{Q}$ . The precedence relation is the union of the relations inside the two factors and $(P\setminus T_{P})\times(Q\setminus S_{Q})$ ; this union is transitive. Event order and labels are inherited from the factors, and the outer interfaces become $S_{P}$ and $T_{Q}$ . An identity pomset has all its events in both interfaces and has no precedence. A starter has every event in its target interface, and a terminator has every event in its source interface. Such pomsets are discrete. They are elementary when exactly one event is started or terminated.

Every interval pomset has an ST-decomposition into starters and terminators. Moreover, any two decompositions are related by splitting or merging consecutive starters or consecutive terminators, and by inserting or removing identities [4, Proposition 31]. In particular, the finitely many elementary pieces of width at most $k$ generate $\mathsf{iiPoms}_{\leq k}$ .

An HDA is a labelled precubical set with sets of initial and accepting cells. Write $\operatorname{ev}(x)$ for the conclist labelling a cell $x$ . For each conclist $U$ , its $U$ -cells have lower and upper face maps $\delta_{A}^{\varepsilon}$ , where $A\subseteq U$ and $\varepsilon\in\{0,1\}$ , removing the events in $A$ . The empty face map is the identity; removing disjoint sets in either order gives the same face, with the induced types understood. A directed path consists of starts from a lower face to a cell and terminations from a cell to an upper face. Its label is the gluing of the corresponding starters and terminators; a length-zero path at a $U$ -cell has label $\mathrm{id}_{U}$ . The language consists of labels of paths from initial to accepting cells. Initial and accepting cells may have positive dimension.

The face identities also ensure that a fixed ST-decomposition of a pomset determines its entire endpoint relation. Indeed, a sequence of starts into a cell can be merged by composing its lower face maps, and conversely can be split by taking the corresponding intermediate faces. The same argument uses upper faces for terminations. Thus each of the changes of ST-decomposition above preserves the possible endpoints. We may therefore use elementary steps without changing any reachability relation. In particular, gluing pomsets composes their endpoint relations.

For a cell of type $U$ , a face is obtained by assigning some events the status $0$ (not started) or $1$ (terminated). The remaining events have status $\star$ (active). Thus

\Theta_{U}=\{0,\star,1\}^{U},\qquad 0<\star<1,\qquad U_{\theta}=\theta^{-1}(\star)

indexes all faces of the standard $U$ -cube. Subconclists are transported to their canonical ordered representatives whenever needed.

Lemma 2.1 (Ordered recogniser).

Under the hypotheses of Theorem 1.1, there exist a finite category $C$ with objects $\mathcal{U}_{k}$ , a functor $F:\mathsf{iiPoms}_{\leq k}\to C$ that is the identity on objects, and $J\subseteq\operatorname{Mor}(C)$ such that:

(a)
$L=F^{-1}(J)$ ;
(b)
each hom-set of $C$ is partially ordered, and composition is monotone;
(c)
$J\cap C(U,V)$ is a lower set for all $U, V$ ;
(d)
$P\sqsubseteq Q$ implies $F(P)\leq F(Q)$ ;
(e)
every endomorphism of $C$ satisfies $c^{h}=c^{h+1}$ .

Proof.

First form the typed image category $A$ : its objects are the actual conclists, and

A(U,V)=\{G(P):P\in\mathsf{iiPoms}_{\leq k}(U,V)\},

with the source and target types retained as part of each arrow. This step allows $G$ to identify objects. Composition and identities come from $D$ . The category $A$ is finite, all its arrows have pomset representatives, and its endomorphisms satisfy the same exponent identity. Let $K_{A}$ be the accepting arrows in this typed image.

For parallel arrows $u, v$ of $A$ , put $u\preceq v$ if

avb\in K_{A}\ \Longrightarrow\ aub\in K_{A}\quad\text{for every composable pair of contexts }a,b\text{ in }A.

(2)

This preorder is compatible with multiplication on both sides. Quotienting by its symmetric part gives a category $C$ with partially ordered hom-sets. Membership in $K_{A}$ is constant on quotient classes, and its image $J$ is a lower set: use identity contexts in (2). The induced functor $F$ recognises $L$ . Exponent identities pass to this quotient.

To check (d), choose pomset representatives of $a$ and $b$ . If $P\sqsubseteq Q$ , then the same subsumption holds after gluing these representatives on the left and right. Downward closure of $L$ gives (2). The restriction to the typed image category ensures that every context used here has such a representative. ∎

This is the ordered version of the syntactic category. Only its finite ordered recognition properties will be needed.

We now use this ordered recogniser to construct cells whose faces are already present. Lower sets provide both the coefficients of the diagrams and the joins needed later to extend prescribed face values.

Fix an object $S\in\mathcal{U}_{k}$ . For $U\in\mathcal{U}_{k}$ , let

\mathcal{I}_{S}(U)=\operatorname{Down}(C(S,U))

be the set of all lower subsets, including the empty subset, ordered by inclusion. This is a finite complete lattice; joins are unions. For $P:U\to V$ , define

I\cdot P=\mathord{\downarrow}\{aF(P):a\in I\}\quad\in\mathcal{I}_{S}(V).

(3)

Lemma 2.2.

The operations (3) satisfy

I\cdot\mathrm{id}_{U}=I,\qquad(I\cdot P)\cdot Q=I\cdot(P*Q),\qquad\Bigl(\bigcup_{j}I_{j}\Bigr)\cdot P=\bigcup_{j}(I_{j}\cdot P).

Moreover, $P\sqsubseteq Q$ implies $I\cdot P\subseteq I\cdot Q$ .

Proof.

The identity assertion uses that $I$ is a lower set. Monotonicity of composition implies $\downarrow((\downarrow A)F(Q))=\downarrow(AF(Q))$ , proving associativity. Taking a lower closure commutes with unions. The last assertion follows from Lemma 2.1(d) and monotonicity of composition. ∎

Each elementary change $\theta\to\theta^{\prime}$ in $\Theta_{U}$ changes one coordinate from $0$ to $\star$ , or from $\star$ to $1$ . Give it the corresponding elementary starter or terminator label $\gamma_{\theta,\theta^{\prime}}:U_{\theta}\to U_{\theta^{\prime}}$ .

Definition 2.3 (Admissible diagram).

A $U$ -cell of $\mathcal{H}_{S}$ is a family

z=(z_{\theta})_{\theta\in\Theta_{U}},\qquad z_{\theta}\in\mathcal{I}_{S}(U_{\theta}),

satisfying, for each elementary change in $\Theta_{U}$ ,

z_{\theta}\cdot\gamma_{\theta,\theta^{\prime}}\ \subseteq\ z_{\theta^{\prime}}.

(4)

For $A\subseteq U$ , the face $\delta_{A}^{\varepsilon}z$ is the restriction obtained by fixing every coordinate of $A$ to $\varepsilon\in\{0,1\}$ . We write $z_{\star}$ for the value at the all-active face.

Restriction preserves (4). Restrictions on disjoint coordinate sets commute, so these face maps satisfy all precubical identities. We include every admissible diagram. There are finitely many of them.

Figure 1: A two-event ideal diagram has nine entries. The central entry is the colour of the two-dimensional cell; the other entries colour its faces. Every arrow satisfies the appropriate starter or terminator inequality (4).

The initial and accepting cells in the component $\mathcal{H}_{S}$ are

	$\displaystyle\bot_{S}$	$\displaystyle=\{z\in\mathcal{H}_{S}[S]:\mathrm{id}_{S}\in z_{\star}\},$		(5)
	$\displaystyle\top_{S}\cap\mathcal{H}_{S}[U]$	$\displaystyle=\{z\in\mathcal{H}_{S}[U]:z_{\star}\subseteq J\cap C(S,U)\}.$		(6)

Here $\mathrm{id}_{S}$ in (5) is the identity arrow of $C$ . Finally, put

X=\coprod_{S\in\mathcal{U}_{k}}\mathcal{H}_{S}

(7)

with these markings. Each component has its own copy of every diagram.

Remark 2.4 (Finiteness and construction size).

Let $r=|\mathcal{U}_{k}|$ and $m=|\operatorname{Mor}(C)|$ . A diagram of type $U$ has $3^{|U|}$ entries, each with at most $2^{m}$ choices. Therefore

|X|\leq r^{2}\,2^{m3^{k}}.

This coarse bound suffices for finiteness. The construction uses only finite sets, the order and multiplication table of $C$ , and the images of elementary starters and terminators.

3 Paths as extensions of face values

A diagram records all faces of a cell, so prescribing the endpoints of a path prescribes several values at once. We first express a pomset-labelled path as a map from its characteristic HDA. A lattice extension argument will then decide whether the prescribed values can coexist.

3.1 Characteristic configurations and colourings

We use the characteristic, or track, HDA introduced in [6], with the configuration presentation of [5, Definition 4.9]. For an interval pomset $P$ , let $\mathcal{B}(P)$ have as cells all configurations $c:P\to\{0,\star,1\}$ satisfying

e<_{P}f\ \text{ and }\ c(f)\neq 0\quad\Longrightarrow\quad c(e)=1.

(8)

Active events form an antichain; their induced labels and event order give the cell type. In particular, $\mathcal{B}(P)$ has dimension at most the width of $P$ . A face replaces selected active statuses by $0$ or $1$ . Condition (8) is preserved by both kinds of face. The distinguished cells are

\iota_{P}(e)=\begin{cases}\star&e\in S_{P},\\ 0&e\notin S_{P},\end{cases}\qquad\tau_{P}(e)=\begin{cases}\star&e\in T_{P},\\ 1&e\notin T_{P}.\end{cases}

The directed face graph has an arc from a lower face to its cell and from a cell to an upper face, changing one status at a time. It is acyclic: every arc strictly increases the sum of statuses when $0,\star,1$ are coded as $0,1,2$ .

The mapping property below is [5, Lemma 4.10], and the language description is [6, Proposition 92]. We include a direct proof for the labelled precubical sets used here.

Lemma 3.1 (Characteristic realisation).

For an interval pomset $P$ :

(a)
the labels of paths from $\iota_{P}$ to $\tau_{P}$ in $\mathcal{B}(P)$ are exactly $\{Q:Q\sqsubseteq P\}$ ;
(b)
for any HDA $Y$ and cells $x, y$ , a path labelled $P$ from $x$ to $y$ exists if and only if there is a type-preserving map of precubical sets $\mathcal{B}(P)\to Y$ sending $\iota_{P}$ to $x$ and $\tau_{P}$ to $y$ .

Proof.

Every path between the distinguished cells starts and terminates exactly the required events. Condition (8) forces all precedence relations of $P$ , and the event orders on its active cells are inherited from $P$ . Its label is consequently subsumed by $P$ . Conversely, an ST-decomposition of any $Q\sqsubseteq P$ runs through configurations satisfying (8). The orders on active events agree, so it defines the required path in $\mathcal{B}(P)$ . In particular, there is a path labelled $P$ .

A map as in (b) sends this path to the desired path in $Y$ . For the converse, expand a given $P$ -path into single-event steps and track its event occurrences through these steps. Regard the lifetime of each event $e$ as an interval $(s_{e},t_{e})$ along the path. Give all source events a common start before the first cell and all target events a common termination after the last cell. The remaining endpoints occur at the corresponding steps. These choices give

e<_{P}f\quad\Longleftrightarrow\quad t_{e}<s_{f},

and may be perturbed so that no start endpoint equals a termination endpoint.

Let $c$ be any cell of $\mathcal{B}(P)$ . Put

A_{c}=\{e:c(e)\neq 0\},\qquad B_{c}=\{e:c(e)\neq 1\}.

For $f\in A_{c}$ and $e\in B_{c}$ , condition (8) excludes $e<_{P}f$ . Hence

\max_{f\in A_{c}}s_{f}\ <\ \min_{e\in B_{c}}t_{e},

(9)

where an empty maximum or minimum is interpreted as $-\infty$ or $+\infty$ . Choose a cut between these quantities and away from endpoints. Every event active in $c$ is active at the cut. Events completed in $c$ have already started, and events unstarted in $c$ have not yet finished. Thus $c$ is a face of the cell of the given path at this cut. Cuts before or after the recorded path give faces of its initial or final cell, respectively.

The permitted cuts form an interval, so their recorded path cells occur consecutively. If two such cells are separated by a start, the changing event has status $0$ in $c$ ; if they are separated by a termination, it has status $1$ in $c$ . In either case the face images of $c$ agree, because the face map of that step commutes with removal of the other coordinates. The image of $c$ in $Y$ is consequently independent of the cut. If $c^{\prime}$ is a face of $c$ , any path cell containing $c$ also contains $c^{\prime}$ , and its face identities show that the two assignments commute with the face map $c\mapsto c^{\prime}$ . The distinguished cells have the prescribed images, proving (b). ∎

The interval cut in (9) is what lets one path determine a map on every characteristic cell. For the target $\mathcal{H}_{S}$ , specifying such a map reduces to assigning ideal values compatible with the face arcs. The following extension lemma gives the needed criterion.

Lemma 3.2 (Extension of inequalities).

Let $\Gamma$ be a finite acyclic directed graph. Associate a complete lattice $A_{v}$ to each vertex and a map preserving all joins to each arc. Write $f_{p}$ for the composite along a path $p$ . Prescribe values $a_{b}\in A_{b}$ at vertices in a subset $B$ . There is a colouring $a_{v}$ of all vertices which extends these values and satisfies every arc inequality if and only if

f_{p}(a_{b})\leq a_{b^{\prime}}\quad\text{for every path }p:b\longrightarrow b^{\prime}\text{ with }b,b^{\prime}\in B.

(10)

Length-zero paths are included.

Proof.

Necessity follows by composing inequalities and using monotonicity. For sufficiency, at every vertex $v$ take

\widehat{a}_{v}=\bigvee\{f_{p}(a_{b}):b\in B,\ p:b\longrightarrow v\}.

(11)

An empty join is the bottom element. The graph is finite and acyclic, so there are finitely many paths. Preservation of all joins includes the empty join; thus an arc sends the bottom value to the bottom value, as required when a vertex has no prescribed ancestor. At a prescribed vertex $b^{\prime}$ , the length-zero path supplies $a_{b^{\prime}}$ , and (10) bounds all other summands by $a_{b^{\prime}}$ . Hence $\widehat{a}_{b^{\prime}}=a_{b^{\prime}}$ . Applying an arc map to (11) distributes over its join. Every resulting summand is contributed by a path to the next vertex, so the arc inequality holds. ∎

Lemma 3.3 (Colourings and cubical maps).

A precubical map $\mathcal{B}(P)\to\mathcal{H}_{S}$ is equivalent to assigning a value $I_{c}\in\mathcal{I}_{S}(\operatorname{ev}(c))$ to every cell $c$ of $\mathcal{B}(P)$ such that

I_{c}\cdot\gamma\subseteq I_{c^{\prime}}

on every arc $c\xrightarrow{\gamma}c^{\prime}$ of its directed face graph. Prescribing the image of a cell prescribes precisely the colours of all its faces.

Proof.

From a map, take the top entry of each image diagram. Conversely, for a cell $c$ , the colours of its faces form an admissible diagram by the arc inequalities. These diagrams commute with face restriction. The two constructions are inverse. ∎

We first apply the extension criterion with only the initial value prescribed. Its least extension reaches exactly the lower set generated by the recognised arrow, which proves that the markings of $X$ recover $L$ .

Proposition 3.4.

The HDA $X$ of (7) accepts exactly $L$ .

Proof.

For soundness, take an accepting path in the component $\mathcal{H}_{S}$ . The image $F(\mathrm{id}_{S})$ belongs to its initial top value by (5). Along an elementary step labelled $Q$ , the top values satisfy $I\cdot Q\subseteq I^{\prime}$ , by (4); the same follows for multi-event steps by factorisation. Induction along the path shows that its complete label $P$ satisfies $F(P)\in I_{\mathrm{final}}$ . By (6), $F(P)\in J$ . Thus $P\in L$ .

For completeness, let $P\in L$ have source $S$ and target $T$ . In the face graph of $\mathcal{B}(P)$ prescribe only the value $\downarrow\mathrm{id}_{S}$ at $\iota_{P}$ , and use the least colouring (11), with the actions of Lemma 2.2. Acyclicity implies that the value at $\iota_{P}$ remains $\downarrow\mathrm{id}_{S}$ , since the only path from $\iota_{P}$ to itself is the length-zero path. By Lemma 3.1(a), the final value is

\bigcup_{Q\sqsubseteq P}(\downarrow\mathrm{id}_{S})\cdot Q=\bigcup_{Q\sqsubseteq P}\downarrow F(Q)=\downarrow F(P).

The last equality uses monotonicity for subsumption and the presence of $Q=P$ . This lower set is contained in $J$ because $P\in L$ . By Lemma 3.3, the colouring gives a map to $\mathcal{H}_{S}$ whose distinguished cells are initial and accepting. The image of the $P$ -path is accepting. ∎

3.2 Prescribed endpoints

The next step concerns paths between arbitrary cells, independently of the initial and accepting markings. Let $P:U\to V$ . A face $\alpha\in\Theta_{U}$ of its initial cube corresponds to the global configuration

c_{\alpha}(e)=\begin{cases}\alpha(e)&e\in S_{P},\\ 0&e\notin S_{P},\end{cases}

and a face $\beta\in\Theta_{V}$ of its final cube to

d_{\beta}(e)=\begin{cases}\beta(e)&e\in T_{P},\\ 1&e\notin T_{P}.\end{cases}

Here and below interface positions are identified with their actual events.

Call $(\alpha,\beta)$ compatible for $P$ when

\alpha(e)\leq\beta(e)\quad(e\in S_{P}\cap T_{P}),

(12)

in the order $0<\star<1$ . For a compatible pair define

	$\displaystyle D_{\alpha,\beta}$	$\displaystyle=\{e\in S_{P}:\alpha(e)=1\}\ \cup\ \{e\in T_{P}:\beta(e)=0\},$
	$\displaystyle S_{\alpha}$	$\displaystyle=\{e\in S_{P}:\alpha(e)=\star\},\qquad T_{\beta}=\{e\in T_{P}:\beta(e)=\star\}.$

The corner pomset $P[\alpha,\beta]$ is the induced pomset on $P-D_{\alpha,\beta}$ , with source $S_{\alpha}$ and target $T_{\beta}$ . Compatibility ensures these interfaces were not deleted. They remain minimal and maximal, so this is an interval pomset of dimension at most $k$ .

Lemma 3.5 (Corner paths).

If $(\alpha,\beta)$ is incompatible, there is no directed path from $c_{\alpha}$ to $d_{\beta}$ in $\mathcal{B}(P)$ . If it is compatible, the labels of such paths are exactly

\{Q:Q\sqsubseteq P[\alpha,\beta]\}.

Proof.

A directed path can only increase event statuses, proving the first claim. For a compatible pair, events deleted at the source are completed throughout the path, and events deleted at the target remain unstarted. All retained events have exactly the source and target statuses prescribed by the corner. Restriction therefore turns any such path into a refinement of the corner pomset.

Conversely, take an ST-path for the corner pomset, or any of its subsumed pomsets. Extend its configurations by keeping source-deleted events at $1$ and target-deleted events at $0$ . These prescriptions cannot conflict: a shared event prescribed $1$ at the source and $0$ at the target would violate compatibility. Source-deleted events are minimal in $P$ and target-deleted events maximal. Their fixed statuses consequently preserve (8) on every precedence pair involving a deleted event. All other precedence constraints hold by construction. This gives the required path in $\mathcal{B}(P)$ , including one whose label is the corner itself. ∎

Proposition 3.6 (Endpoint criterion).

Fix a coefficient source $S$ and cells $x\in\mathcal{H}_{S}[U]$ , $y\in\mathcal{H}_{S}[V]$ . Suppose $P:U\to V$ has an event outside $S_{P}\cup T_{P}$ . Then there is a path labelled $P$ from $x$ to $y$ if and only if

x_{\alpha}\cdot P[\alpha,\beta]\ \subseteq\ y_{\beta}\quad\text{for every pair compatible for $P$.}

(13)

Proof.

An event outside both interfaces has status $0$ on every face of the initial cube and status $1$ on every face of the final cube. The two cubes in $\mathcal{B}(P)$ are therefore disjoint, and no directed path goes from a face of the final cube to a face of the initial cube.

By Lemmas 3.1 and 3.3, the required path exists exactly when the face colours prescribed by $x$ and $y$ extend to all of $\mathcal{B}(P)$ . A path between two faces of the same boundary cube stays in that cube: every event outside the cube has equal initial and final statuses and thus cannot change. Its inequalities are already satisfied by the admissibility of $x$ or $y$ . Reverse paths between the boundary cubes do not exist. The remaining conditions in Lemma 3.2 are precisely those for forward paths from $c_{\alpha}$ to $d_{\beta}$ .

By Lemma 3.5, no condition is imposed for incompatible pairs. For a compatible pair, all labels are subsumed by $P[\alpha,\beta]$ , and this maximal label is itself realised. Monotonicity in Lemma 2.2 reduces all its path inequalities to the single inequality (13). ∎

Thus the joins used to fill the characteristic HDA reduce arbitrary cell-to-cell reachability to the finite family of corner inequalities (13). We can now study repeated executions by comparing the corresponding corner pomsets.

4 Stabilisation under iteration

We now establish the uniform bound. The case $k=0$ is immediate, since only the empty pomset and zero-dimensional cells occur. Assume $k\geq 1$ in this section.

Let $P:U\to U$ and write $r=|U|\leq k$ . An event belonging to both interfaces defines a partial map

f_{P}:\{1,\ldots,r\}\rightharpoonup\{1,\ldots,r\}:\quad i\longmapsto j

when source position $i$ and target position $j$ are that same event. This is an order-preserving partial injection: the two interface orders agree on their common events. Under gluing, survival through $n$ copies is described by $f_{P}^{n}$ . A nontrivial cycle would transport an event periodically among interface positions; the order rules out precisely this possibility.

Lemma 4.1 (Stable survival).

Let $E$ be the set of fixed positions of $f_{P}$ . For every $n\geq k$ , $f_{P}^{n}$ is the partial identity on $E$ . Thus the events shared by the two interfaces of $P^{n}$ are exactly those represented by $E$ , in their original positions.

Proof.

An order-preserving partial injection on a finite linear order has no cycle of length greater than one. For example, in a nontrivial cycle its least element is mapped to a larger one, whereas its predecessor in the cycle is larger and maps to that least element, contradicting order preservation. Injectivity also prevents a nontrivial chain from entering a fixed point. Every nonfixed chain therefore ends after at most $r$ applications. The remaining points are precisely the fixed points, proving the claim. ∎

An event corresponding to a position of $E$ occurs in every copy of $P$ and is identified throughout the gluing. We call these events persistent. In particular, deleting any subset $R$ of them produces an endomorphism $P-R:U-R\to U-R$ .

Lemma 4.2 (Separation of the boundary cubes).

If $P\neq\mathrm{id}_{U}$ , then $P^{n}$ has an event outside its two interfaces for every $n\geq k+1$ .

Proof.

Both interfaces have $r$ events. If $|P|=r$ , then they both consist of all events, and $P=\mathrm{id}_{U}$ . Otherwise $d=|P|-r\geq 1$ , and gluing gives

|P^{n}|=r+nd.

For $n\geq k+1$ , this is greater than $2r$ , whereas the union of the endpoint interfaces has at most $2r$ events. ∎

The preceding lemmas give both ingredients needed to compare endpoint criteria for large powers: the compatibility relation has stabilised, and the two boundary cubes are separated. We next isolate the effect of their face assignments inside fixed outer factors.

For $n\geq k$ , Lemma 4.1 makes compatibility of faces $\alpha,\beta\in\Theta_{U}$ independent of $n$ : the only comparisons in (12) are at positions of $E$ .

Lemma 4.3 (Boundary factorisation).

Fix $P:U\to U$ and a compatible pair $\alpha,\beta$ for its powers $P^{n}$ , $n\geq k$ . There are a subset $R$ of the persistent events and fixed pomsets $A_{\alpha,\beta}:U_{\alpha}\to U-R$ and $B_{\alpha,\beta}:U-R\to U_{\beta}$ , independent of $n$ , such that for every $n\geq 2k$ ,

P^{n}[\alpha,\beta]=A_{\alpha,\beta}*(P-R)^{n-2k}*B_{\alpha,\beta}.

(14)

The middle factor is an endomorphism of the reduced interface $U-R$ .

Proof.

Let

R=\{e\in E:\alpha(e)=1\text{ or }\beta(e)=0\}.

These are exactly the persistent events deleted by the corner operation. Write

P^{n}=H*P^{n-2k}*T,\qquad H=P^{k},\quad T=P^{k},

with fresh copies and the canonical gluing identifications. Besides $R$ , the corner deletes two sets: nonpersistent events in the source interface assigned $1$ by $\alpha$ , and nonpersistent events in the target interface assigned $0$ by $\beta$ .

Every event of the first set has disappeared before the target interface of $H$ , by Lemma 4.1. Thus it is contained wholly in $H$ and its deletion does not affect the gluing interface on the right of $H$ . Dually, every event of the second set is absent from the source interface of $T$ ; it belongs wholly to $T$ and its deletion does not affect the gluing interface on the left of $T$ . Remove these sets in their respective factors and remove $R$ throughout. Denote the resulting first and last factors by $H^{\prime}$ and $T^{\prime}$ . Their adjacent interfaces are both $U-R$ , and the middle factor becomes $(P-R)^{n-2k}$ . Induced deletion commutes with these gluings in this situation. Indeed, a persistent event is in both interfaces of every factor, so it is incomparable in precedence with every event of that factor and creates none of the additional cross-factor precedence relations. A nonpersistent event deleted in the first factor is a source event of the whole product, and one deleted in the last factor is a target event of the whole product. Neither can be an internal point of a precedence chain between retained events. Thus deleting them cannot remove a transitive witness needed for an order relation between retained events. The cross-factor relation in the definition of gluing restricts to exactly the cross-factor relation of the reduced factors. Labels and orders of concurrent events are inherited throughout. This proves the required commutation, including when the middle factor is an identity.

It remains to change the outside interfaces to the active positions of $\alpha$ and $\beta$ . Prepend to $H^{\prime}$ the starter which starts its remaining source events assigned $0$ by $\alpha$ . Append to $T^{\prime}$ the terminator which terminates its remaining target events assigned $1$ by $\beta$ . Such a starter or terminator changes the corresponding interface without adding an event or a precedence relation to the factor. The resulting pomsets are $A_{\alpha,\beta}$ and $B_{\alpha,\beta}$ . They are independent of $n$ and give exactly the event set, induced orders, labels, and interfaces of the corner pomset, proving (14). ∎

Corollary 4.4 (Stable corner images).

For every $P:U\to U$ , every compatible pair $\alpha,\beta$ , and every $n\geq 2k+h$ ,

F\bigl(P^{n}[\alpha,\beta]\bigr)=F\bigl(P^{n+1}[\alpha,\beta]\bigr).

(15)

Proof.

In (14), $F(P-R)$ belongs to the endomorphism monoid $C(U-R,U-R)$ . Apply its exponent identity to the middle factor; its exponent is $n-2k\geq h$ . The two fixed outside factors do not change. ∎

The corner images now stabilise with one exponent, so the endpoint criterion proves the theorem simultaneously for all pairs of cells.

Proof of Theorem 1.1.

Apply Lemma 2.1 and construct $X$ by Definition 2.3 and (5)–(7). It is finite, has dimension at most $k$ , and recognises $L$ by Proposition 3.4. For $k=0$ the assertion is immediate. Let $k\geq 1$ and put $N=2k+h$ .

Fix any component $\mathcal{H}_{S}$ , any $U$ -cells $x, y$ in it, and any $P:U\to U$ . The identity pomset leaves each cell unchanged, so assume $P\neq\mathrm{id}_{U}$ . For $n\geq N$ , Lemma 4.2 permits the use of the endpoint criterion for both $P^{n}$ and $P^{n+1}$ . By Lemma 4.1, the same pairs $\alpha,\beta$ are compatible for these two powers. For each such pair, Corollary 4.4 and (3) imply

x_{\alpha}\cdot P^{n}[\alpha,\beta]=x_{\alpha}\cdot P^{n+1}[\alpha,\beta].

The entire finite family of inequalities (13) is therefore identical. It follows that

y\in d_{X}(x,P^{n})\quad\Longleftrightarrow\quad y\in d_{X}(x,P^{n+1}).

There are no paths between distinct components. Since $x, y, P$ were arbitrary, this proves equality of the full reachability relations with the single exponent $N$ , and hence Definition 34 of [4].

All stages are effective. The typed image category is generated by the finitely many elementary ST arrows. The context tests defining its ordered quotient range over a finite category. Lower sets, diagrams, and their face restrictions can then be enumerated by finite computations. ∎

The exponent $2k+h$ is uniform over all cells and all endomorphism pomsets. The two $k$ terms come from discarding the transient interface histories at the two ends; no attempt has been made to optimise them. For a particular interface of size $r$ , the same argument yields $2r+h$ . When $r=0$ , a nonidentity pomset already has an internal event, and the unique corner condition uses its unmodified power, giving the bound $h$ directly.

The HDA can be large: the size bound in Remark 2.4 grows with both the recognising category and the number of cube faces. Finding smaller counter-free realisations, or minimisation procedures which preserve this property, remains a separate algorithmic question.

References

[1] Marcel-Paul Schützenberger. On finite monoids having only trivial subgroups. Information and Control, 8(2):190–194, 1965. doi:10.1016/S0019-9958(65)90108-7.
[2] Volker Diekert and Paul Gastin. First-order definable languages. In Jörg Flum, Erich Grädel, and Thomas Wilke, editors, Logic and Automata: History and Perspectives, Texts in Logic and Games, volume 2, pages 261–306. Amsterdam University Press, 2008. Author version.
[3] Amazigh Amrane, Hugo Bazille, Emily Clement, Uli Fahrenberg, Marie Fortin, and Krzysztof Ziemiański. Büchi–Elgot–Trakhtenbrot theorem for higher-dimensional automata. arXiv:2505.10461, 2025. arXiv:2505.10461.
[4] Enzo Erlich, Jérémy Ledent, and Krzysztof Ziemiański. Algebraic characterization of FO-definable languages of higher-dimensional automata. In 37th International Conference on Concurrency Theory (CONCUR 2026), Leibniz International Proceedings in Informatics, volume 391, pages 32:1–32:18. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2026. doi:10.4230/LIPIcs.CONCUR.2026.32. Full version (theorem numbering used here): arXiv:2605.25253v2.
[5] Uli Fahrenberg and Krzysztof Ziemiański. Myhill–Nerode theorem for higher-dimensional automata. Fundamenta Informaticae, 192(3–4):219–259, 2024. doi:10.3233/FI-242194.
[6] Uli Fahrenberg, Christian Johansen, Georg Struth, and Krzysztof Ziemiański. Languages of higher-dimensional automata. Mathematical Structures in Computer Science, 31(5):575–613, 2021. doi:10.1017/S0960129521000293.

Appendix A Counters introduced by canonical residual completion

The following unary, two-dimensional example starts with a counter-free HDA and produces an equivalent HDA with a period-two endpoint relation. Unlike the obstruction for a chosen module in [4, Section 5.2], this example uses the canonical suffix-residual module. We refine it by retaining the residuals obtained after deleting subsets of the target interface, as in [4, Lemma 25], and use the face maps of [4, Lemma 26]. This addresses the canonical construction suggested in the conclusion of that paper. The verification uses the explicit relation and profile tables below.

A.1 An eight-cell counter-free HDA

Let the alphabet be $\{a\}$ . The HDA $X_{0}$ has vertices $0,1$ , with $0$ the only initial and accepting vertex. Its edges, all labelled $a$ , are:

Edge	Lower endpoint	Upper endpoint
$e$	$0$	$1$
$f$	$1$	$0$
$\ell$	$1$	$1$

It has three squares, all of type $[a,a]$ . The two lower faces of each square coincide, as do the two upper faces:

Square	Both lower faces	Both upper faces
$s$	$e$	$f$
$t$	$\ell$	$\ell$
$u$	$\ell$	$f$

The lower endpoints of the two lower edges of each square agree, as do the upper endpoints of its two upper edges. For each square, the upper endpoint of a lower edge and the lower endpoint of an upper edge are both $1$ . These are the four precubical identities. There are eight cells in total. Write $C$ for the closed pomset consisting of two concurrent $a$ -events, and $\mathcal{P}^{+}$ for all nonempty unary interval pomsets of dimension at most two with empty source and target interfaces. Write $\varepsilon=\mathrm{id}_{\varnothing}$ , and let $C^{*}$ denote the finite gluing powers of $C$ , including $\varepsilon$ . Then

L=C^{*}\ \cup\ C^{*}a\mathcal{P}^{+}.

The sub-HDA consisting of $1,\ell,t$ has one cell of each unary type up to dimension two, so every elementary ST-decomposition of a closed pomset can be followed within it. To execute a nonempty pomset from $1$ to $0$ , follow this sub-HDA until the last start. If that start enters an edge, choose $f$ instead of $\ell$ ; the only remaining step is its termination at $0$ . If it enters a square, choose $u$ instead of $t$ ; the two remaining terminations pass through $f$ and end at $0$ . Thus the language from $1$ to $0$ is exactly $\mathcal{P}^{+}$ .

Starting at $0$ , the first edge is $e$ . Terminating it completes a single $a$ and reaches $1$ . Starting a second event instead enters $s$ ; its upper edge is $f$ , from which no further start is possible, so the two events must both terminate, returning to $0$ . This contributes exactly $C$ . Repeating this alternative proves the displayed formula for $L$ .

We next verify counter-freeness in the full sense of Definition 34 of [4]. Encode a relation by its row bitmasks: a subset of target positions is represented by the sum of the corresponding powers of two. For example, $(2,0,6)$ has rows $\{1\},\varnothing,\{1,2\}$ , with positions numbered from zero. For composable relations $R=(r_{i})$ and $S=(s_{j})$ , execution-order composition is given exactly by

(RS)_{i}=\mathop{\mathrm{OR}}_{j:\,r_{i}\,\mathrm{AND}\,2^{j}\neq 0}s_{j},

(16)

where $\mathrm{OR}$ and $\mathrm{AND}$ are bitwise union and intersection; the empty union is zero. With vertices ordered $(0,1)$ , edges ordered $(e,f,\ell)$ and squares ordered $(s,t,u)$ , the four elementary relations are

\sigma=(1,6),\qquad\tau=(2,1,2),\qquad\theta=(1,0,6),\qquad\eta=(2,4,2).

They respectively start from dimension zero to one, terminate from one to zero, start from one to two, and terminate from two to one. The two possible event positions give the same relations. Set

D=\theta\eta=(2,0,6),\qquad K=\tau\sigma=(6,1,6).

An elementary path from dimension one back to dimension one is a concatenation of excursions through dimension zero or dimension two. These have relations $K$ and $D$ , respectively. Since a fixed ST-decomposition determines the whole endpoint relation, every edge endomorphism relation is a product of $D, K$ . The table below gives the resulting monoid, its products on the right by the two generators, and the least $q\geq 1$ for which $R^{q}=R^{q+1}$ , using (16). Each displayed element is the indicated word in $D, K$ , and the table contains the identity and is closed under both right multiplications. It therefore exhausts the generated monoid.

Element	Row bitmasks	$\times D$	$\times K$	Exponent
$1$	$(1,2,4)$	$D$	$K$	1
$D$	$(2,0,6)$	$D^{2}$	$D K$	2
$K$	$(6,1,6)$	$K D$	$K^{2}$	3
$D^{2}$	$(0,0,6)$	$D^{2}$	$D^{2}K$	1
$D K$	$(1,0,7)$	$D$	$DK^{2}$	1
$K D$	$(6,2,6)$	$KD^{2}$	$K D K$	1
$K^{2}$	$(7,6,7)$	$K^{2}D$	$K^{3}$	2
$D^{2}K$	$(0,0,7)$	$D^{2}$	$D^{2}K$	1
$DK^{2}$	$(6,0,7)$	$KD^{2}$	$DK^{3}$	2
$KD^{2}$	$(6,0,6)$	$KD^{2}$	$DK^{3}$	1
$K D K$	$(7,1,7)$	$K D$	$K^{2}$	2
$K^{2}D$	$(6,6,6)$	$K^{2}D$	$K^{3}$	1
$K^{3}$	$(7,7,7)$	$K^{2}D$	$K^{3}$	1
$DK^{3}$	$(7,0,7)$	$KD^{2}$	$DK^{3}$	1

Every vertex endomorphism relation is the identity or $\sigma W\tau$ , with $W$ in this table. The resulting relations are exactly

(1,2),\ (2,3),\ (1,3),\ (3,3),\ (0,3),

with stabilisation exponent at most two. Every square endomorphism relation is the identity or $\eta W\theta$ . They are exactly

\begin{gathered}(1,2,4),\ (0,6,0),\ (1,6,1),\ (0,7,0),\\ (6,7,6),\ (1,7,1),\ (6,6,6),\ (7,7,7),\end{gathered}

also with exponent at most two. These lists exhaust endomorphism relations at every interface type, and hence

d_{X_{0}}(x,P^{3})=d_{X_{0}}(x,P^{4})\quad\text{for every cell $x$ and every $P:U\to U$.}

Thus $X_{0}$ is counter-free. Its language $L$ is aperiodically recognisable by Proposition 35 of [4], and it is downward closed as an HDA language.

A.2 Residual completion and its period-two relation

For a prefix $P:\varnothing\to U$ , define its suffix residual by

r(P)=P\backslash L=\{Q:U\to\varnothing\mid P*Q\in L\}.

Residuals act on the right by $r(P)\cdot Q=r(P*Q)$ . This is well-defined because equality of suffix languages is preserved by further prefix extension. The reachable residuals, sorted by target interface, are:

Interface	Nonempty residuals	Empty residual
$\varnothing$	$A,B,C_{0}$	$\perp_{0}$
$[a]$	$E, F, G$	$\perp_{1}$
$[a,a]$	$H, I$	$\perp_{2}$

Here $A=L$ , $B=\mathcal{P}^{+}$ and $C_{0}=\mathcal{P}^{+}\cup\{\varepsilon\}$ , represented by the vertex subsets $\{0\}$ , $\{1\}$ and $\{0,1\}$ , respectively. The subscript distinguishes $C_{0}$ from the concurrent pair $C$ . The residuals $E, F, G$ are the suffix languages from the cell sets $\{e\}$ , $\{f\}$ and $\{f,\ell\}$ ; $\{e,f,\ell\}$ has the same suffix language as the last set. Residuals $H, I$ come from $\{s\}$ and $\{t,u\}$ ; the set $\{s,t,u\}$ is equivalent to the latter. The complete elementary action is

\begin{array}[]{ll}\text{start }\varnothing\to[a]:&A\mapsto E,\ B\mapsto G,\ C_{0}\mapsto G,\ \perp_{0}\mapsto\perp_{1},\\ \text{terminate }[a]\to\varnothing:&E\mapsto B,\ F\mapsto A,\ G\mapsto C_{0},\ \perp_{1}\mapsto\perp_{0},\\ \text{start }[a]\to[a,a]:&E\mapsto H,\ F\mapsto\perp_{2},\ G\mapsto I,\ \perp_{1}\mapsto\perp_{2},\\ \text{terminate }[a,a]\to[a]:&H\mapsto F,\ I\mapsto G,\ \perp_{2}\mapsto\perp_{1}.\end{array}

The last two rows hold for either event position. The initial state is $A$ ; the accepting states are $A,C_{0}$ . To verify completeness, start with the vertex subset $\{0\}$ and propagate subsets by the four elementary relations. The subsets represented above, together with the empty subsets, are closed under these operations. The identifications $\{f,\ell\}\sim\{e,f,\ell\}$ and $\{t,u\}\sim\{s,t,u\}$ preserve both transitions and acceptance, so they preserve all suffix languages. All displayed residuals are reachable. They are distinct: zero-dimensional states are separated by the empty suffix or $a$ ; one-dimensional states by termination or termination followed by $a$ ; and $H, I$ by two terminations followed by $a$ . Every nonempty residual has an accepting suffix, separating it from the empty residual.

To define lower faces, retain the deletion profile

v(P)=\bigl(r(P-A^{\prime})\bigr)_{A^{\prime}\subseteq T_{P}}.

For completeness, the following rules determine its update under every elementary step. If a starter introduces a new event $e$ , a profile coordinate that deletes $e$ is the old coordinate deleting the remaining specified events. A coordinate that keeps $e$ is obtained from the old coordinate by the corresponding starter on its reduced interface. If a terminator removes an active event $e$ , the new coordinate indexed by $A^{\prime}\subseteq T_{P}\setminus\{e\}$ is the old coordinate indexed by $A^{\prime}$ , acted on by termination of $e$ in the reduced interface. These rules follow by deleting the indicated events in the gluing definition, and use only the residual action table above.

Call a profile live when its first coordinate is a nonempty residual. The live profiles are

\begin{array}[]{ll}0:&(A),\quad(B),\quad(C_{0}),\\ 1:&e^{\prime}=(E,A),\quad f^{\prime}=(F,B),\quad g^{\prime}=(G,B),\quad h^{\prime}=(G,C_{0}),\\ 2:&s^{\prime}=(H,E,E,A),\quad t^{\prime}=(I,G,G,B),\quad u^{\prime}=(I,G,G,C_{0}).\end{array}

The coordinates in dimension two mean: delete neither event, the first, the second, or both. Here vertex names also denote their one-entry profiles. The update rules give the following finite table of prefix extensions; these are not the upward face transitions of the completed HDA.

Profile	Append one start	Append one termination
$A$	$e^{\prime}$	—
$B$	$g^{\prime}$	—
$C_{0}$	$h^{\prime}$	—
$e^{\prime}$	$s^{\prime}$	$B$
$f^{\prime}$	dead	$A$
$g^{\prime}$	$t^{\prime}$	$C_{0}$
$h^{\prime}$	$u^{\prime}$	$C_{0}$
$s^{\prime}$	—	$f^{\prime}$
$t^{\prime}$	—	$h^{\prime}$
$u^{\prime}$	—	$h^{\prime}$

A dash means that the step is unavailable within the dimension bound; “dead” means that the first coordinate is empty. When two event positions are possible, both give the listed profile. Every listed profile is reachable from $A$ by this table. Conversely, a prefix with empty residual keeps empty residual under every extension. Induction on an elementary ST-decomposition therefore shows that these are all live profiles. This proves exhaustiveness without enumerating dead profiles.

In the coherent residual completion, a lower face restricts the profile to coordinates that delete the specified event. An upper face is given by its termination update. Thus the vertices are $A,B,C_{0}$ , and the four edges have the following faces:

Edge	Lower endpoint	Upper endpoint
$e^{\prime}=(E,A)$	$A$	$B$
$f^{\prime}=(F,B)$	$B$	$A$
$g^{\prime}=(G,B)$	$B$	$C_{0}$
$h^{\prime}=(G,C_{0})$	$C_{0}$	$C_{0}$

The squares $s^{\prime},t^{\prime},u^{\prime}$ have, respectively, the pairs of lower and upper faces $(e^{\prime},f^{\prime})$ , $(g^{\prime},h^{\prime})$ , and $(h^{\prime},h^{\prime})$ , with both faces of each kind coinciding. The initial vertex is $A$ , and the accepting vertices are $A,C_{0}$ . The displayed cells are closed under faces, so they form an HDA $Y$ .

We can check $\operatorname{Lang}(Y)=L$ directly. The sub-HDA $C_{0},h^{\prime},u^{\prime}$ executes every closed pomset of width at most two. From $B$ , every nonempty such pomset can reach $C_{0}$ : use $g^{\prime}$ for the first edge and, if a second event starts before the first termination, use $t^{\prime}$ for the first square. The first termination then enters $C_{0}$ or $h^{\prime}$ , after which the remaining steps stay in that sub-HDA. Since $B$ is not accepting, its accepting language is exactly $\mathcal{P}^{+}$ . From $A$ , the first edge $e^{\prime}$ either terminates at $B$ , contributing $a$ , or enters $s^{\prime}$ and then passes through $f^{\prime}$ back to $A$ , contributing $C$ . The same decomposition used for $X_{0}$ gives $\operatorname{Lang}(Y)=C^{*}\cup C^{*}a\mathcal{P}^{+}=L$ .

Although this completion preserves the language, it changes the effect of iterating a closed letter. In vertex order $(A,B,C_{0})$ , the ordinary closed letter $a$ acts in $Y$ by

R_{a}=(2,5,4),\qquad A\longrightarrow B,\quad B\longrightarrow\{A,C_{0}\},\quad C_{0}\longrightarrow C_{0}.

Consequently,

$\displaystyle d_{Y}(A,a)$	$\displaystyle=\{B\},$
$\displaystyle d_{Y}(A,a^{2n})$	$\displaystyle=\{A,C_{0}\}$	$\displaystyle(n\geq 1),$
$\displaystyle d_{Y}(A,a^{2n+1})$	$\displaystyle=\{B,C_{0}\}$	$\displaystyle(n\geq 1).$

There is no stabilisation exponent, so $Y$ is not counter-free. The same counter remains in the full completion. Indeed, an upper face of a dead profile is dead because its first coordinate is acted on by termination. A start from a dead cell cannot enter a live cell either, since every lower face of a live cell occurs in the displayed live sub-HDA. No path can therefore return from a dead cell to these vertices. Adding the omitted profiles does not change the displayed endpoint sets on $A,B,C_{0}$ . Thus canonical suffix residuals, even with the specified coherent deletion-profile refinement, need not yield a counter-free HDA, although $X_{0}$ recognises the same language with exponent three.