Higher-Dimensional Automata: Extension to Infinite Tracks

We fix a finite alphabet $\mathrm{\Sigma }$. An ipomset (over $\mathrm{\Sigma }$) is a structure consisting of a finite set of events $P$, two strict partial orders: the precedence order, and $⇢$ the event order, a set $S\subseteq P$ of source interfaces, a set $T\subseteq P$ of target interfaces such that the elements of $S$ are -minimal and those of $T$ are -maximal, and a labeling function $\lambda :P\to \mathrm{\Sigma }$. In addition, we require that the relation is total, but not necessarily an order. In fact, if we have and $y⇢x$, then is not an order.

For the purpose of notation, we use ${}_S{P}_T$ for an ipomset , or refer to it by its set of events $P$ and to its components by adding the subscript _P.

We highlight two special cases of ipomsets: conclists $(U,⇢,\lambda )$ where $S_U=T_U=\mathrm{\varnothing }$ and hence $⇢$ total, with $\mathrm{\square }$ the set of conclists, and identities ${\mathrm{𝗂𝖽}}_U{=}_U{U}_U$ where $S_U=T_U=U$ and , with $\mathrm{𝖨𝖽}$ the set of identities. We call ${\mathrm{𝗂𝖽}}_{\mathrm{\varnothing }}$ the empty conclist/identity. Note that for any ipomset $P$, $S_P=(S,{⇢}_{\upharpoonleft S\times S},{\lambda }_{\upharpoonleft S})$ and $T_P=(T,{⇢}_{\upharpoonleft T\times T},{\lambda }_{\upharpoonleft T})$, where “_↿” denotes restriction, are conclists. An ipomset $P$ is said to be interval (called iipomset) if is an interval order, i.e. if for all $w,x,y,z\in P$, if and , then or .

Let $P$ and $Q$ be two ipomsets. We say that $Q$ subsumes $P$ (written $P⊑Q$) if there is a bijection $f:P\to Q$ (a subsumption) such that ${\lambda }_Q\circ f={\lambda }_P$, $f(S_P)=S_Q$, and $f(T_P)=T_Q$, and $\forall x,y\in P$ such that $x{\nless }_{P}y$ and $y{\nless }_{P}x$, we have $x{⇢}_{P}y\Rightarrow f(x){⇢}_{Q}f(y)$. Informally speaking, $P$ is more precedence ordered than $Q$.

An isomorphism of ipomsets is an invertible subsumption (whose inverse is again a subsumption); isomorphic ipomsets are denoted $P\cong Q$. Due to the totality of , isomorphisms between ipomsets are unique [4], so we may switch freely between ipomsets and their isomorphism classes. The set of ipomsets is denoted $\mathrm{𝗂𝖯𝗈𝗆𝗌}$, and the set of interval ipomsets is written $\mathrm{𝗂𝗂𝖯𝗈𝗆𝗌}$.

In an ipomset $P$, a chain is a subset of $P$ totally ordered by . An antichain $A$ of $P$ is such that . Hence $A$ is totally ordered by ${⇢}_P$. The width of $P$ is .

Similarly to ipomsets, an $\omega$-ipomset is a structure of the form . The only changes are that $P$ is countably infinite and there is no target interface. However, let ${\mathrm{\Omega }}_P$ denote the set of all -maximal elements. This is not similar to a target interface: even if ${\mathrm{\Omega }}_P$ represents unfinished events, terminating them (by trying to glue an ipomset after $P$) may cause chains greater than $\omega$.

For the remainder of the paper, we focus on a subclass of $\omega$-ipomsets.

The first point is here to forbid $\omega$-ipomsets with chains greater than $\omega$, and therefore extend properly classical $\omega$-words and $\omega$-pomsets [31]. It is a classical property required in event structures (see [44] for example). The second point is to avoid an infinite number of concurrent events. This condition implies in particular that $S_P$ and ${\mathrm{\Omega }}_P$ are finite. Both conditions also imply that is a well quasi-order, but the converse is not true. In the rest of this paper, unless specified, we will talk about valid $\omega$-ipomsets, and will omit the word “valid”.

