The Finiteness Problem for Automaton Semigroups of Extended Bounded Activity

Abstract

We extend the notion of activity for automaton semigroups and monoids introduced by Bartholdi, Godin, Klimann and Picantin to a more general setting. Their activity notion was already a generalization of Sidki’s activity hierarchy for automaton groups. Using the concept of expandability introduced earlier by the current authors, we show that the language of $\omega$-words with infinite orbits is effectively a deterministic Büchi language for our extended activity. This generalizes a similar previous result on automaton groups by Bondarenko and the third author. By a result of Francoeur and the current authors, the description via a Büchi automaton immediately yields that the finiteness problem for complete automaton semigroups and monoids of bounded activity is decidable. In fact, we obtain a stronger result where we may consider sub-orbits under the action of a regular, suffix-closed language over the generators. This, in particular, also yields that it is decidable whether a finitely generated subsemigroup (or -monoid) of a bounded complete automaton semigroup is finite.

Keywords: automaton semigroup; automaton monoid; bounded automaton; finiteness problem; orbit.
Mathematics Subject Classification 2010: 68Q70, 20M35, 20E08

1 Introduction

The class of automaton groups is a rich source for groups with exotic properties. Probably the most famous one of these groups is Grigorchuk’s group (and we refer the reader e. g. to [3, 24] for many more examples). Grigorchuk’s group was the first example of a group with intermediate growth (see e. g. [17] for more information) and is also a Burnside group (in the sense that it is infinite while very element has finite order) as well as amenable but not elementary amenable (see e. g. [20]). Interestingly, it is not finitely presented [15] but, as an automaton group, it has a finite description using an automaton. This demonstrates that using automata to generate groups (and also semigroups) is algorithmically interesting as we may give the generating automaton as a finite input to an algorithm, which allows us to consider algorithms for groups that do not have finite presentations (in the sense of a pair of finitely many generators and finitely many relations over them).

An automaton in this context is a deterministic and complete finite-state, letter-to-letter transducer (where we do not need any initial or final states), i. e. a finite graph whose edges are labeled by pairs $(a,b)$ of an input letter $a$ and an output letter $b$. The idea is that (since the automaton is deterministic and complete) we may start reading an input word $u$ in some state $p$ (which is the term used to denote the nodes of such a graph in this setting) and obtain a corresponding output word $v$. This way, we may associate to $p$ a function that maps $u$ to $v$ and we may consider the closure under composition of these functions for all states, which is one way to define the semigroup generated by the automaton. If the automaton is additionally invertible, we have that all the induced functions are bijections and we may also include their inverses in the closure under composition, which yields the group generated by the automaton. Groups and semigroups arising in this way are called automaton groups and automaton semigroups.

More structure was brought into the class of automaton groups by Sidki who introduced the activity of an invertible automaton [27]. His idea was to look at the structure of the cycles in the automaton (see [27] or e. g. [30] for more details on the connection to the geometric structure of the automaton). A word $u$ here is said to be active for a state $p$ if, after reading $u$ starting in $p$, we do not end in a/the state acting as the identity on all words. If the number of active words of any length is bounded uniformly by a constant, we say that $p$ has bounded activity. If the number of words grows linearly with their length, we speak of linear activity. If it grows quadratically (cubically, etc.), also the activity is quadratic (cubic, etc.). It turns out, that the activity is either polynomial (with a natural number as the degree) or it is exponential.

The activity of a single state naturally generalizes to the activity of a group element (which is typically given as a word over the states as generators). If two group elements have, say, bounded activity, also their product has, which allows us to speak, for example, of bounded automaton groups (in which all elements have bounded activity). This yields an infinite hierarchy within the class of automaton groups, which consists of a polynomial and an exponential part. Interestingly, many famous and interesting example of automaton groups are already contained in the second-lowest level of bounded activity (the lowest level consists of all finite groups). This applies, in particular, to Grigorchuk’s group (and the reader may find further examples e. g. in [30]).

Maybe surprisingly, bounded automaton groups (despite their already quite complicated nature) seem to be “finite enough” such that many of their decision problems remain decidable (or have lower complexity compared to general automaton groups). For example, the order problem is decidable in such groups [5] while it is undecidable for general automaton groups [14, 2]. Their finiteness problem is also decidable [4] while the problem is widely suspected to be undecidable in the general case but sill open [16, 7.2.(b)] (it is known to be undecidable for automaton semigroups [13]). Furthermore, bounded automaton groups are contracting [6] (see also e. g. [24, 30]) and their word problem is therefore solvable in logarithmic space (by a deterministic Turing machine) while, for general automaton groups, there is one with PSpace-complete word problem [29] (see [30] for more background information; see also [22] for the word problem on the lowest level of the hierarchy).

Likely driven by such algorithmic results (as they show that the order/torsion problem remains decidable), Bartholdi, Godin, Klimann and Picantin [1] generalized the notion of activity to automaton monoids. In order to keep certain desirable properties of the activity notion in the group case, their generalization rather uses the output instead of the input in order to define active words, which makes the geometric characterization based on the cyclic structure of the generating automaton less transparent. However, they still count those words that do not end in the/an identity state, which obviously is only a useful concept if such an identity state exists; in this case, however, the generated semigroup is necessarily a monoid. As a potential extension (that is also interesting for semigroups), they propose to replace the identity state by what is called the maximal NoCyWEx subautomaton (which necessarily generates a finite subsemigroup).

However, there does not seem to be any reason to only consider this particular subautomaton. Instead, we introduce a different notion of extended activity where we may consider any subset $S$ of states (which is not a restriction as any finite set of semigroup elements may always be considered to appear as single states) that is closed in the sense that we may not leave $S$ by reading any word in the generators. A(n output) word is then $S$-active if we do not end in a state in $S$ after reading it. This strictly generalizes all previous activity notions: if we let $S$ contain only the identity state, we obtain the activity notion for groups and monoids and, if we take $S$ as the NoCyWEx part of the automaton, we obtain the above extended activity.

We then consider automata which have bounded $S$-activity. We show that, if we are given the promise that $S$ generates a finite subsemigroup (as the finiteness problem for automaton semigroups is undecidable [13]), then the finiteness problem for automaton semigroups of bounded $S$-activity is decidable. This works, in particular, for all the other activity notions and generalizes the corresponding group result [4] to semigroups and monoids. In fact, we obtain this algorithmic result by showing that the language of $\omega$-words with an infinite orbits is recognized (by an effectively constructible) deterministic Büchi acceptor (which also is a generalization from the group case in [4]). The construction of this Büchi acceptor is based on the notion of expandability introduced by the authors in [9] and the final connection to the finiteness problem is due to the fact that an automaton semigroup is infinite if and only if it admits an (infinite) word with an infinite orbit. As an additional result of our characterization of words with infinite orbits as deterministic Büchi languages, we also obtain that an automaton semigroup of bounded $S$-activity is infinite if and only if it admits an ultimately periodic word with an infinite orbits.

In fact, we obtain these results not only for the full orbits but also for the case where we consider the sub-orbits given by a regular, suffix-closed language of the state set. This shows, in particular, that the finiteness problem for finitely generated subsemigroups of automaton semigroups with bounded $S$-activity is decidable (which the order problem is a special case of; compare to [1]).

2 Preliminaries

Sets, Semigroups, Words and (Regular) Languages.

We write $\mathcal{P}(A)$ for the power set of a set $A$ and $A\uplus B$ for the disjoint union of two sets $A$ and $B$. A set $S$ with an associative operation is a semigroup and, if $S$ additionally has a neutral element (i. e. an element $e\in S$ with $es=s=se$ for all $s\in S$), it is a monoid. The assume the reader to be familiar with the basics of semigroup theory but we will not need any advanced concepts.

An alphabet is a non-empty, finite set $\Sigma$. By $\Sigma^{*}$, we denote the set of finite words over $\Sigma$ including the empty word $\varepsilon$. If we want to exclude it, we write $\Sigma^{+}$. For the set of finite words of length exactly $n\geq 0$, we write $\Sigma^{n}$. By $\Sigma^{\omega}$, we denote the set of $\omega$-words (i. e. right infinite words) over $\Sigma$. We use the terms word for both, finite words and $\omega$-words and a language can either be a subset of $\Sigma^{*}$ or a subset of $\Sigma^{\omega}$.

Regular Languages.

For a language $L\subseteq\Sigma^{*}$ (of finite words), we define the (Myhill-Nerode) relation $u\mathrel{L}v\iff(\forall x\in\Sigma^{*}:ux\in L\iff vx\in L)$. The classes of this relation are called the (Myhill-Nerode) classes of $L$ and the class of $u\in\Sigma^{*}$ is denoted by $\mathscr{C}_{L}(u)$ or simply $\mathscr{C}(u)$ if the language is clear from the context. A language of finite words is regular if it has finitely many classes.

Büchi Acceptors and $\omega$-Regular Languages.

An (edge-accepting) Büchi acceptor (BA) is a tuple $\mathcal{B}=(Z,\Gamma,\tau,z_{0},\mathcal{F})$ where $Z$ is a finite set of states, $\Gamma$ is an alphabet, $\tau\subseteq Z\times\Gamma\times Z$ is a set of transitions, $z_{0}\in Z$ is the initial state and $\mathcal{F}\subseteq\tau$ is the set of accepting transitions. In the context of transitions, we also write for the element $(y,a,z)\in Z\times\Gamma\times Z$.

A Büchi acceptor $\mathcal{B}=(Z,\Gamma,\tau,z_{0},\mathcal{F})$ is deterministic if we have