Let $P$ and $Q$ be two (valid) $\omega$-ipomsets. We define the subsumption $P⊑Q$ as in the finite case by preserving also the -maximal elements ${\mathrm{\Omega }}_P$. Again, isomorphisms of $\omega$-ipomsets are invertible subsumptions (whose inverse is again a subsumption). The first result of this paper is the unicity of these isomorphisms. The proof is similar to the finite case, using pomset filtration (see [18, Lem. 34]):

Note that the proposition does not hold for general (non-valid) $\omega$-ipomsets: for example, all shifts by $n\in \mathbb{Z}$ are non-trivial automorphisms of $\mathbb{Z}$. As in the finite case, we may now switch freely between $\omega$-ipomsets and their isomorphism classes. The set of $\omega$-ipomsets is denoted ${\mathrm{𝗂𝖯𝗈𝗆𝗌}}^{\omega }$, and we use the notation ${\mathrm{𝗂𝖯𝗈𝗆𝗌}}^{\mathrm{\infty }}≔\mathrm{𝗂𝖯𝗈𝗆𝗌}\cup {\mathrm{𝗂𝖯𝗈𝗆𝗌}}^{\omega }$.

We extend here the operations $\ast$ (gluing) and $\parallel$ (parallel composition) to $\omega$-ipomsets.

For $(P,Q)\in ({\mathrm{𝗂𝖯𝗈𝗆𝗌}}^{\mathrm{\infty }}\times {\mathrm{𝗂𝖯𝗈𝗆𝗌}}^{\mathrm{\infty }})\setminus (\mathrm{𝗂𝖯𝗈𝗆𝗌}\times \mathrm{𝗂𝖯𝗈𝗆𝗌})$, the parallel composition $P\parallel Q$ (or $\left[\begin{array}{c}P\\ Q\end{array}\right]$) is the $\omega$-ipomset where $\bigsqcup$ is the disjoint union and $x⇢y$ iff $(x,y)\in P\times Q$ or $x{⇢}_{P}y$ or $x{⇢}_{Q}y$.

The gluing composition $P\ast Q$ (or $PQ$ ) of $(P,Q)\in \mathrm{𝗂𝖯𝗈𝗆𝗌}\times {\mathrm{𝗂𝖯𝗈𝗆𝗌}}^{\omega }$ is defined if there exists a unique¹¹1Isomorphisms of conclists is a special case of ipomset isomorphisms. Unicity is ensured by event order. isomorphism $f:T_P\to S_Q$, by ²²2($P\bigsqcup Q){}_{x\sim f(x)}$ is the quotient of the disjoint union under the unique isomorphism $f:T_P\to S_Q$., where:

• $\mathrm{■}$

  iff , , or $x\in P\setminus T_P$ and $y\in Q\setminus S_Q$;

• $\mathrm{■}$

  $⇢$ is the transitive closure of ${⇢}_P\cup {⇢}_Q$ on ${(P\bigsqcup Q)}_{/x\sim f(x)}$.

Informally, the sources of $Q$ are attached to the targets of $P$.

Note that both $\ast$ and $\parallel$ are associative and non-commutative. The non-commutativity of $\parallel$ is due to event order. The latter is crucial for isomorphism unicity and to define gluing composition. Still, even if $\left[\begin{array}{c}a\\ b\end{array}\right]\ne \left[\begin{array}{c}b\\ a\end{array}\right]$, both express that $a$ and $b$ are running concurrently. Alur et al in [1] introduced a similar “ordered parallel composition” for application purposes.

We also introduce an infinite gluing of an $\omega$-sequence of ipomsets. Let ${(P_i)}_{i\in \mathbb{N}}\in {\mathrm{𝗂𝖯𝗈𝗆𝗌}}^{\mathbb{N}}$ such that for all $i$, $T_{P_i}\cong S_{P_{i\text{+}1}}$. We define $P=P_0\ast P_1\ast \mathrm{\cdots }$ by , where

• $\mathrm{■}$

  $P={({\bigcup }_{i\in \mathbb{N}}(P_i,i))}_{/x\sim f(x)}$ where $f:{\bigcup }_{i\in \mathbb{N}}(T_i,i)\to {\bigcup }_{i\in \mathbb{N}}(S_i,i)$ such that $f(x,i)=(f_i(x),$ $i+1)$ with $f_i$ the unique isomorphism between $T_{P_i}$ and $S_{P_{i\text{+}1}}$;

• $\mathrm{■}$

  $S_P=S_{P_0}\times \{0\}$;

• $\mathrm{■}$

  if ($i=j$ and ) or ($i\text{+}1⩽j$, $x\in P_i\setminus T_{P_i}$ and $y\in P_{i\text{+}1}\setminus S_{P_{i\text{+}1}}$);

• $\mathrm{■}$

  ${⇢}_P$ is the transitive closure of ${\bigcup }_{i\in \mathbb{N}}{⇢}_{P_i}$;

• $\mathrm{■}$

  ${\lambda }_P(x,i)={\lambda }_{P_i}(x)$ for $i\in \mathbb{N}$ and $x\in P_i$.

Note in particular that when $P_i\in \mathrm{𝖨𝖽}$ we have $P_0\ast \mathrm{\cdots }\ast P_{i-1}\ast P_i\ast P_{i+1}\ast \mathrm{\cdots }=P_0\ast \mathrm{\cdots }\ast P_{i-1}\ast P_{i+1}\ast \mathrm{\cdots }$. We let denote by $P^{\omega }$ the $\omega$-ipomset defined by the infinite gluing of the constant sequence equal to $P$ with $S_P\cong T_P$.

Intuitively, $P$ is infinite since it is obtained by composing infinitely many non-identities, finite past is a consequence of the infinite gluing definition, and finiteness of antichains is due to width-boundedness of the operands. Note that this is not an equivalence condition. The infinite gluing may define a valid $\omega$-ipomset even if $\mathrm{𝗐𝖽}(P_i)$ are not bounded (see Fig. 3). Finding an equivalence condition on $(P_i)$ is hard, because it has to consider event order. For example, Fig. 6 exhibits two infinite products behaving differently with only a change of event order.

We will here only deal with interval $\omega$-ipomsets. An $\omega$-ipomset is interval (denoted $\omega$-iipomset) if for all $w,x,y,z\in P$, if and , then or . The set of all interval $\omega$-ipomsets is denoted ${\mathrm{𝗂𝗂𝖯𝗈𝗆𝗌}}^{\omega }$ (and we use the notation ${\mathrm{𝗂𝗂𝖯𝗈𝗆𝗌}}^{\mathrm{\infty }}≔\mathrm{𝗂𝗂𝖯𝗈𝗆𝗌}\cup {\mathrm{𝗂𝗂𝖯𝗈𝗆𝗌}}^{\omega }$).

There are multiple equivalent ways to define interval ipomsets [18, Lem. 39], and the same goes for $\omega$-ipomsets.

We say that $P\in {\mathrm{𝗂𝖯𝗈𝗆𝗌}}^{\omega }$ admits an interval representation if there are two functions $b,e:P\to \mathbb{N}\cup \{+\mathrm{\infty }\}$ such that for all $x,y\in P$, $b(x)⩽e(x)$ and .

As for finite pomsets and with similar arguments, the following holds:

Establishing the equivalence between the first two items is a routine. The third item is less intuitive, but it implies the second one by showing that the set of maximal antichains equipped with $\ll$ is isomorphic to . From that, to an event $a\in P$ we can associate the interval going from the index of the first appearance of $a$ in the antichains to the index of the last appearance.