$$d_{y,a}=\left|\{\leavevmode\hbox to17.02pt{\vbox to11.31pt{\pgfpicture\makeatletter\hbox{\hskip 2.6308pt\lower-3.12498pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.6308pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.29681pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$z$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{5.9638pt}{0.97221pt}\pgfsys@lineto{10.56375pt}{0.97221pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{1.36386pt}{0.97221pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.11375pt}{3.17221pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$a$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\in\tau\mid z\in Z\}\right|=1 y z a y z a$$

for all $y\in Z$ and $a\in\Gamma$.

A run of the Büchi acceptor $\mathcal{B}$ is an infinite sequence

where $\leavevmode\hbox to25.71pt{\vbox to12.6pt{\pgfpicture\makeatletter\hbox{\hskip 5.92876pt\lower-3.12498pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.92876pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y_{i-1}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{12.59477pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y_{i}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{9.26176pt}{0.97221pt}\pgfsys@lineto{13.86171pt}{0.97221pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.66182pt}{0.97221pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{6.73647pt}{4.46487pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$a_{i}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\in\tau$ for all $i\geq 1$. The input of this run is $a_{1}a_{2}\dots\in\Gamma^{\omega}$. Such a run is initial if $y_{0}=z_{0}$ and it is accepting if $\leavevmode\hbox to25.71pt{\vbox to12.6pt{\pgfpicture\makeatletter\hbox{\hskip 5.92876pt\lower-3.12498pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.92876pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y_{i-1}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{12.59477pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y_{i}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{9.26176pt}{0.97221pt}\pgfsys@lineto{13.86171pt}{0.97221pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.66182pt}{0.97221pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{6.73647pt}{4.46487pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$a_{i}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\in\mathcal{F}$ for infinitely many $i\geq 1$. The Büchi acceptor accepts an $\omega$-word $\alpha\in\Gamma^{\omega}$ if it admits an accepting initial run whose input is $\alpha$. The language (of $\omega$-words) of accepted words is the language recognized (or accepted) by the Büchi acceptor. A language is $\omega$-regular if it is accepted by some Büchi acceptor and, if the Büchi acceptor is deterministic, the language is deterministic $\omega$-regular.

Remark 2.1.

Instead of defining the acceptance using accepting transitions we could have used the more common acceptance criterion based on accepting states (where an $\omega$-word $\alpha$ is accepted if there is an initial run of the above form with input $\alpha$ such that infinitely many of the visited states $y_{i}$ are accepting). It is not difficult to see, though, that the two notions are equivalent: A state-accepting BA is tuned into an edge-accepting one by marking all transitions going into an accepting state as accepting. In the other direction, we duplicate every state and have an accepting and a non-accepting version. Now, we let accepting transitions end in the accepting one and non-accepting transitions end in the corresponding non-accepting state.

Remark 2.2.

It is well-known that the class of deterministic $\omega$-regular languages is a proper subclass of all $\omega$-regular languages. See, for example, [26] for more information on $\omega$-regular languages.

Semigroup Presentations and Free Products.

A semigroup presentation is a pair $\langle Q\mid\mathcal{R}\rangle_{\mathscr{S}}$ of a set of generators $Q$ and a (possibly infinite) set of relations $\mathcal{R}\subseteq Q^{+}\times Q^{+}$. Typically, we will only consider finitely generated semigroups (i. e. we assume $Q$ to be a finite set and, usually, also non-empty). If we denote by $\mathcal{C}$ the smallest congruence $\mathcal{C}\subseteq Q^{+}\times Q^{+}$ with $\mathcal{R}\subseteq\mathcal{C}$, the semigroup presented by such a presentation is $S=Q^{+}/\mathcal{C}$ formed by the congruence classes $[\cdot]_{\mathcal{C}}$ of $\mathcal{C}$ with the (well-defined!) operation $[u]_{\mathcal{C}}\cdot[v]_{\mathcal{C}}=[uv]_{\mathcal{C}}$. Every semigroup generated by a finite, non-empty set $Q$ is presented by some semigroup presentation of this form.

The free product of the semigroups $S=\langle Q\mid\mathcal{S}\rangle_{\mathscr{S}}$ and $T=\langle P\mid\mathcal{R}\rangle_{\mathscr{S}}$ is the semigroup $S\star T=\langle Q\uplus P\mid\mathcal{S}\cup\mathcal{R}\rangle_{\mathscr{S}}$. For example, we have $\{p,q\}^{+}=p^{+}\star q^{+}$. Any element of $S\star T$ can be written as a non-empty sequence of blocks $\bm{p}_{0}\bm{q}_{1}\bm{p}_{1}\ldots\bm{q}_{k}\bm{p}_{k}$ where $\bm{p}_{0},\bm{p}_{k}\in P^{*}$ may be empty but the other blocks $\bm{q}_{i}\in Q^{+}$ (for $1\leq i\leq k$) and $\bm{p}_{i}\in P^{+}$ (for $1\leq i<k$) may not.

Remark.

Of course, there is also the free product of monoids (and monoid presentations). However, in this paper, we only consider free products of semigroups (in particular, we have $\{p,q\}^{*}\not\simeq p^{*}\star q^{*}$).

$\mathscr{S}$-automata.

In the setting of the current paper, an automaton is a tuple $\mathcal{T}=(Q,\Sigma,\delta)$ where $Q$ is the finite, non-empty set of states, $\Sigma$ is an alphabet and $\delta\in Q\times\Sigma\times\Sigma\times Q$ is a set of transitions. In the context of transitions, we also use the graphical notations and for the tuple $(p,a,b,q)\in Q\times\Sigma\times\Sigma\times Q$. The intuitive idea is that, if this element is contained in $\delta$, we may read the input letter $a$ starting in $p$ and obtain the output letter $b$ and end in $q$.

A run in an automaton $\mathcal{T}=(Q,\Sigma,\delta)$ is a sequence

with $\leavevmode\hbox to25.25pt{\vbox to11.3pt{\pgfpicture\makeatletter\hbox{\hskip 5.81358pt\lower-3.12498pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.81358pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$p_{i-1}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{12.4796pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$p_{i}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{9.14659pt}{0.97221pt}\pgfsys@lineto{13.74654pt}{0.97221pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.54665pt}{0.97221pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{1.58287pt}{2.92221pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$a_{i}/b_{i}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\in\delta$ for all $0<i\leq\ell$ (where $\ell\geq 0$). It starts in $p_{0}$, ends in $p_{\ell}$, its input is $a_{1}\dots a_{\ell}$ and its output is $b_{1}\dots b_{\ell}$. We will abbreviate such a run also as .

An automaton $\mathcal{T}=(Q,\Sigma,\delta)$ is a complete $\mathscr{S}$-automaton if we have

$$d_{p,a}=\left|\{\leavevmode\hbox to16.52pt{\vbox to11.3pt{\pgfpicture\makeatletter\hbox{\hskip 2.51563pt\lower-3.12498pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.51563pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$p$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.18164pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$q$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{5.84863pt}{0.97221pt}\pgfsys@lineto{10.44858pt}{0.97221pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{1.24869pt}{0.97221pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.47568pt}{2.92221pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$a/b$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\in\delta\mid b\in\Sigma,q\in Q\}\right|=1 p q a/b p q a/b$$

for all $p\in Q$ and $a\in\Sigma$. It is easy to see that, in such an automaton, there is a unique run starting in $p$ with input $u$ for every $p\in Q$ and $u\in\Sigma^{*}$. This allows us to uniquely define $p\circ u$ as the output and $p\cdot u$ as the end of this run. This can naturally be extended into a left action of $Q^{*}$ on $\Sigma^{*}$ by letting $\varepsilon\circ u=u$ and, inductively, $\bm{q}p\circ u=\bm{q}\circ(p\circ u)$ for $p\in Q$ and $\bm{q}\in Q^{*}$. Clearly, we have $q_{\ell}\dots q_{1}\circ u=q_{\ell}\circ\dots\circ q_{1}\circ u$.

Similarly, we may also extend the notation $p\cdot u$ into a right action of $\Sigma^{*}$ on $Q^{*}$, which is called the dual action, by letting $\varepsilon\cdot u=\varepsilon$ and

$$\bm{q}p\cdot u=\left[\bm{q}\cdot(p\circ u)\right]\,(p\cdot u)\text{.}$$

For any complete $\mathscr{S}$-automaton $\mathcal{T}=(Q,\Sigma,\delta)$, we define the relation ${=_{\mathcal{T}}}\subseteq Q^{*}\times Q^{*}$ by

$$\bm{p}=_{\mathcal{T}}\bm{q}\iff\forall w\in\Sigma^{*}:\bm{p}\circ w=\bm{q}\circ w\textbf{.}$$

It is easy to see that ${=_{\mathcal{T}}}$ is a congruence. Thus, $Q^{+}/{{=_{\mathcal{T}}}}$ is a semigroup $\mathscr{S}(\mathcal{T})$ and we say that it is the semigroup generated by $\mathcal{T}$. Any semigroup arising in this way is called an automaton semigroup.

In addition to ${=_{\mathcal{T}}}$, we will use similar notation. In particular, we will write $\bm{q}\in_{\mathcal{T}}P$ for $\bm{q}\in Q^{*}$ and $P\subseteq Q^{*}$ if there is some $\bm{p}\in P$ with $\bm{q}=_{\mathcal{T}}\bm{p}$. For $P\subseteq Q^{+}$ and $\bm{q}\in Q^{+}$, writing $\bm{q}\in_{\mathcal{T}}P^{+}$ means that the image of $\bm{q}$ in the semigroup $\mathscr{S}(\mathcal{T})$ is contained in the subsemigroup generated by $P$.

Example 2.3.

The classical example of a complete $\mathscr{S}$-automaton is the adding machine:

Clearly, we have $e\circ u=u$ for all $u\in\{0,1\}^{*}$. In order to understand the action of $q$, it is best to look at an example. We have:

$$q\circ 000 =100 q^{3}\circ 000 =q\circ 010=110$$

$$q^{2}\circ 000 =q\circ 100=010 q^{4}\circ 000 =q\circ 110=001$$

More generally, if we denote the binary representation of $n\in\mathbb{N}$ of length $\ell$ in reverse/with the least significant bit on the left as $\operatorname{bin}n$, we have $q\circ\operatorname{bin}_{\ell}n=\operatorname{bin}_{\ell}(n+1)$ for all $n\in\mathbb{N}$ (with sufficiently large $\ell$). This shows ${q}^{i}\neq_{\mathcal{T}}q^{j}$ for all $i\neq j$ (with $i,j>0$). By identifying $q^{0}$ with $e$, we obtain that the semigroup generated by the adding machine is (isomorphic to) the free monogenic monoid $q^{*}$.

Union and Power Automata.

The union of two automata $\mathcal{T}_{1}=(Q_{1},\Sigma_{1},\delta_{1})$ and $\mathcal{T}_{2}=(Q_{2},\Sigma_{2},\delta_{2})$ is the automaton $\mathcal{T}_{1}\cup\mathcal{T}_{2}=(Q_{1}\cup Q_{2},\Sigma_{1}\cup\Sigma_{2},\delta_{1}\cup\delta_{2})$. The most common case of a union automaton is when the automata use the same alphabet but their state sets are disjoint. In this case, the union of two complete $\mathscr{S}$-automata is a complete $\mathscr{S}$-automaton.

The composition of two automata $\mathcal{T}_{2}=(Q_{2},\Sigma,\delta_{2})$ and $\mathcal{T}_{1}=(Q_{1},\Sigma,\delta_{1})$ over the same alphabet is $\mathcal{T}_{2}\circ\mathcal{T}_{1}=(Q_{2}Q_{1},\Sigma,\delta_{2}\circ\delta_{1})$ where $Q_{2}Q_{1}=\{q_{2}q_{1}\mid q_{1}\in Q_{1},q_{2}\in Q_{2}\}$ is the Cartesean product and

$$\delta_{2}\circ\delta_{1}=\{\leavevmode\hbox to37.57pt{\vbox to11.3pt{\pgfpicture\makeatletter\hbox{\hskip 7.83125pt\lower-3.12498pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-7.83125pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$p_{2}p_{1}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{14.49727pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$q_{2}q_{1}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{11.16426pt}{0.97221pt}\pgfsys@lineto{15.7642pt}{0.97221pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{6.56432pt}{0.97221pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.8274pt}{2.92221pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$a/c$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mid\exists b\in\Sigma:\leavevmode\hbox to22.12pt{\vbox to11.3pt{\pgfpicture\makeatletter\hbox{\hskip 3.91562pt\lower-3.12498pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.91562pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$p_{1}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{10.58163pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$q_{1}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{7.24863pt}{0.97221pt}\pgfsys@lineto{11.84857pt}{0.97221pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{2.64868pt}{0.97221pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-0.07568pt}{2.92221pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$a/b$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\in\delta_{1},\leavevmode\hbox to22.12pt{\vbox to11.3pt{\pgfpicture\makeatletter\hbox{\hskip 3.91562pt\lower-3.12498pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.91562pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$p_{2}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{10.58163pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$q_{2}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{7.24863pt}{0.97221pt}\pgfsys@lineto{11.84857pt}{0.97221pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{2.64868pt}{0.97221pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.25974pt}{2.92221pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$b/c$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\in\delta_{2}\}\text{.} p_{2}p_{1} q_{2}q_{1} a/c p_{1} q_{1} a/b p_{2} q_{2} b/c p_{2}p_{1} q_{2}q_{1} a/c p_{1} q_{1} a/b p_{2} q_{2} b/c$$

The composition of two complete $\mathscr{S}$-automata over the same alphabet is a complete $\mathscr{S}$-automaton.

The $k$-th power of an automaton $\mathcal{T}=(Q,\Sigma,\delta)$ (with $k\geq 1$) is the $k$-fold composition of $\mathcal{T}$ with itself. Any power of a complete $\mathscr{S}$-automaton is a complete $\mathscr{S}$-automaton and the action of $\bm{p}\in Q^{+}$ as a state sequence over $Q$ (with respect $\mathcal{T}$) is the same as the action of $\bm{p}\in Q^{|\bm{p}|}$ as a state of $\mathcal{T}^{|\bm{p}|}$, which makes the notation $\bm{p}\circ u$ unambiguous. The same holds for $\bm{p}\cdot u$ by the construction of the power automaton. The semigroup generated by the union of a complete $\mathscr{S}$-automaton with some of its powers is the same as the semigroup generated by the original automaton. This allows us to use the power automaton construction to make sure that any fixed state sequence acts in the same way as a single state of the automaton. For our results later on, it will be important to note here that power and union automata are computable.

For the remainder of this paper, we fix an arbitrary complete $\mathscr{S}$-automaton $\mathcal{T}=(Q,\Sigma,\delta)$.

Orbits.

For a language $R\subseteq Q^{*}$, the $R$-orbit of a word $w\in\Sigma^{*}\cup\Sigma^{\omega}$ is $R\circ w=\{\bm{r}\circ w\mid\bm{r}\in R\}$. The $Q^{*}$-orbit of $w$ is also simply called the orbit of $w$. The orbital transducer $\mathcal{T}\circ w$ of $w\in\Sigma^{*}$ is the complete $\mathscr{S}$-automaton with state set $Q^{*}\circ w$ and alphabet $Q$ whose transitions are given by

$$\{\leavevmode\hbox to36.23pt{\vbox to11.3pt{\pgfpicture\makeatletter\hbox{\hskip 6.49673pt\lower-4.09721pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.86229pt}{-2.15277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$u$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.5283pt}{-2.15277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$p\circ u$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{6.1953pt}{0.0pt}\pgfsys@lineto{10.79524pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{1.59535pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-6.49673pt}{1.95pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$p/p\cdot u$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mid u,v\in Q^{*}\circ w,p,q\in Q\}\text{.} u p\circ u p/p\cdot u u p\circ u p/p\cdot u$$

We designate $w$ as the root of $\mathcal{T}\circ w$. Since $\bm{p}\circ u$ is a left action, it is natural to write the runs of $\mathcal{T}\circ w$ from right to left. Thus, we write

to indicate that $\mathcal{T}\circ w$ contains a run from $u_{0}$ to $u_{\ell}$ with input $p_{1}\dots p_{\ell}$ and output $q_{1}\dots q_{\ell}$ (where $p_{1},\dots,p_{\ell},q_{1},\dots,q_{\ell}\in Q$). Notice that, for $p_{\ell}\dots p_{1}=\bm{p}$ and $q_{\ell}\dots q_{1}=\bm{q}$, such a run means that we have $u_{\ell}=\bm{p}\circ u_{0}=p_{\ell}\dots p_{1}\circ u_{0}$ and $q_{\ell}\dots q_{1}=\bm{q}=\bm{p}\cdot u_{0}=p_{\ell}\dots p_{1}\cdot u_{0}$, which justifies this somewhat reverse notation. As a short-hand notation, we also write for the same run. Often, we will not be interested in the input of the run and simply write to indicate that there is a run for some $\bm{p}\in Q^{+}$.

The Product $\mathcal{T}\circ w\times R$.

For some language $R\subseteq Q^{*}$, the product $\mathcal{T}\circ w\times R$ is a possibly infinite $\mathscr{S}$-automaton over the alphabet $Q$. Its states are of the form $(u,C)$ where $u\in Q^{*}\circ w$ and $C$ is a class of $R$ and we have a transition if we have a transition in $\mathcal{T}\circ w$. We restrict $\mathcal{T}\circ w\times R$ to the part reachable from its root $(w,\mathscr{C}(\varepsilon))$. We use the same conventions to write transitions and runs in $\mathcal{T}\circ w\times R$ as in $\mathcal{T}\circ w$. In particular, we omit the input label if we are not interested in it.

Note that we have a run in $\mathcal{T}\circ w\times R$ if and only if we have $u=\bm{p}\circ w$, $\bm{q}=\bm{p}\cdot w$ and $C=\mathscr{C}(\bm{p})$. Furthermore, $\mathcal{T}\circ w\times R$ is finite if $R$ is regular.

Expandability.

A finite word $w\in\Sigma^{*}$ is $R$-expandable for $R\subseteq Q^{*}$ if there is some $x\in\Sigma^{*}$ with $|R\circ w|<|R\circ wx|$. In this case, $x$ is said to $R$-expand $w$.

Remark.

The notion of expandability was introduced in [9] where it was shown that it is decidable whether a given word is expandable with respect to the action of a given $\mathscr{S}$-automaton and that there is a bound on the length of the expanding suffix.

Generalized Activity.

We say that a subset $S\subseteq Q$ of states of $\mathcal{T}$ is closed (under the dual action) if we have

$$S\cdot\Sigma^{*}=\{s\cdot u\mid s\in S,u\in\Sigma^{*}\}\subseteq S\text{.}$$

For such a closed subset $S$, we may consider the restriction $\delta|_{S}$ of $\delta$ into a relation $\delta|_{S}\subseteq S\times\Sigma\times\Sigma\times S$, which yields a complete $\mathscr{S}$-automaton $\mathcal{T}|_{S}=(S,\Sigma,\delta|_{S})$. Notice that the action $\bm{s}\circ u$ of some $\bm{s}\in S^{+}$ is the same when we consider it with respect to $\mathcal{T}$ or with respect to $\mathcal{T}|_{S}$. This justifies that we define the semigroup generated by $\mathcal{T}|_{S}$ as $S^{+}/{=_{\mathcal{T}}}$ (which is the subsemigroup generated by $S$ in the semigroup generated by $\mathcal{T}$).

We are mostly interested in the case that this generated semigroup is finite. Therefore, we fix an arbitrary closed subset $S\subseteq Q$ such that the generated semigroup $S^{+}/{=_{\mathcal{T}}}$ is finite.

For a state sequence $\bm{p}\in Q^{+}$, we define its set of $S$-active words of length $n\in\mathbb{N}$ as

$$A_{\bm{p}}(n)=\{v\mid\exists u\in\Sigma^{n}:\bm{p}\circ u=v,\bm{p}\cdot u\not\in_{\mathcal{T}}S^{+}\}$$

and the set of $S$-active words as $A_{\bm{p}}=\bigcup_{n\geq 0}A_{\bm{p}}(n)$. The $S$-activity of $\bm{p}$ is the growth of the function $n\mapsto\alpha_{\bm{p}}(n)=|A_{\bm{p}}(n)|$.

Please note that, instead of considering $\bm{p}$ as a state sequence over $Q$, we may also consider it as a single state of $\mathcal{T}^{|\bm{p}|}$ and obtain the same sets of active words.

With regard to orbital transducers, a word $v\in\Sigma^{n}$ is $S$-active (i. e. in $A_{\bm{p}}(n)$) if and only if there is some $u\in\Sigma^{n}$ with a run in $\mathcal{T}\circ u$ such that $\bm{q}\not\in_{\mathcal{T}}S^{+}$. In other words, we collect all the words that have an ingoing run in any orbital transducer $\mathcal{T}\circ w$ whose output is not labeled by an element contained in the subsemigroup generated by $S$.

Remark.

Our notion of $S$-activity generalizes the activity notion for automaton monoids introduced in [1]. An automaton monoid is an automaton semigroup generated by a complete $\mathscr{S}$-automaton $\mathcal{T}=(Q,\Sigma,\delta)$ containing an identity state $e\in Q$ (i. e. we have $\leavevmode\hbox to15.98pt{\vbox to9.35pt{\pgfpicture\makeatletter\hbox{\hskip 2.32813pt\lower-2.15277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.32813pt}{-2.15277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$e$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{8.99414pt}{-2.15277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$e$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{5.66113pt}{0.0pt}\pgfsys@lineto{10.26108pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{1.06119pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.01115pt}{1.95pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$a/a$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\in\delta$ for all $a\in\Sigma$). For such an automaton, the set $\{e\}$ is clearly closed and its generated subsemigroup is the trivial monoid (and, thus, in particular finite). The activity defined in [1] is then precisely the $\{e\}$-activity in our terminology. In fact, [1] already contains an extension of the activity notion where the set $S$ is given by the NoCyWEx part of the generating automaton (which always generates a finite subsemigroup).

The activity notion for automaton monoids from [1] is, in turn, a generalization of the original activity notion for automaton groups (which are generated by invertible automata) introduced by Sidki [27]. The main difference is that, in the group case, we may use the input words to define the set of active words, i. e. we could let

$$A_{\bm{p}}(n)=\{u\in\Sigma^{n}\mid\bm{p}\circ u\neq_{\mathcal{T}}e\}$$

(where $e$ is the identity state). The straight-forward generalization of this definition to automaton monoids is not well-behaved (and we refer the reader to [1] for more details on this).

Our generalization of the activity notion maintains many desirable properties of the original notion(s). First, it remains subadditive (compare to [1, Lemma 5]).

Fact 2.4.

For $\bm{p},\bm{q}\in Q^{+}$, we have $\alpha_{\bm{q}\bm{p}}(n)\leq\alpha_{\bm{q}}(n)+\alpha_{\bm{p}}(n)$ for all $n\geq 0$.

Proof.

We show $A_{\bm{qp}}(n)\subseteq A_{\bm{q}}(n)\cup\bm{q}\circ A_{\bm{p}}(n)$ where $\bm{q}\circ A_{\bm{p}}(n)=\{\bm{q}\circ v\mid v\in A_{\bm{p}}(n)\}$ and, thus, $|\bm{q}\circ A_{\bm{p}}(n)|\leq|A_{\bm{p}}(n)|=\alpha_{\bm{p}}(n)$.

Suppose we have $w\in A_{\bm{qp}}(n)$. By definition, there is some $u\in\Sigma^{n}$ with $\bm{qp}\circ u=w$ and $\bm{qp}\not\in_{\mathcal{T}}S^{+}$. We cannot have $\bm{p}\cdot u\in_{\mathcal{T}}S^{+}$ and $\bm{q}\cdot v\in_{\mathcal{T}}S^{+}$ for $v=\bm{p}\circ u$ since this would imply $\bm{qp}\cdot u=(\bm{q}\cdot v)(\bm{p}\cdot u)\in_{\mathcal{T}}S^{+}$. Thus, we have $\bm{p}\cdot u\not\in_{\mathcal{T}}S^{+}$ or $\bm{q}\cdot v\not\in_{\mathcal{T}}S^{+}$. In the first case, we have $v=\bm{p}\circ u\in A_{\bm{p}}(n)$ and, thus, $w=\bm{q}\circ v\in\bm{q}\circ A_{\bm{p}}(n)$. In the second case, we have $w\in A_{\bm{q}}(n)$ directly by definition. ∎

Next, the set of $S$-active words is regular.

Fact 2.5.

The set of $S$-active words $A_{\bm{p}}$ is regular for all state sequences $\bm{p}\in Q^{+}$.

Proof.

We will describe how to obtain (in fact, compute) a non-deterministic finite acceptor (NFA) recognizing $A_{\bm{p}}$. We refer the reader to [1], [30] or a standard textbook on formal language theory (such as [18]) for proper definitions of NFAs and how they relate to our definition of regular languages.

Recall that we may consider $\bm{p}$ as a single state of the power automaton $\mathcal{T}^{|\bm{p}|}$ (and still obtain the same set of active words). By replacing $\mathcal{T}$ with $\mathcal{T}^{|\bm{p}|}$, we may, thus, without loss of generality assume $\bm{p}=p\in Q$. We mark all states $q$ in $\mathcal{T}$ with $q\not\in_{\mathcal{T}}S^{+}$ as accepting and $p$ as initial. Afterwards, we drop the inputs from all transitions and obtain an NFA. By construction, we obtain that the words accepted by this are precisely the $S$-active ones. ∎

The growth of a language $L\subseteq\Sigma^{*}$ is the growth of the function $n\mapsto\gamma_{L}(n)=|L\cap\Sigma^{n}|$. Thus, by definition, $\alpha_{\bm{p}}$ is the growth function of the language of $S$-active words. It is well-known that a regular language either grows polynomially of exponentially (see e. g. [30, Subsection 6.5.1]). Here, exponential growth means that there is some $r>1$ such that $\gamma_{L}(n)\geq r^{n}$ for infinitely many $n$ (while, of course, $\gamma_{L}(n)\leq|\Sigma|^{n}$ for all $n$) and polynomial growth of degree exactly $d\geq 0$ means that there is some $d$ and polynomials $p(n)$ and $q(n)$ of degree $d$ with $\gamma_{L}(n)\geq p(n)$ for infinitely many $n$ and $\gamma_{L}(n)\leq q(n)$ for all $n$. The special case of polynomial growth of degree $-\infty$ occurs if $\gamma_{L}$ eventually becomes the constant zero function (which happens if and only if $L$ is a finite language). We say that a language has polynomial growth of degree at most $d$ if it has polynomial growth of degree exactly $d^{\prime}$ for some $d^{\prime}\leq d$.

Now, a language has polynomial growth if it has polynomial growth of degree $d$ for some $d\in\{-\infty\}\cup\mathbb{N}$. Since the $S$-activity of the state sequence $\bm{p}$ is the growth of its language of $S$-active words, this immediately induces definitions of polynomial or exponential $S$-activity and we obtain:

Fact 2.6.

The $S$-activity of a state sequence is either polynomial or exponential.

One important special case of polynomial $S$-activity occurs when there is a constant bounding $\alpha_{\bm{p}}(n)$ for all $n$. In this case, the $S$-activity of $\bm{p}$ is called bounded and this is what we will mostly be concerned with in this paper. If $\alpha_{\bm{p}}(n)$ eventually becomes the constant zero function (i. e. if the language of $S$-active words is finite), we say that $\bm{p}$ is $S$-finitary.

Extension to Automata.

The subadditivity stated in Fact 2.4 ensure that, if we take two state sequences $\bm{q}$ and $\bm{p}$ of polynomial activity (or bounded activity), then their concatenation $\bm{q}\bm{p}$ remains to have polynomial (bounded) activity. This justifies that we may define the activity of the entire $\mathscr{S}$-automaton $\mathcal{T}=(Q,\Sigma,\delta)$ as the activity of the states. More precisely, we define the set of $S$-active words of length $n$ for the whole automaton as

$$A(n)=\bigcup_{q\in Q}A_{q}(n)$$

and the $S$-activity of $\mathcal{T}$ as the growth of the function $n\mapsto\alpha(n)=|A(n)|$. Clearly, we have $\alpha_{p}(n)\leq\alpha(n)\leq\sum_{q\in Q}\alpha_{q}(n)$ for all $n\in\mathbb{N}$ and $p\in Q$. Thus, and by Fact 2.4, we also have that the $S$-activity of any state sequence $\bm{p}\in Q^{+}$ is polynomial with degree at most $d$ if the $S$-activity of $\mathcal{T}$ is. This underlines that our definition is useful.

As with state sequences, we say that $\mathcal{T}$ is of bounded $S$-activity if there is some constant bounding the $S$-activity of $\mathcal{T}$ and we say that $\mathcal{T}$ is $S$-finitary if all states of $\mathcal{T}$ are.

Example 2.7.

The adding machine from Example 2.3 is well known to have bounded $\{e\}$-activity.

However, our extended notion of activity allows us to go beyond groups and monoids. Let $S$ be a semigroup that is not a monoid. We may adjoin a new element $e$ to $S$ with $e^{2}=e$ and $es=s=se$ for all $s\in S$ and obtain the monoid $S^{e}$. It is easy to see that $S$ acts faithfully on $S^{e}$ by left translation (see e. g. [19, Theorem 1 .1.2]), which basically shows that $(S,S^{e},\delta)$ with

$$\delta =\{\leavevmode\hbox to16.28pt{\vbox to9.35pt{\pgfpicture\makeatletter\hbox{\hskip 2.46382pt\lower-2.15277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.34375pt}{-2.15277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$s$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.00977pt}{-2.15277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$s$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{5.67676pt}{0.0pt}\pgfsys@lineto{10.2767pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{1.07681pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.46382pt}{1.95pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$t/st$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mid s\in S,t\in S^{e}\} s s t/st s s t/st$$

is a complete $\mathscr{S}$-automaton generating $S$ (see [7, Proposition 4.6]). The activity of this automaton in the sense of [1] is exponential but it is trivially $S$-finitary. The generating automaton is NoCyWEx in the sense of [1] and, thus, also finitary in the more extended sense defined there.

However, there are also non-NoCyWEx automata generating finite semigroups. For example, the complete $\mathscr{S}$-automaton

with alphabet $\{a,\bot\}$ generates the monoid $U_{1}=\{e,z\}$ with $e^{2}=e$ and $z^{2}=ez=ze=z$. As $z$ is not the neutral element, this automaton has exponential activity in the sense of [1] and it has bounded activity (but is not finitary!) in the NoCyWEx-sense of [1].

We may even go further. As an example, consider the complete $\mathscr{S}$-automaton $\mathcal{T}=(\{q,e,z\},\{0,1,a,\bot\},\delta)$

which combines the above example (with additional $0/0$- and $1/1$-self-loops at all states that do not change the generated semigroup) with the adding machine from Example 2.3. Using an induction on $|u|\in\{0,1,a,\bot\}^{*}$ and an exhaustive calculation, one may easily see that all states commute in the generated semigroup and that we have $qe=_{\mathcal{T}}q$, which turns $e$ into a neutral element. Next, we have

$$q^{i}\circ 0^{\ell}=q^{i}e\circ 0^{\ell}=q^{i}z\circ 0^{\ell}=\operatorname{bin}_{\ell}i$$

(for $\ell$ sufficiently large), which shows $q^{i}s\neq_{\mathcal{T}}q^{j}t$ for all $i\neq j$ and $s,t\in\{e,z\}$. Finally, we clearly have $q^{i}e\neq_{\mathcal{T}}q^{i}z$ for all $i\geq 0$ and, thus, that the semigroup generated by $\mathcal{T}$ is (isomorphic to) $q^{*}\times U_{1}$.

The interesting part about this last example $\mathcal{T}$ is that the automaton has exponential activity both with respect to the identity function (and even its neutral element $e$) as well as to its NoCyWEx part (which only contains of $z$). Nevertheless, it has bounded $\{e,z\}$-activity (where the subsemigroup generated by $e$ and $z$ is (isomorphic to) $U_{1}$).

Remark 2.8.

The isomorphism problem for automaton group and, thus, for automaton semigroups is undecidable (this follows from [28] but, in the semigroup case, also from the direct construction in [11]). However, the (uniform) word problem is decidable (in fact, it is PSpace-complete [10, 29], see also [30]). Thus, for any fixed finite semigroup $T$, we may test whether there is a subset $P$ of states whose generated subsemigroup is isomorphic to $T$: We enumerate all elements of the subsemigroup (for example, using breath-first search in the Cayley graph) until we have found all elements or more than $|T|$-many elements. In the second case, the subsemigroup cannot be isormorphic to $T$ and, in the first case, we may test the isomorphism between finite semigroups. This allows us to consider our notion of $S$-activity in a more abstract sense where, instead of fixing a subset of states, we fix some finite semigroup $T$ and search for a closed subset of states generating $T$.

3 Expansion Relation

Recall that we fixed some complete $\mathscr{S}$-automaton $\mathcal{T}=(Q,\Sigma,\delta)$ and some closed subset $S\subseteq Q$ such that $S^{+}/{=_{\mathcal{T}}}$ is finite. Without loss of generality, we may assume that for every $\bm{t}\in S^{+}$, there is exactly one $s\in S$ with $\bm{t}=_{\mathcal{T}}s$: since there are only finitely many equivalence classes under $=_{\mathcal{T}}$, we may replace $\mathcal{T}$ by a finite union of suitable powers of $\mathcal{T}$ and then minimize the automaton to avoid multiple states with the same action.

We write $P=Q\setminus S$ for the states outside the closed subset and consider the free product $(S^{+}/{=_{\mathcal{T}}})\star P^{+}=Q^{+}/{\approx}$ of semigroups. In other words, two words $\bm{p},\bm{q}\in Q^{+}$ are equivalent under $\approx$ if they are the same up to reductions within the $S^{+}$ blocks. To simplify our notation, we also define $\varepsilon\approx\varepsilon$. In this free product, we may define the normal form of some word $\bm{p}_{0}\bm{t}_{1}\bm{p}_{1}\ldots\bm{t}_{n}\bm{p}_{n}$ with $\bm{p}_{0},\bm{p}_{n}\in P^{*}$, $\bm{p}_{1},\dots,\bm{p}_{n-1}\in P^{+}$ and $\bm{t}_{1},\dots,\bm{t}_{n}\in S^{+}$ as $\bm{p}_{0}s_{1}\bm{p}_{1}\dots s_{n}\bm{p}_{n}$ where $s_{i}$ is the unique element $s_{i}\in S$ with $s_{i}\equiv\bm{t}_{i}$ for $1\leq i\leq n$.

Example 3.1.

If our automaton $\mathcal{T}$ contains an identity state $e$ and we choose $S=\{e\}$, then taking the normal form of some $\bm{p}\in Q^{+}$ is to reduce all blocks of the form $e^{n}$ to a single $e$. Accordingly, $\bm{p}\approx\bm{q}$ holds if and only if we end up with the same word when doing this for $\bm{p}$ and for $\bm{q}$.

It is not difficult to see that $Q^{+}/{=_{\mathcal{T}}}$, the semigroup generated by $\mathcal{T}$, is a quotient of $Q^{+}/{\approx}$:

Fact 3.2.

We have $\bm{p}\approx\bm{q}\implies\bm{p}=_{\mathcal{T}}\bm{q}$ for all $\bm{p},\bm{q}\in Q^{+}$.

Similarly, the action $\bm{q}\cdot u$ is compatible with the classes of $\approx$ since it is compatible with the classes of $=_{\mathcal{T}}$ (i. e. the semigroup generate by $\mathcal{T}$):

Fact 3.3.

We have $\bm{p}\approx\bm{q}\implies\bm{p}\cdot u\approx\bm{q}\cdot u$ for all $\bm{p},\bm{q}\in Q^{+}$ and $u\in\Sigma^{*}$.

To further simplify our notation from here on, we fix some language $R\subseteq Q^{*}$ and simply say that a finite word is expandable if it is $R$-expandable. Similarly, we say that $x\in\Sigma^{+}$ expands some $w\in\Sigma^{*}$ if it $R$-expands it.

We now use the above free product to define a relation that will allow us to detect whether a word $w\in\Sigma^{*}$ is expandable for not. The idea is basically that two state sequences $\bm{p}$ and $\bm{q}$ are equivalent if there are runs and to the same word in the orbital transducer of $w$. However, we will do this only “up to equality in the $S^{+}$ blocks” and this is where the free product comes into play. Additionally, we also have to keep track of the classes of the inputs (with respect to $R$).

Definition 3.4.

For $w\in\Sigma^{*}$, we define the expansion relation $\mathcal{E}_{w}\subseteq Q^{+}\times Q^{+}$ by

$$\bm{p}_{1}\mathrel{\mathcal{E}_{w}}\bm{p}_{2}\iff\exists\bm{p}_{1}^{\prime},\bm{p}_{2}^{\prime}\in Q^{+}\text{ with } \bm{p}_{1}\approx\bm{p}_{1}^{\prime},\bm{p}_{2}\approx\bm{p}_{2}^{\prime}\text{ and}$$

$$\text{runs }\leavevmode\hbox to19.3pt{\vbox to8.64pt{\pgfpicture\makeatletter\hbox{\hskip 2.603pt\lower-2.15277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.603pt}{-2.15277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$v$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.26901pt}{-2.15277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$w$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{{}}{{}}}{}{{}}{}{{}}{{{}}{{}}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{{{}{}}} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}{{}}} {}{}{}{}{{}}\pgfsys@moveto{5.936pt}{-0.71132pt}\pgfsys@lineto{10.53595pt}{-0.71132pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{1.33606pt}{-0.71132pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-0.7702pt}{1.23868pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$\bm{r}^{\prime}_{1}/\bm{p}_{1}^{\prime}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\text{ and }\leavevmode\hbox to19.3pt{\vbox to8.64pt{\pgfpicture\makeatletter\hbox{\hskip 2.603pt\lower-2.15277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.603pt}{-2.15277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$v$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.26901pt}{-2.15277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$w$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{{}}{{}}}{}{{}}{}{{}}{{{}}{{}}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{{{}{}}} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}{{}}} {}{}{}{}{{}}\pgfsys@moveto{5.936pt}{-0.71132pt}\pgfsys@lineto{10.53595pt}{-0.71132pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{1.33606pt}{-0.71132pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-0.7702pt}{1.23868pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$\bm{r}^{\prime}_{2}/\bm{p}_{2}^{\prime}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\text{ in }\mathcal{T}\circ w v w \bm{r}^{\prime}_{1}/\bm{p}_{1}^{\prime} v w \bm{r}^{\prime}_{2}/\bm{p}_{2}^{\prime} v w \bm{r}^{\prime}_{1}/\bm{p}_{1}^{\prime} v w \bm{r}^{\prime}_{2}/\bm{p}_{2}^{\prime}$$

$$\text{for some }v\in Q^{*}\circ w\text{ and }\bm{r}^{\prime}_{1},\bm{r}^{\prime}_{2}\in R\text{.}$$

Note that $\mathcal{E}_{w}$ implicitly depends on $R$.

We will show that $\mathcal{E}_{w}$ can be used to test whether $w$ is expandable:

Proposition 3.5.

A word $x\in\Sigma^{*}$ expands a word $w\in\Sigma^{*}$ if and only if there are some $\bm{p}_{1},\bm{p}_{2}\in Q^{+}$ with $\bm{p}_{1}\mathrel{\mathcal{E}_{w}}\bm{p}_{2}$ and $\bm{p}_{1}\circ x\neq\bm{p}_{2}\circ x$.

Proof.

Consider the surjective map $\pi:R\circ wx\to R\circ w$, $\bm{r}\circ wx\mapsto\bm{r}\circ w$. It is injective if and only if $|R\circ wx|=|R\circ w|$ (i. e. $x$ does not expand $w$).

For the first direction, suppose that it is not injective. Then, there are $\bm{r}_{1},\bm{r}_{2}\in R$ with $\bm{r}_{1}\circ wx\neq\bm{r}_{2}\circ wx$ but $\bm{r}_{1}\circ w=v=\bm{r}_{2}\circ w$. The latter implies that there are runs and in $\mathcal{T}\circ w$ with $\bm{p}_{1}=\bm{r}_{1}\cdot w$ and $\bm{p}_{2}=\bm{r}_{2}\cdot w$, which means that we have $\bm{p}_{1}\mathrel{\mathcal{E}_{w}}\bm{p}_{2}$. The former implies $v(\bm{p}_{1}\circ x)=(\bm{r}_{1}\circ w)(\bm{r}_{1}\cdot w\circ x)=\bm{r}_{1}\circ wx\neq\bm{r}_{2}\circ wx=(\bm{r}_{2}\circ w)(\bm{r}_{2}\cdot w\circ x)=v(\bm{p}_{2}\circ x)$. Thus, we have $\bm{p}_{1}\circ x\neq\bm{p}_{2}\circ x$.

For the other direction, suppose that $\pi$ is injective and that we have $\bm{p}_{1},\bm{p}_{2}\in Q^{+}$ with $\bm{p}_{1}\mathrel{\mathcal{E}_{w}}\bm{p}_{2}$. By definition, there are $\bm{p}_{1}^{\prime},\bm{p}_{2}^{\prime}$ with $\bm{p}_{1}\approx\bm{p}_{1}^{\prime}$, $\bm{p}_{2}\approx\bm{p}_{2}^{\prime}$ and runs and in $\mathcal{T}\circ w$. Thus, we have $\bm{r}_{1}^{\prime}\circ w=v=\bm{r}_{2}^{\prime}\circ w$ and, since $\pi$ is injective, also $\bm{r}_{1}^{\prime}\circ wx=\bm{r}_{2}^{\prime}\circ wx$. We obtain $v(\bm{p}_{1}^{\prime}\circ x)=(\bm{r}_{1}^{\prime}\circ w)(\bm{r}_{1}^{\prime}\cdot w\circ x)=\bm{r}_{1}^{\prime}\circ wx=\bm{r}_{2}^{\prime}\circ wx=(\bm{r}_{2}^{\prime}\circ w)(\bm{r}_{2}^{\prime}\cdot w\circ x)=v(\bm{p}_{2}^{\prime}\circ x)$, which implies $\bm{p}_{1}\circ x=\bm{p}_{1}^{\prime}\circ x=\bm{p}_{2}^{\prime}\circ x=\bm{p}_{2}\circ x$ since we have $\bm{p}_{1}=_{\mathcal{T}}\bm{p}_{1}^{\prime}$ and $\bm{p}_{2}=_{\mathcal{T}}\bm{p}_{2}^{\prime}$ by Fact 3.2. ∎

An immediate consequence of the last result is that expandability only depends on the expansion relation:

Proposition 3.6.

For all $u,v,x\in\Sigma^{*}$, we have

$$\mathcal{E}_{u}=\mathcal{E}_{v}\implies\left(|R\circ u|<|R\circ ux|\iff|R\circ v|<|R\circ vx|\right)\text{.}$$

Proof.

Let $\mathcal{E}_{u}=\mathcal{E}_{v}$ and $|R\circ u|<|R\circ ux|$. By Proposition 3.5, there are $\bm{p}_{1},\bm{p}_{2}\in Q^{+}$ with $\bm{p}_{1}\mathrel{\mathcal{E}_{u}}\bm{p}_{2}$ and $\bm{p}_{1}\circ x\neq\bm{p}_{2}\circ x$. The former is the same as $\bm{p}_{1}\mathrel{\mathcal{E}_{v}}\bm{p}_{2}$ and, form the other direction of Proposition 3.5, we obtain $|R\circ v|<|R\circ vx|$. ∎

We have just seen that it suffices to know the expansion relation for a word $w$ to answer the question whether a given $x$ expands $w$. Next, we will see that the expansion relation is compatible with appending a word.

Proposition 3.7.

For all $u,v,x\in\Sigma^{*}$, we have $\mathcal{E}_{u}=\mathcal{E}_{v}\implies\mathcal{E}_{ux}=\mathcal{E}_{vx}$.

Proof.

We will only show the statement for $x=a\in\Sigma$ since the general case follows from this using an induction. Assume that we have $\mathcal{E}_{u}=\mathcal{E}_{v}$ for some $u,v\in\Sigma^{*}$. If we have $\bm{q}_{1}\mathrel{\mathcal{E}_{ua}}\bm{q}_{2}$ for some $\bm{q}_{1},\bm{q}_{2}\in Q^{+}$, then there are $\bm{q}_{1}^{\prime},\bm{q}_{2}^{\prime}\in Q^{+}$ and $\bm{r}^{\prime}_{1},\bm{r}^{\prime}_{2}\in R$ with $\bm{q}_{1}\approx\bm{q}_{1}^{\prime}$, $\bm{q}_{2}\approx\bm{q}_{2}^{\prime}$ and runs and in $\mathcal{T}\circ ua$ for some $u^{\prime}\in\Sigma^{*}$ and $a^{\prime}\in\Sigma$. By the construction of $\mathcal{T}\circ ua$ this is only possible if there are $\bm{p}_{1}^{\prime},\bm{p}_{2}^{\prime}\in Q^{+}$ with $\bm{p}_{1}^{\prime}\cdot a=\bm{q}_{1}^{\prime}$, $\bm{p}_{2}^{\prime}\cdot a=\bm{q}_{2}^{\prime}$, $\bm{p}_{1}^{\prime}\circ a=a^{\prime}=\bm{p}_{2}^{\prime}\circ a$ and runs and in $\mathcal{T}\circ u$, which implies that we have $\bm{p}^{\prime}_{1}\mathrel{\mathcal{E}_{u}}\bm{p}^{\prime}_{2}$ and, thus, $\bm{p}^{\prime}_{1}\mathrel{\mathcal{E}_{v}}\bm{p}^{\prime}_{2}$.

This, in turn, implies that there are $\bm{p}_{1}^{\prime\prime},\bm{p}_{2}^{\prime\prime}\in Q^{+}$ and $\bm{r}^{\prime\prime}_{1},\bm{r}^{\prime\prime}_{2}\in R$ with $\bm{p}_{1}^{\prime\prime}\approx\bm{p}_{1}^{\prime}$, $\bm{p}_{2}^{\prime\prime}\approx\bm{p}_{2}^{\prime}$ and runs and in $\mathcal{T}\circ v$ for some $v^{\prime}\in\Sigma^{*}$. From this follows $\bm{p}_{1}^{\prime}\equiv\bm{p}_{1}^{\prime\prime}$ and $\bm{p}_{2}^{\prime}\equiv\bm{p}_{2}^{\prime\prime}$ by Fact 3.2, which, in particular, means $a^{\prime}=\bm{p}_{1}^{\prime}\circ a=\bm{p}_{1}^{\prime\prime}\circ a$ and $a^{\prime}=\bm{p}_{2}^{\prime}\circ a=\bm{p}_{2}^{\prime\prime}\circ a$. Thus, we have runs and in $\mathcal{T}\circ va$ for $\bm{q}_{1}^{\prime\prime}=\bm{p}_{1}^{\prime\prime}\cdot a$ and $\bm{q}_{2}^{\prime\prime}=\bm{p}_{2}^{\prime\prime}\cdot a$. Finally, Fact 3.3 yields $\bm{q}_{1}^{\prime\prime}=\bm{p}_{1}^{\prime\prime}\cdot a\approx\bm{p}_{1}^{\prime}\cdot a=\bm{q}_{1}^{\prime}\approx\bm{q}_{1}$ and $\bm{q}_{2}^{\prime\prime}=\bm{p}_{2}^{\prime\prime}\cdot a\approx\bm{p}_{2}^{\prime}\cdot a=\bm{q}_{2}^{\prime}\approx\bm{q}_{2}$, which shows $\bm{q}_{1}\mathrel{\mathcal{E}_{va}}\bm{q}_{2}$. The other direction is symmetric. ∎

4 Bounded Activity

In this section, we will use the previous results to show that the $\omega$-words with infinite $R$-orbit form a deterministic $\omega$-regular language if the automaton $\mathcal{T}$ is of bounded $S$-activity and $R$ is regular. Therefore, we assume the latter from now on and that there is some constant $K$ bounding all $\alpha(n)$ with $n\in\mathbb{N}$.

4.1 A Finite Acceptor for the Expansion Relation

The basic idea of our approach is that we will store the expansion relation using a finite acceptor whose size is uniformly bounded. While we could use nondeterministic finite-state transducers for this, we will instead introduce a different acceptor model that more closely mimics a minimization of the orbital transducer or, in fact, the product $\mathcal{T}\circ w\times R$.

Definition 4.1.

A nondeterministic finite relation acceptor (NFRA) $\mathcal{A}$ is a tuple $(Z,\Gamma,\tau,\allowbreak z_{0},\mathcal{F})$ where $Z$ is a set of states, $\Gamma$ is an alphabet, $\tau\subseteq Z\times\Gamma\times Z$ is the set of transitions, $z_{0}\in Z$ is the initial state and $\mathcal{F}\subseteq Z\times Z$ is the acceptance relation. For a transition $(y,a,z)$, we also use the graphical notations and .

A run of the NFRA $\mathcal{A}=(Z,\Gamma,\tau,z_{0},\mathcal{F})$ on a word $a_{1}\dots a_{n}$ with $a_{1},\dots,a_{n}\in\Gamma$ is a sequence

with $\leavevmode\hbox to22.91pt{\vbox to12.6pt{\pgfpicture\makeatletter\hbox{\hskip 4.52876pt\lower-3.12498pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.52876pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y_{i-}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.19478pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y_{i}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{7.86177pt}{0.97221pt}\pgfsys@lineto{12.46172pt}{0.97221pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.26183pt}{0.97221pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.33647pt}{4.46487pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$a_{i}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\in\tau$ for all $1\leq i\leq n$. It starts in $y_{0}$ and ends in $y_{n}$. It is initial if $y_{0}=z_{0}$. In short-hand notation, we also denote this run by .

An NFRA $\mathcal{A}=(Z,\Gamma,\tau,z_{0},\mathcal{F})$ accepts a pair $(u,v)\in\Gamma^{*}\times\Gamma^{*}$ if it admits an initial run ending in $z$ on $u$ and an initial run ending in $y$ on $u$ with $z\mathrel{\mathcal{F}}y$. The recognized relation for $\mathcal{A}$ is $\mathscr{R}(\mathcal{A})=\{(u,v)\in\Gamma^{*}\times\Gamma^{*}\mid\mathcal{A}\text{ accepts }(u,v)\}$.

Remark 4.2.

For readers familiar with rational subsets of monoids (see e. g. [12]), we want to point out that $\mathscr{R}(\mathcal{A})$ is indeed a rational relation (in the sense that it is a rational subset of the monoid $\Gamma^{*}\times\Gamma^{*}$). This may be seen from observing that any NFRA $\mathcal{A}=(Z,\Gamma,\tau,z_{0},\mathcal{F})$ may be turned into a (more traditional) non-deterministic, finite-state (spelling) $\Gamma^{*}\times\Gamma^{*}$-acceptor (again, see e. g. [12] for more information on $M$-automata or, as we call them here, $M$-acceptors). The idea is to take $Z\times Z$ as the state set, $(z_{0},z_{0})$ as the initial state, $\mathcal{F}$ as the set of final states and add the transitions

$$\{\leavevmode\hbox to54.6pt{\vbox to15.85pt{\pgfpicture\makeatletter\hbox{\hskip 11.59953pt\lower-5.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.59953pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$(x,y)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{18.26555pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$(x^{\prime},y)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{14.93254pt}{-0.34723pt}\pgfsys@lineto{19.53249pt}{-0.34723pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{10.3326pt}{-0.34723pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{6.9226pt}{3.60277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$(a,\varepsilon)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mid\leavevmode\hbox to19.64pt{\vbox to9.37pt{\pgfpicture\makeatletter\hbox{\hskip 2.85764pt\lower-2.15277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.85764pt}{-2.15277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.52365pt}{-2.15277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x^{\prime}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{6.19064pt}{0.0pt}\pgfsys@lineto{10.79059pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{1.5907pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.34059pt}{2.2pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$a$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\in\tau,y\in Z\} (x,y) (x^{\prime},y) (a,\varepsilon) x x^{\prime} a (x,y) (x^{\prime},y) (a,\varepsilon) x x^{\prime} a$$

$${}\cup \{\leavevmode\hbox to54.6pt{\vbox to15.85pt{\pgfpicture\makeatletter\hbox{\hskip 11.59953pt\lower-5.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.59953pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$(x,y)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{18.26555pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$(x,y^{\prime})$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{14.93254pt}{-0.34723pt}\pgfsys@lineto{19.53249pt}{-0.34723pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{10.3326pt}{-0.34723pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{6.9226pt}{3.60277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$(\varepsilon,a)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mid\leavevmode\hbox to18.73pt{\vbox to11.31pt{\pgfpicture\makeatletter\hbox{\hskip 2.6308pt\lower-3.125pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.6308pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.29681pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y^{\prime}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{5.9638pt}{0.97221pt}\pgfsys@lineto{10.56375pt}{0.97221pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{1.36386pt}{0.97221pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.11375pt}{3.17221pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$a$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\in\tau,x\in Z\}\text{.} (x,y) (x,y^{\prime}) (\varepsilon,a) y y^{\prime} a (x,y) (x,y^{\prime}) (\varepsilon,a) y y^{\prime} a$$

It is now a routine matter to check that the NFRA $\mathcal{A}$ accepts a pair $(u,v)$ if and only if there is an initial run ending in a final state in the thus constructed acceptor where the concatenation of the first components of the transitions on that run is exactly $u$ and the concatenation of the second components is exactly $v$.

We will describe an NFRA that recognizes the expansion relation $\mathcal{E}_{w}$ for some word $w\in\Sigma^{*}$, which we fix for the rest of this subsection to simplify our notation. Additionally, we define $A=A(|w|)$. Remember that we have $|A|\leq K$.

Definition 4.3.

Let

$$Z={} \{(u,\varepsilon,C,C)\mid u\in A\cup\{w\},C\text{ class of }R\}\cup{}$$

$$\{(u,s,C,D)\mid u\in A\cup\{w\},s\in S,C\text{ and }D\text{ classes of }R\}\text{.}$$

For every $\bm{t}\in S^{+}$, $u\in A\cup\{w\}$ and every pair $C,D$ of classes of $R$, there is exactly one element $(u,s,C,D)$ in $Z$ with $\bm{t}=_{\mathcal{T}}s$. For convenience, we write $(u,\bm{t},C,D)$ for this unique element.

Define

$$\mathscr{W}:Z \to\mathcal{P}(Q^{*}\circ w)$$

$$(u,\varepsilon,C,C) \mapsto\{u\}$$

$$(u,s,C,D) \mapsto\{u^{\prime}\mid\exists\bm{t}\in S^{+}:s=_{\mathcal{T}}\bm{t},\leavevmode\hbox to60.52pt{\vbox to11.14pt{\pgfpicture\makeatletter\hbox{\hskip 14.02187pt\lower-5.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-14.02187pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$(u^{\prime},D)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{20.68788pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$(u,C)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{{}}{{}}}{}{{}}{}{{}}{{{}}{{}}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{{{}{}}} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}{{}}} {}{}{}{}{{}}\pgfsys@moveto{17.35487pt}{-1.05855pt}\pgfsys@lineto{21.95482pt}{-1.05855pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{12.75493pt}{-1.05855pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{14.34099pt}{0.89145pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$/\bm{t}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\text{ in }\mathcal{T}\circ w\times R\}\text{ for }s\in S\text{.} (u^{\prime},D) (u,C) /\bm{t} (u^{\prime},D) (u,C) /\bm{t}$$

and let $\mathcal{A}_{w}$ denote the NFRA with states $Z$, alphabet $Q$, transitions

$$\{\leavevmode\hbox to100.72pt{\vbox to11.87pt{\pgfpicture\makeatletter\hbox{\hskip 23.3341pt\lower-5.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.3341pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$(u,\varepsilon,C,C)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{30.00012pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$(u,s,C,D)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{26.66711pt}{-0.34723pt}\pgfsys@lineto{31.26706pt}{-0.34723pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{22.06717pt}{-0.34723pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{25.02649pt}{1.85277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$s$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mid\begin{aligned} &u\in A\cup\{w\},C\text{ class of }R,\\ &s\in S,D\text{ class of }R\}\end{aligned} (u,\varepsilon,C,C) (u,s,C,D) s$$

$${}\cup{} \{\leavevmode\hbox to105.05pt{\vbox to13.16pt{\pgfpicture\makeatletter\hbox{\hskip 23.6935pt\lower-5.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.6935pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$(u,s,C,D)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{30.35951pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$(u,st,C,D)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{27.0265pt}{-0.34723pt}\pgfsys@lineto{31.62645pt}{-0.34723pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{22.42656pt}{-0.34723pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{25.76262pt}{1.85277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$t$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mid\begin{aligned} &u\in A\cup\{w\},C,D\text{ classes of }R,\\ &s,t\in S\}\end{aligned} (u,s,C,D) (u,st,C,D) t$$

$${}\cup{} \{\leavevmode\hbox to100.23pt{\vbox to13.23pt{\pgfpicture\makeatletter\hbox{\hskip 23.3341pt\lower-5.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.3341pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$(u,\varepsilon,C,C)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{30.00012pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$(v,\varepsilon,E,E)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{26.66711pt}{-0.34723pt}\pgfsys@lineto{31.26706pt}{-0.34723pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{22.06717pt}{-0.34723pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{24.90617pt}{3.21385pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$p$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mid\begin{aligned} &u\in A\cup\{w\},C\text{ class of }R,\\ &\exists u^{\prime}\in\mathscr{W}(u,\varepsilon,C,C)\text{ with }\\ &\leavevmode\hbox to59.4pt{\vbox to11.85pt{\pgfpicture\makeatletter\hbox{\hskip 12.69327pt\lower-5.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-12.69327pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$(v,E)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{19.35928pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$(u^{\prime},C)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{19.62622pt}{-0.34723pt}\pgfsys@lineto{17.02628pt}{-0.34723pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{19.62622pt}{-0.34723pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.40425pt}{1.60277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$/p$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\text{ in }\mathcal{T}\circ w\times R\\ &\text{for }p\in P\text{ and some class $E$ of $R$}\}\end{aligned} (u,\varepsilon,C,C) (v,\varepsilon,E,E) p (v,E) (u^{\prime},C) /p$$

$${}\cup{} \{\leavevmode\hbox to100.95pt{\vbox to13.23pt{\pgfpicture\makeatletter\hbox{\hskip 23.6935pt\lower-5.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.6935pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$(u,s,C,D)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{30.35951pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$(v,\varepsilon,E,E)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{27.0265pt}{-0.34723pt}\pgfsys@lineto{31.62645pt}{-0.34723pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{22.42656pt}{-0.34723pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{25.26556pt}{3.21385pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$p$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mid\begin{aligned} &u\in A\cup\{w\},C,D\text{ classes of }R,s\in S,\\ &\exists u^{\prime}\in\mathscr{W}(u,s,C,D)\text{ with }\\ &\leavevmode\hbox to60.1pt{\vbox to11.85pt{\pgfpicture\makeatletter\hbox{\hskip 12.69327pt\lower-5.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-12.69327pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$(v,E)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{19.35928pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$(u^{\prime},D)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{19.62622pt}{-0.34723pt}\pgfsys@lineto{17.02628pt}{-0.34723pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{19.62622pt}{-0.34723pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.40425pt}{1.60277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$/p$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\text{ in }\mathcal{T}\circ w\times R\\ &\text{for }p\in P\text{ and some class $E$ of $R$}\}\text{,}\end{aligned} (u,s,C,D) (v,\varepsilon,E,E) p (v,E) (u^{\prime},D) /p$$

initial state $(w,\varepsilon,\mathscr{C}(\varepsilon),\mathscr{C}(\varepsilon))$ and the accepting relation $\mathcal{F}\subseteq Z\times Z$ given by

$$(u,s,C,D)\mathrel{\mathcal{F}}(v,t,E,F)\iff D,F\subseteq R,\mathscr{W}(u,s,C,D)\cap\mathscr{W}(v,t,E,F)\neq\emptyset\text{.}$$

Remark 4.4.

We may define this acceptor for any language $R\subseteq Q^{+}$ but it only remains finite if $R$ has finitely many classes (i. e. if $R$ is regular). The size of the state set $Z$ of $\mathcal{A}_{w}$ is then $(|A\cup\{w\}|)(1\cdot N+|S|\cdot N^{2})\leq(K+1)N(|S|N+1)$ where $N$ is the number of classes of $R$. Thus, the size of $\mathcal{A}_{w}$ is not only finite but uniformly bounded. Furthermore, note that $\mathcal{A}_{w}$ can clearly be computed from $w$, $\mathcal{T}$, $R$ and $S$.

The states of the NFRA represent parts of the orbital transducer $\mathcal{T}\circ w$ or – more precisely – the product $\mathcal{T}\circ w\times R$. This correspondence is given by $\mathscr{W}$: states of the form $(u,\varepsilon,C,C)$ represent the (constantly many) words from $A\cup\{w\}$ with an in-going transition whose output is not from $S$ and the other states of the form $(u,s,C,D)$ represent the words reachable with output equal to $s$ in $\mathscr{S}(\mathcal{T})$ from those words in $A\cup\{w\}$. We have basically attached a copy of the (finite) Cayley graph of $S^{+}/{=_{\mathcal{T}}}$ to every $u\in A\cup\{w\}$. Additionally, we continue to have those transitions whose output is not from $S$.

While we are mostly interested in the output of the transitions in $\mathcal{T}\circ w$, we use the last two components of a state to track the class of $R$ for the input. The first one is used to store the class of the input up to when we entered the last word from $A\cup\{w\}$ and, in the second one, we nondeterministically guess the class of the input when we leave the local copy of the Cayley graph. Of course, it is possible that the nondeterministic choice is impossible to realize; in this case, we have that $\mathscr{W}$ of a state is the empty set.

Proposition 4.5.

The recognized relation of $\mathcal{A}_{w}$ is $\mathcal{E}_{w}$.

Proof.

First, we show the following (which we will refer to as Claim I): if we have a run for some $\bm{r},\bm{q}\in Q^{*}$ and $v\in\Sigma^{*}$ in $\mathcal{T}\circ w$, then, for all $\bm{q}^{\prime}\in Q^{*}$ with $\bm{q}^{\prime}\approx\bm{q}$, we have a run

in $\mathcal{A}_{w}$ for some $u\in A\cup\{w\}$, $s\in S\uplus\{\varepsilon\}$ and class $C$ of $R$ with $v\in\mathscr{W}(u,s,C,\mathscr{C}(\bm{r}))$. From the claim follows that $\bm{p}\mathrel{\mathcal{E}}_{w}\bm{q}$ implies that $\mathcal{A}_{w}$ accepts $(\bm{p},\bm{q})$ for all $\bm{p},\bm{q}\in Q^{+}$.

In order to show Claim I, we first observe that we have a run in $\mathcal{T}\circ w$ if and only if we have a run in $\mathcal{T}\circ w\times R$. We use this fact and an induction on the letters from $P$ and the $S^{+}$ blocks of $\bm{q}$ to show the claim. For the empty state sequence, there is nothing to show as we have $\mathscr{W}(w,\varepsilon,\mathscr{C}(\varepsilon),\mathscr{C}(\varepsilon))=\{w\}$.

Next, we consider the state sequences $\bm{s}\bm{q}$ with $\bm{s}\in S^{+}$ and $\bm{q}\in\{\varepsilon\}\cup PQ^{*}$ and suppose that there is a run in $\mathcal{T}\circ w\times R$ for some $u,u^{\prime}\in\Sigma^{*}$. For every $\bm{q}^{\prime}\in Q^{*}$ with $\bm{q}^{\prime}\approx\bm{q}$, we have a run in $\mathcal{A}_{w}$ by induction (or because $\bm{q}$ is empty). Note here that only states of the form $(u,\varepsilon,C,C)$ have ingoing transitions labeled with elements from $P$ (and that the initial state is of this form as well). To conclude this case we show that we have a run for all $\bm{t}\in S^{+}$ with $\bm{t}\approx\bm{s}$. This is sufficient because we have $u^{\prime}\in\mathscr{W}(u,\bm{s},C,D)$ due to the run in $\mathcal{T}\circ w\times R$. We write $\bm{t}=t_{\ell}\dots t_{2}t_{1}$ for $t_{1},\dots,t_{\ell}\in S$ and observe that we have a run

in $\mathcal{A}_{w}$ by construction.

For the remaining inductive case, consider a state sequence $p\bm{q}$ with $p\in P$ and $\bm{q}\in Q^{*}$ such that there is a run in $\mathcal{T}\circ w\times R$. Let $\bm{q}^{\prime}\in Q^{*}$ be arbitrary with $\bm{q}^{\prime}\approx\bm{q}$. By induction (or because $\bm{q}$ is empty), we have a run in $\mathcal{A}_{w}$ for some $u\in A\cup\{w\}$, $s\in S\uplus\{\varepsilon\}$ and class $E$ of $R$ with $u^{\prime}\in\mathscr{W}(u,s,E,C)$. We also have a transition in $\mathcal{A}_{w}$ by construction because we have the transition in $\mathcal{T}\circ w\times R$. This concludes our proof of Claim I and the first direction as we have $\mathscr{W}(v,\varepsilon,D,D)=\{v\}$.

For the other direction, we show the similar Claim II: if we have a run

in $\mathcal{A}_{w}$ for some $\bm{q}\in Q^{*}$, $u\in A\cup\{w\}$, $s\in S\uplus\{\varepsilon\}$ and classes $C,D$ of $R$, then, for every $u^{\prime}\in\mathscr{W}(u,s,C,D)$, there is some $\bm{q}^{\prime}\in Q^{*}$ with $\bm{q}^{\prime}\approx\bm{q}$, some $\bm{r}^{\prime}\in D$ and a run in $\mathcal{T}\circ w$. The claim implies that $\bm{p}\mathrel{\mathcal{E}_{w}}\bm{q}$ holds if $\mathcal{A}_{w}$ accepts some pair $(\bm{p},\bm{q})\in Q^{+}\times Q^{+}$.

Recall that we have a run in $\mathcal{T}\circ w$ if and only if we have the run in $\mathcal{T}\circ w\times R$. We use this and another induction on the letters from $P$ and the $S^{+}$ blocks of $\bm{q}$ to show claim II. For the empty state sequence, there is nothing to show as we have $\mathscr{W}(w,\varepsilon,\mathscr{C}(\varepsilon),\mathscr{C}(\varepsilon))=\{w\}$.

Therefore, we first consider a state sequence $\bm{s}\bm{q}$ with $\bm{s}\in S^{+}$ and $\bm{q}\in\{\varepsilon\}\cup PQ^{*}$ such that we have a run in $\mathcal{A}_{w}$ for some $u\in A\cup\{w\}$ and classes $C,D$ of $R$. Note that the states on the left have to be of this form due to the construction of $\mathcal{A}_{w}$: only states of the form $(u,\varepsilon,C,C)$ have ingoing transitions labeled with an element from $P$ (and the initial state is of this form) and, from them, we can only reach states of the form $(u,\bm{s},C,D)$ by a run labeled with $\bm{s}$. Since we have $\mathscr{W}(u,\varepsilon,C,C)=\{u\}$, there is some $\bm{q}^{\prime}\in Q^{*}$ with $\bm{q}^{\prime}\approx\bm{q}$ and a run in $\mathcal{T}\circ w\times R$ by induction. We are done with this inductive case if we show that, for every $u^{\prime}\in\mathscr{W}(u,\bm{s},C,D)$, there is a run in $\mathcal{T}\circ w\times R$ for some $\bm{t}\in S^{+}$ with $\bm{t}\approx\bm{s}$. Such a run exists, however, by the definition of $\mathscr{W}(u,\bm{s},C,D)$.

It remains to consider the state sequences $p\bm{q}$ with $p\in P$ and $\bm{q}\in Q^{*}$ such that there is a run in $\mathcal{A}_{w}$ for some $u,v\in A\cup\{w\}$, $s\in S\uplus\{\varepsilon\}$ and classes $C,D,E$ of $R$. Again, the state on the left has to be of this form because only such states have ingoing transitions with an element from $P$ as the label. Also by the construction of $\mathcal{A}_{w}$, we obtain that there is some $u^{\prime}\in\mathscr{W}(u,s,C,D)$ with a run in $\mathcal{T}\circ w\times R$ from the transition in $\mathcal{A}_{w}$. By induction, we also obtain that there is some $\bm{q}^{\prime}\in Q^{*}$ with $\bm{q}^{\prime}\approx\bm{q}$ and a run in $\mathcal{T}\circ w\times R$, which concludes our proof because we have $\mathscr{W}(v,\varepsilon,E,E)=\{v\}$. ∎

4.2 $\omega$-Regular

Theorem 4.6.

For a regular language $R\subseteq Q^{*}$, the language

$$\{\alpha\in\Sigma^{\omega}\mid|R\circ\alpha|=\infty\}$$

is recognized by a deterministic Büchi acceptor. Furthermore, this acceptor can be computed from $\mathcal{T}$, $R$ and $S$.

Proof.

Using Definition 4.3 and Proposition 4.5, we can compute an NFRA $\mathcal{A}_{w}$ recognizing $\mathcal{E}_{w}$ with at most $(K+1)N(|S|N+1)$ states where $N$ is the number of classes of $R$ from $\mathcal{T}\circ w$. We will use these NFRAs for the states of the deterministic Büchi acceptor we need to compute.

We start with $\mathcal{A}_{\varepsilon}$ as the initial state. As long as a state $\mathcal{A}_{w}$ has no outgoing transitions, we compute $\mathcal{A}_{wa}$ from $\mathcal{T}\circ wa$ for all $a\in\Sigma$. We can have two situations: either $\mathcal{A}_{wa}$ does not appear as a state yet (then we add it) or we have $\mathcal{A}_{wa}=\mathcal{A}_{w^{\prime}}$ for some previously added state $\mathcal{A}_{w^{\prime}}$ (where the equality is to be understood with respect to abstract edge-labeled graphs with a marked initial state and a binary (acceptance) relation over the nodes). In both cases, we add the transition and we mark it as accepting if we have $|R\circ w|<|R\circ wa|$. The process of adding new states and transitions has to terminate because there are only finitely many possible NFRAs $\mathcal{A}_{w}$.

From this construction and Proposition 3.7, we obtain that, if we read a word $w$ starting in the initial state, then we end in a state $\mathcal{A}_{w^{\prime}}$ recognizing $\mathcal{E}_{w}$. Together with Proposition 3.6, this insures that, if we use an accepting transition , the $R$-orbit of $w$ is (strictly) smaller than the $R$-orbit of $wa$. Thus, the recognized $\omega$-language of the Büchi acceptor consists exactly of the $\omega$-words with an infinite $R$-orbit. ∎

Remark 4.7.

Using a straight-forward guess and check approach, one can see that the isomorphism problem for NFRAs

Input:	NFRAs $\mathcal{A}_{1}=(Z_{1},\Gamma,\tau_{1},z_{0,1},\mathcal{F}_{1})$ and $\mathcal{A}_{2}=(Z_{2},\Gamma,\tau_{2},z_{0,2},\mathcal{F}_{2})$
Question:	is $\mathscr{R}(\mathcal{A}_{1})=\mathscr{R}(\mathcal{A}_{2})$?

is certainly in PSpace (see e. g. [25] or [30] for more information on complexity theory). Therefore, instead of adding a transition to the Büchi acceptor in the proof of Theorem 4.6, we can instead check whether we already have a state $\mathcal{A}_{w^{\prime}}$ that accepts $\mathcal{E}_{wa}$ and add a transition . This yields a potentially smaller acceptor.

For a finite word $v\in\Sigma^{+}$, we write $v^{\omega}=vv\dots$ for the $\omega$-word arising from $v$ by concatenating it with itself infinitely often. An $\omega$-word is ultimately periodic if it is of the form $uv^{\omega}$ for $u\in\Sigma^{*}$ and $v\in\Sigma^{+}$. Any non-empty $\omega$-regular language contains an ultimately periodic word (see e. g. [26]). We immediately obtain from Theorem 4.6 the following specialization of [8, Corollary 3.3] for automaton semigroups of bounded $S$-activity. [8, Corollary 3.3] states that a general automaton semigroup is infinite if and only if it admits a(n infinite) word with an infinite orbit.

Corollary 4.8.

The semigroup $\mathscr{S}(\mathcal{T})$ generated by the automaton $\mathcal{T}=(Q,\Sigma,\delta)$ of bounded $S$-activity is infinite if and only if there are $u\in\Sigma^{*}$ and $v\in\Sigma^{+}$ with $Q^{*}\circ uv^{\omega}$ (i. e. if it admits an ultimately periodic word with an infinite orbit).

4.3 The Finiteness Problem for Bounded Automaton Semigroups

Theorem 4.9.

The problem

Input:	a complete $\mathscr{S}$-automaton $\mathcal{T}=(Q,\Sigma,\delta)$, a regular, suffix-closed language $R\subseteq Q^{*}$ and a closed subset $S\subseteq Q$ such that $S$ generates a finite subsemigroup and $\mathcal{T}$ is of bounded $S$-activity
Question:	is the image of $R$ in $\mathscr{S}(\mathcal{T})$ finite?

is decidable.

Proof.

Since $R$ is suffix-closed, the subset of $\mathscr{S}(\mathcal{T})$ induced by projecting $R$ into the semigroup is infinite if and only if there is an $\omega$-word with an infinite $R$-orbit [8, Theorem 3.2]. Thus, the stated decision problem is equivalent to testing whether such an $\omega$-word exists. Since the language of such words is effectively deterministic $\omega$-regular by Theorem 4.6, this problem is decidable (as the emptiness problem for (deterministic) Büchi acceptors is decidable, see e. g. [26, Proposition 10.11]). ∎

An immediate consequence of this result is that the finiteness problem for complete automaton semigroups of bounded $S$-activity is decidable.

Corollary 4.10.

The finiteness problem for $\mathscr{S}$-automata of bounded activity

Input:	a complete $\mathscr{S}$-automaton $\mathcal{T}=(Q,\Sigma,\delta)$ and a closed subset $S\subseteq Q$ such that $S$ generates a finite subsemigroup and $\mathcal{T}$ is of bounded $S$-activity
Question:	is $\mathscr{S}(\mathcal{T})$ finite?

is decidable.

Additionally, we also get that the finiteness problem for finitely generated subsemigroups of complete automaton semigroups of bounded $S$-activity is decidable. This in particular includes the (uniform) order problem for complete automaton semigroups of bounded $S$-activity (compare to [1]).

Corollary 4.11.

The subsemigroup finiteness problem for $\mathscr{S}$-automata of bounded activity

Input:	a complete $\mathscr{S}$-automaton $\mathcal{T}=(Q,\Sigma,\delta)$, a finite set $\bm{R}\subseteq Q^{*}$ and a closed subset $S\subseteq Q$ such that $S$ generates a finite subsemigroup and $\mathcal{T}$ is of bounded $S$-activity
Question:	is the subsemigroup of $\mathscr{S}(\mathcal{T})$ generated by $\bm{R}$ finite?

is decidable.

We also obtain some algorithmic consequences for the semigroup generated by the dual automaton. The dual of the complete $\mathscr{S}$-automaton $\mathcal{T}=(Q,\Sigma,\delta)$ is the complete $\mathscr{S}$-automaton $\partial\mathcal{T}=(\Sigma,Q,\partial\delta)$ with

$$\partial\delta=\{\leavevmode\hbox to16.24pt{\vbox to9.35pt{\pgfpicture\makeatletter\hbox{\hskip 2.64294pt\lower-2.15277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.64294pt}{-2.15277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$a$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.30896pt}{-2.15277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$b$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{5.97595pt}{0.0pt}\pgfsys@lineto{10.5759pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{1.376pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.44518pt}{1.95pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$p/q$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mid\leavevmode\hbox to16.52pt{\vbox to11.3pt{\pgfpicture\makeatletter\hbox{\hskip 2.51563pt\lower-3.12498pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.51563pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$p$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.18164pt}{-1.18056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$q$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{5.84863pt}{0.97221pt}\pgfsys@lineto{10.44858pt}{0.97221pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{1.24869pt}{0.97221pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.47568pt}{2.92221pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize$a/b$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\in\delta\}\text{.} a b p/q p q a/b a b p/q p q a/b$$

Concerning the dual, we have the following results regarding the existence of elements with (or without) torsion.

Corollary 4.12.

The problems

Input:	a complete $\mathscr{S}$-automaton $\mathcal{T}=(Q,\Sigma,\delta)$ and a closed subset $S\subseteq Q$ such that $S$ generates a finite subsemigroup and $\mathcal{T}$ is of bounded $S$-activity
Question:	does $\mathscr{S}(\partial\mathcal{T})$ contain an element without torsion?

and

Input:	a complete $\mathscr{S}$-automaton $\mathcal{T}=(Q,\Sigma,\delta)$ and a closed subset $S\subseteq Q$ such that $S$ generates a finite subsemigroup and $\mathcal{T}$ is of bounded $S$-activity
Question:	is $\mathscr{S}(\partial\mathcal{T})$ torsion-free?

are decidable.

Proof.

[8, Theorem 3.12] yields that $\mathscr{S}(\partial\mathcal{T})$ contains an element of torsion if and only if there is a periodic word $u^{\omega}$ (with $u\in\Sigma^{+}$) whose orbit $Q^{*}\circ u^{\omega}$ is finite. Similarly, it also yields that $\mathscr{S}(\partial\mathcal{T})$ contains an element without torsion if and only if $Q^{*}\circ u^{\omega}$ is infinite for some $u\in\Sigma^{+}$. Therefore, the two stated problems boil down to testing whether an $\omega$-regular language (or its complement, which is also $\omega$-regular [26]) contain a periodic word. This, however, is decidable. ∎