A starter $U$ is a discrete ipomset (i.e.  is empty) with $T_U=U$ (hence written ${}_S{U}_U$), and a terminator $U$ is a discrete ipomset with $S_U=U$ (written ${}_U{U}_T$). We denote by $\mathrm{\Xi }$ the set of starters and terminators. Note that $\mathrm{𝖨𝖽}\subseteq \mathrm{\Xi }$. We say that $U\in \mathrm{\Xi }$ is proper if $U\in \mathrm{\Xi }\setminus \mathrm{𝖨𝖽}$. A starter ${}_{U-A}{U}_U$ will be written ${}_A{}^{}\uparrow U$ (meaning it contains the events in $U$ and start the events in $A\subseteq U$), and a terminator ${}_U{U}_{U-A}$ will be written $U{\downarrow }_A$. We call a step decomposition of $P\in {\mathrm{𝗂𝖯𝗈𝗆𝗌}}^{\omega }$ a sequence of starters and terminators ${(U_i)}_{i\in \mathbb{N}}$ such that $P=U_0\ast U_1\ast \mathrm{\cdots }$, and a decomposition is said to be sparse if proper starters and terminators are alternating. As for finite iipomsets [22], we can prove uniqueness of sparse decompositions of $\omega$-iipomsets:

Defining such a decomposition gives us a characterization of $\omega$-iipomsets in terms of their prefixes. We say that $A\in \mathrm{𝗂𝖯𝗈𝗆𝗌}$ is a (finite) prefix of $P\in {\mathrm{𝗂𝖯𝗈𝗆𝗌}}^{\mathrm{\infty }}$ if there is $Q\in {\mathrm{𝗂𝖯𝗈𝗆𝗌}}^{\mathrm{\infty }}$ such that $P=AQ$, and then write $A\prec P$. We call $\mathrm{𝖯𝗋𝖾𝖿}(P)$ the set of all prefixes of $P$.

The following lemma is trivial in classical $\omega$-word theory, but here relies crucially on the fact that we deal with valid $\omega$-ipomsets.

A precubical set is a structure $(X,\mathrm{𝖾𝗏},\mathrm{\Delta })$ with:

• $\mathrm{■}$

  a set of cells $X$;

• $\mathrm{■}$

  a function $\mathrm{𝖾𝗏}:X\to \mathrm{\square }$ which assigns to a cell its list of active events (for $U\in \mathrm{\square }$ we write $X[U]=\{q\in X|\mathrm{𝖾𝗏}(x)=U\}$);

• $\mathrm{■}$

  face maps $\mathrm{\Delta }=\{{\delta }_{A,U}^0,{\delta }_{A,U}^1|U\in \mathrm{\square },A\subseteq U\}$ such that ${\delta }_{A,U}^0,{\delta }_{A,U}^1:X[U]\to X[U-A]$;

• $\mathrm{■}$

  for $A,B\subseteq U\text{ s.t. }A\cap B=\mathrm{\varnothing }$ and $\mu ,\nu \in \{0,1\}$, we have the following precubical identities: ${\delta }_{A,U-B}^{\mu }\circ {\delta }_{B,U}^{\nu }={\delta }_{B,U-A}^{\nu }\circ {\delta }_{A,U}^{\mu }$.

We usually refer to a precubical set by its set of cells $X$, and for face maps we often omit the second subscript $U$. The dimension of a cell $q\in X$ is the size $|\mathrm{𝖾𝗏}(q)|$. An upper face map ${\delta }_A^1$ terminates the events in $A$, whereas a lower face map ${\delta }_A^0$ “unstarts” these events, that is, it maps to a cell where the events of $A$ are not yet started.

A higher-dimensional automaton is a tuple $(X,{\perp }_X,{\top }_X)$ where $X$ is a finite precubical set, and ${\perp }_X,{\top }_X\subseteq X$ are the sets of starting and accepting cells. We may omit the subscripts _X if the context is clear, and refer to an HDA only by its precubical set.

A track $\alpha$ in $X$ is a sequence $(q_0,{\phi }_1,q_1,\mathrm{\dots },{\phi }_n,q_n)$ where $q_i\in X$ are cells and ${\phi }_i$ denote face map types. That is, for all $i⩽n$, $(q_i,{\phi }_i,q_{i\text{+}1})$ is:

• $\mathrm{■}$

  either an upstep: $({\delta }_A^0(q_{i\text{+}1}),{\nearrow }^A,q_{i\text{+}1})$ with $A\subseteq \mathrm{𝖾𝗏}(q_{i\text{+}1})$,

• $\mathrm{■}$

  or a downstep: $(q_i,{\searrow }_B,{\delta }_B^1(q_i))$ with $B\subseteq \mathrm{𝖾𝗏}(q_i)$.

The source of $\alpha$ is $\mathrm{𝗌𝗋𝖼}(\alpha )=q_0$ and its target is $\mathrm{𝗍𝗀𝗍}(\alpha )=q_n$. A track is accepting if $\mathrm{𝗌𝗋𝖼}(\alpha )\in {\perp }_X$ and $\mathrm{𝗍𝗀𝗍}(\alpha )\in {\top }_X$. Note that tracks are concatenations (denoted using $\ast$) of upsteps and downsteps. The language of an HDA is defined in terms of the event ipomsets of its accepting tracks. Formally, the event ipomset of a track $\alpha$ (written $\mathrm{𝖾𝗏}(\alpha )$) is defined by:

• $\mathrm{■}$

  $\mathrm{𝖾𝗏}((q))={\mathrm{𝗂𝖽}}_{\mathrm{𝖾𝗏}(q)}$ (with $q\in X$ and $(q)$ a single-cell track)

• $\mathrm{■}$

  $\mathrm{𝖾𝗏}((q,{\nearrow }^A,p))={}_A{}^{}\uparrow \mathrm{𝖾𝗏}(p)$ (the starter which starts events $A$)

• $\mathrm{■}$

  $\mathrm{𝖾𝗏}((q,{\searrow }_B,p))=\mathrm{𝖾𝗏}(q){\downarrow }_B$ (the terminator which terminates events $B$)

• $\mathrm{■}$

  $\mathrm{𝖾𝗏}({\alpha }_1\ast \mathrm{\cdots }\ast {\alpha }_n)=\mathrm{𝖾𝗏}({\alpha }_1)\ast \mathrm{\cdots }\ast \mathrm{𝖾𝗏}({\alpha }_n)$

We say that two tracks $\alpha$ and $\beta$ are equivalent, denoted $\alpha \simeq \beta$, with $\simeq$ the relation generated by the three cases $(x{\nearrow }^{A}y{\nearrow }^{B}z)\simeq (x{\nearrow }^{A\cup B}z)$, $(x{\searrow }_{A}y{\searrow }_{B}z)\simeq (x{\searrow }_{A\cup B}z)$, and $\gamma \alpha \delta \simeq \gamma \beta \delta$ whenever $\alpha \simeq \beta$. Basically, two tracks are equivalent if their “contractions” into sparse tracks (i.e. alternating upsteps and downsteps) and event ipomsets are equal.

The language of an HDA $X$ is $L(X)=\{\mathrm{𝖾𝗏}(\alpha )|\mathrm{𝗌𝗋𝖼}(\alpha )\in {\perp }_X\text{ and }\mathrm{𝗍𝗀𝗍}(\alpha )\in {\top }_X\}$. The following result about languages of HDAs is a fundamental property:

For $L\subseteq \mathrm{𝗂𝖯𝗈𝗆𝗌}$, we write $L\mathrm{\downarrow }=\{P\in \mathrm{𝗂𝗂𝖯𝗈𝗆𝗌}|\exists Q\in L,P⊑Q\}$ for the subsumption closure of $L$. For example, the language of Ex. 14 is $L(X)=\{b\bullet ,\bullet b\bullet ,\left[\begin{array}{c}a\\ b\bullet \end{array}\right],\left[\begin{array}{c}a\\ \bullet b\bullet \end{array}\right],\left[\begin{array}{c}a\\ b\end{array}\right],\left[\begin{array}{c}a\\ \bullet b\end{array}\right]\}\mathrm{\downarrow }$. Let us extend the notation to $R\subseteq 2^{\mathrm{𝗂𝖯𝗈𝗆𝗌}}$ with $R\mathrm{\downarrow }=\{L\mathrm{\downarrow }|L\in R\}$.

Previous work [19] defines down-closed rational operations $\cup$, ${\ast }_{\mathrm{\downarrow }}$, ${\parallel }_{\mathrm{\downarrow }}$ and (Kleene plus) ${}^{{+}_{\mathrm{\downarrow }}}$ for languages of finite iipomsets, as follows:

• $\mathrm{■}$

  $L{\ast }_{\mathrm{\downarrow }}M=\{P\ast Q\mid P\in L,Q\in M,T_P=S_Q\}\mathrm{\downarrow }$,

• $\mathrm{■}$

  ${L\parallel }_{\mathrm{\downarrow }}M=\{P\Vert Q\mid P\in L,Q\in M\}\mathrm{\downarrow }$,

• $\mathrm{■}$

  $L^{{+}_{\mathrm{\downarrow }}}={\bigcup }_{n\ge 1}{L}^n$, with $L^1=L$ and $L^{n+1}=L{\ast }_{\mathrm{\downarrow }}{L}^n$.

The class $D\text{-}ℛat$ of down-closed rational languages is then defined to be the smallest class that contains $\mathrm{\varnothing }$, $\{{\mathrm{𝗂𝖽}}_{\mathrm{\varnothing }}\}$, $\{a\}$, $\{\bullet a\}$,$\{a\bullet \}$, $\{\bullet a\bullet \}$ (for $a\in \mathrm{\Sigma }$), and is closed under the operations above. Note that the explicit downclosure $\mathrm{\downarrow }$ of the operations above ensures that the built languages contain only interval ipomsets.³³3For $L=\{ac\}$ and $M=\{\bullet bd\bullet \}$, $(ac\parallel \bullet bd\bullet )\notin L{\parallel }_{\mathrm{\downarrow }}M$ but, for example, the ipomsets of Fig 2 are in ${L\parallel }_{\mathrm{\downarrow }}M$. We will below introduce rational operations which do not apply down-closure; to distinguish them from the ones above we have added a subscript ${}_{\mathrm{\downarrow }}$.

An $\omega$-HDA is an HDA whose tracks are infinite. Formally, an $\omega$-track is an infinite sequence $\alpha =(q_0,{\phi }_1,q_1,\mathrm{\dots })$ where $q_i\in X$ and each $(q_i,{\phi }_i,q_{i\text{+}1})$ is an upstep or a downstep. The event ipomset of an $\omega$-track is defined similarly using the infinite gluing. From this we may directly introduce the classical acceptance conditions of $\omega$-automata theory:

Let $\mathrm{𝖨𝗇𝖿}(\alpha )=\{q\in X\mid |\{i|q_i=q\}|=+\mathrm{\infty }\}$ be the set of cells seen infinitely often by $\alpha$. A Büchi $\omega$-HDA is an HDA $(X,{\perp }_X,{\top }_X)$ where ${\perp }_X,{\top }_X\subseteq X$ are the sets of starting and accepting cells, and where an $\omega$-track $\alpha$ is accepting if $\mathrm{𝗌𝗋𝖼}(\alpha )\in {\perp }_X$ and $\mathrm{𝖨𝗇𝖿}(\alpha )\cap {\top }_X\ne \mathrm{\varnothing }$. Similarly, a Muller $\omega$-HDA is an HDA $(X,{\perp }_X,F_X)$ where ${\perp }_X\subseteq X$ is the set of starting cells and $F_X\subseteq 2^X$ is the set of accepting sets of cells, and where an $\omega$-track $\alpha$ is accepting if $\mathrm{𝗌𝗋𝖼}(\alpha )\in {\perp }_X$ and $\mathrm{𝖨𝗇𝖿}(\alpha )\in F_X$.

The language of a Büchi $\omega$-HDA $X$ is $L(X)=\{\mathrm{𝖾𝗏}(\alpha )|\mathrm{𝗌𝗋𝖼}(\alpha )\in {\perp }_X\text{ and }\mathrm{𝖨𝗇𝖿}(\alpha )\cap {\top }_X\ne \mathrm{\varnothing }\}$ and we call Büchi $\omega$-regular such a language. Similarly, for a Muller $\omega$-HDA $Y$ we have $L(Y)=\{\mathrm{𝖾𝗏}(\alpha )|\mathrm{𝗌𝗋𝖼}(\alpha )\in {\perp }_Y\text{ and }\mathrm{𝖨𝗇𝖿}(\alpha )\in F_Y\}$ and we call Muller $\omega$-regular such a language. As in classical $\omega$-theory, a Büchi $\omega$-HDA $X_B$ can be seen as a Muller $\omega$-HDA $X_M$, where the acceptance condition is modified to $F_{X_M}=\{A\subseteq X|A\cap {\top }_X\ne \mathrm{\varnothing }\}$. Hence Büchi $\omega$-regular languages are Muller $\omega$-regular. However, unlike HDAs over finite ipomsets we have:

An ST-automaton is a plain ($\omega$-)automaton over $\mathrm{\Xi }$, with an additional labeling of states, that can produce ($\omega$-)iipomsets if the letters are glued. It especially can mimic the behavior of an ($\omega$-)HDA with a canonical translation. We use here the most recent definition of these objects, introduced in [4], which subsumes other variants that have been used in [19, 7, 2, 3, 8, 17, 16].

We let $\overline{\mathrm{\Xi }}=(\overline{\mathrm{\Xi }},\cdot ,\epsilon )$ denote the free monoid on $\overline{\mathrm{\Xi }}=\mathrm{\Xi }$ seen as an alphabet, using concatenation instead of gluing and $\epsilon$ for the empty word (which is different from the letter ${\mathrm{𝗂𝖽}}_{\mathrm{\varnothing }}\in \overline{\mathrm{\Xi }}$).

An ST-automaton $A$ is a finite labeled automaton $(Q,E,I,F,\lambda )$ over the (infinite) alphabet $\overline{\mathrm{\Xi }}$, where $Q$ is the set of states, $E\subseteq Q\times (\overline{\mathrm{\Xi }}\setminus \mathrm{𝖨𝖽})\times Q$ is the set of transitions, $I\subseteq Q$ are the initial states, $F$ is an acceptance condition and $\lambda :Q\to \mathrm{\square }$ is a labeling of states that is coherent with $E$, meaning that for all $(p{,}_S{U}_T,q)\in E,\lambda (p)=S$ and $\lambda (q)=T$.

A path $\pi =(q_0,e_0,q_1,e_1,\mathrm{\dots },e_{n-1},q_n)$ in an ST-automaton $A$ is an alternation of states and transitions such that $e_i=(q_i,P_i,q_{i+1})\in E$. Its label is $l(\pi )={\mathrm{𝗂𝖽}}_{\lambda (q_0)}\cdot P_0\cdot {\mathrm{𝗂𝖽}}_{\lambda (q_1)}\cdot$ $\mathrm{\dots }\cdot P_{n-1}\cdot {\mathrm{𝗂𝖽}}_{\lambda (q_n)}$ seen as a word. We say that $\pi$ is accepting if $q_0\in I$ and $q_n\in F$. The language of an ST-automaton $A$, denoted $L(A)$, is the set of labels of its accepting paths. The same can be done for $\omega$-paths, which are accepted according to a Büchi or Muller condition.

In the following, we build an ST-automaton $ST(X)$ from an ($\omega$-)HDA $X$, following [4]. The intuition is that each cell (of any dimension) becomes a state, and for each upstep $(p={\delta }_A^0(q),{\nearrow }^A,q)$ resp. downstep $(p,{\searrow }_B,{\delta }_B^1(p)=q)$ in $X$, a transition is introduced from the state corresponding to $p$ to the one corresponding to $q$, labeled with ${}_A{}^{}\uparrow \mathrm{𝖾𝗏}(q)$ resp. $\mathrm{𝖾𝗏}(p){\downarrow }_B$), to mimic the behavior of the HDA. More formally, for an HDA $(X,{\perp }_X,F_X)$, we associate the ST-automaton $ST(X)=(Q,E,I,F,\lambda )$ with:

• $\mathrm{■}$

  $Q=X$, $I={\perp }_X$, $F=F_X$, $\lambda =\mathrm{𝖾𝗏}$,

• $\mathrm{■}$

  $E=\{({\delta }_A^0(q),{}_A{}^{}\uparrow \mathrm{𝖾𝗏}(q),q)|A\subseteq \mathrm{𝖾𝗏}(q)\}\cup \{(q,\mathrm{𝖾𝗏}(q){\downarrow }_A,{\delta }_A^1(q))|A\subseteq \mathrm{𝖾𝗏}(q)\}$.

By construction, there is a one-to-one correspondence between tracks in $X$ and paths in $ST(X)$: with a track $\alpha =(q_0,{\phi }_0,q_1,\mathrm{\dots })$ of $X$ we associate the path $ST(\alpha )=(q_0,e_0,q_1,\mathrm{\dots })$ of $ST(X)$ such that

• $\mathrm{■}$

  $(q_i,{\phi }_i,q_{i\text{+}1})=({\delta }_{A_i}^0(q_{i\text{+}1}),{\nearrow }^{A_i},q_{i\text{+}1})\Rightarrow A_i\subseteq \mathrm{𝖾𝗏}(q_{i\text{+}1})$, $e_i=(q_i,{}_{A_i}{}^{}\uparrow \mathrm{𝖾𝗏}(q_{i\text{+}1}),q_{i\text{+}1})\in E$

• $\mathrm{■}$

  $(q_i,{\phi }_i,q_{i\text{+}1})=(q_i,{\searrow }_{A_i},{\delta }_{A_i}^1(q_i))\Rightarrow A_i\subseteq \mathrm{𝖾𝗏}(q_i)$, $e_i=(q_i,\mathrm{𝖾𝗏}(q_i){\downarrow }_{A_i},q_{i\text{+}1})\in E$

This proves the following lemma:

Since the labeling $\lambda$ is coherent with $E$, a word produced by an ST-automaton $A$ is coherent in the sense that if $P_1\cdot P_2\cdot \mathrm{\dots }$ is the label of a path in $A$, then $T_{P_i}\cong S_{P_{i\text{+}1}}$ for all $i⩾0$ (and thus it can be seen as the gluing of starters and terminators). To be more precise, the set of coherent finite words over $\overline{\mathrm{\Xi }}$ is denoted ${\mathrm{𝖢𝗈𝗁}}^{+}(\overline{\mathrm{\Xi }})=\{U_1\cdot \mathrm{\dots }\cdot U_n|U_i\in \overline{\mathrm{\Xi }},T_{U_i}\cong S_{U_{i\text{+}1}}\}$.

For $\omega$-words we denote by ${\mathrm{𝖢𝗈𝗁}}^{\omega }(\overline{\mathrm{\Xi }})$ the set of coherent infinite words over $\overline{\mathrm{\Xi }}$, defined by

and as usual we write ${\mathrm{𝖢𝗈𝗁}}^{\mathrm{\infty }}(\overline{\mathrm{\Xi }})={\mathrm{𝖢𝗈𝗁}}^{+}(\overline{\mathrm{\Xi }})\cup {\mathrm{𝖢𝗈𝗁}}^{\omega }(\overline{\mathrm{\Xi }})$.