Saturation Problems for Families of Automata

The paper is structured as follows. We continue the introduction with a discussion of related work. In Section 2 we introduce the main definitions. In Section 3 we present the polynomial time saturation algorithms (Section 3.1), the learning algorithms (Section 3.2), and the PSPACE-completeness of almost saturation (Section 3.3). The regularity problem is shown to be PSPACE-complete in Section 4, and the exponential lower bounds for transformations between the models are presented in Section 5. We conclude in Section 6.

The problem of saturation was first raised in the conclusion of [13] for the $L_{\$}$ representation of ultimately periodic words: “How can we decide efficiently that a rational language $K\subseteq A^{\ast }\$A^{+}$ is saturated by $\stackrel{\text{UP}}{\equiv }$?” Here, two words $u\$v$ and $u^{\prime }\$v^{\prime }$ are in relation $\stackrel{\text{UP}}{\equiv }$ if $u{v}^{\omega }=u^{\prime }{(v^{\prime })}^{\omega }$. A variation of the problem appears in [12] in terms of so called period languages: For an $\omega$-language $L$, a finite word $v$ is called a period of $L$ if there is an ultimately periodic word of the form $u{v}^{\omega }$ in $L$, and $\mathrm{𝗉𝖾𝗋}(L)$ denotes the set of all these periods of $L$. So $\mathrm{𝗉𝖾𝗋}(L)$ is obtained from $L_{\$}$ by removing the prefixes up to (and including) the $\$$. It is shown that a language $K$ of finite words is a period language iff $K$ is closed under the operations of power, root, and conjugation, where $\mathrm{𝗉𝗈𝗐}(K)=\{v^k\mid v\in K,k\ge 1\}$, $\mathrm{𝗋𝗈𝗈𝗍}(K)=\{v\mid \exists k>0:v^k\in L\}$, and $\mathrm{𝖼𝗈𝗇𝗃}(K)=\{v_2{v}_1\mid v_1{v}_2\in K\}$. Our notion of power-stable corresponds to closure under $\mathrm{𝗋𝗈𝗈𝗍}$ and $\mathrm{𝗉𝗈𝗐}$, and our notion of loopshift-stable corresponds to closure under conjugation. Given any $K\subseteq {\mathrm{\Sigma }}^{\ast }$, the least period language containing $K$ is $\mathrm{𝗉𝖾𝗋}(L)=\mathrm{𝗋𝗈𝗈𝗍}(\mathrm{𝗉𝗈𝗐}(\mathrm{𝖼𝗈𝗇𝗃}(K)))$. Then [12] poses three decision problems for a given regular language $K\subseteq {\mathrm{\Sigma }}^{\ast }$: (1) Is $K$ a period language? (2) Is $\mathrm{𝗉𝖾𝗋}(K)$ regular? (3) Is $\mathrm{𝗉𝗈𝗐}(K)$ regular?

Problem (1) is a variation of the saturation problem for FDFAs that focuses solely on periods, independent of their prefixes. It is observed in [12] that Problem (1) is decidable without considering the complexity. Similarly, Problem (2) is a variation of the regularity problem that we study for FDFAs, again considering only periods independent of their prefixes. It is left open in [12] whether Problem (2) is decidable, but a reduction to Problem (3) is given. Notably, this reduction is exponential since it constructs a DFA for $\mathrm{𝗋𝗈𝗈𝗍}(\mathrm{𝖼𝗈𝗇𝗃}(K))$. Later, Problem (3) was shown to be decidable in [18] without an analysis of the complexity. Our results in Section 4 give a direct proof that Problem (2) is PSPACE-complete.

The paper [7] defines cyclic languages as those that are closed under the operations of power, root, and conjugation, and gives a characterization of regular cyclic languages in terms of so called strongly cyclic languages. So the cyclic languages are precisely the period languages of [12]. Decidability questions are not studied in [7].

In [16], lasso automata are considered, which are automata accepting pairs of finite words. The representation basically corresponds to the $u\$v$ representation of [13] but without an explicit $\$$ symbol, using different transition relations instead. It is easy to see that lasso automata and automata for the $u\$v$ representation are equivalent up to minor rewriting of the automata. The property of full saturation corresponds to the notion of bisimulation invariance in [16]: two lassos $(u,v)$ and $(u^{\prime },v^{\prime })$ are called bisimilar if $u{v}^{\omega }=u^{\prime }{(v^{\prime })}^{\omega }$, and a lasso automaton is bisimulation invariant if it accepts all pairs from a bisimulation class or none. Bisimulation invariance is characterized in [16] by the properties circular (power-stable in our terminology) and coherent (loopshift-stable in our terminology), [15, Theorem 2], [16, Section 3.3]. An $\mathrm{\Omega }$-automaton is defined as a circular and coherent lasso automaton, which corresponds to the property of full saturation for FDFAs. This property of a lasso automaton is shown to be decidable in [16, Theorem 18] without considering the complexity (since the decision procedure builds the monoid from a DFA, it is at least exponential). Another decision procedure is given in [14, Proposition 12] with a doubly exponential upper bound.

Finally, the saturation problem for FDFAs is explicitly considered in [2, Theorem 4.7], where it is shown to be in PSPACE by giving an upper bound (exponential in the size of the FDFA) on the size of shortest pairs violating saturation if the given FDFA is not saturated.

There are some active and some passive learning algorithms for different representations of regular $\omega$-languages, but all of them are either for subclasses of the regular $\omega$-languages, or they are not polynomial time (for active learners) or not polynomial in the required data (for passive learners), where the complexity for learning a class $𝒞$ of representations is measured in a smallest representation of the target language from $𝒞$. The only known polynomial time active learner for regular $\omega$-languages in the minimally adequate teacher model of [1] is for deterministic weak Büchi automata [28]. There are active learners for nondeterministic Büchi automata (NBA) [17, 24] and for deterministic Büchi and co-Büchi automata [26], but these are heuristics for the construction of NBA that are not polynomial in the target representations. The algorithm from [17] uses an active learner for DFAs for learning the $u\$v$ representation of [13] for regular $\omega$-languages. Whenever the DFA learner asks an equivalence query, the DFA is turned into an NBA, and from a counter-example for the NBA a counter example for the DFA is derived. Our active learner uses the same principle but turns the DFA for the $u\$v$ representation into an FDFA and checks whether it is fully saturated.

There is a polynomial time active learner for deterministic parity automata [30], but this algorithm uses in addition to membership and equivalence queries so-called loop-index queries that provide some information on the target automaton, not just the target language. So this algorithm does not fit into the minimally adquate teacher model from [1]. The paper [3] presents a learning algorithm for FDFAs. But it turns out that this is not a learning algorithm for regular $\omega$-languages: The authors make the assumption that the FDFAs used in equivalence queries define regular $\omega$-languages (beginning of Section 4 in [3]) while they only provide such a semantics for saturated FDFAs. So their algorithm requires an oracle that returns concrete representations of ultimately periodic words as counter-examples for arbitrary FDFAs, which is not an oracle for regular $\omega$-languages. Our algorithms solve this problem by first using the polynomial time saturation check, making sure that we only submit saturated FDFAs to the equivalence oracle.

Concerning passive learners, the only polynomial time algorithms that can learn regular $\omega$-languages in the limit from polynomial data are for subclasses that make restrictions on the canonical Myhill/Nerode right-congruence of the potential target languages. The algorithm from [4] can only learn languages for which the minimal automaton has only one state per Myhill/Nerode equivalence class (referred to as IRC languages for “informative right congruence”). The algorithm from [8] can also learn languages beyond that class but there is no characterization of the class of languages that can be inferred beyond the IRC languages. The algorithm in [9] infers deterministic Büchi automata (DBA) in polynomial time but the upper bound on the size of characteristic samples for a DBA-recognizable language $L$ is exponential in a smallest DBA for $L$, in general. The algorithm in [10] generalizes this to deterministic parity automata (DPA) and can infer a DPA for each regular $\omega$-language, but a polynomial bound for the size of characteristic samples is only given for languages accepted by a DPA that has at most $k$ states per Myhill/Nerode class for a fixed $k$.

The paper [19] considers a model of FDFA with so-called duo-normalized acceptance and mentions connections to the model FWPM from [10] in a few places, without going into details of the connection. Using results from [10], it is not very hard to show that the models can be considered the same in the sense that they can be easily converted into each other without changing the transition structure. We give a proof of this in the full version of the paper.

${ℱ}^{\prime }$ can nondeterministically guess, for $(u,v)$, the shift $(u{v}_1,v_2{v}_1)$; $𝒯(u{v}_1)$; and the state $p$ the accepting run of $N_{𝒯(u{v}_1)}$ on $v_2{v}_1$ is in after reading $v_2$, and use its nondeterministic power to validate the guess. $◀$

We now state the main theorems of this section.

To show hardness, it is enough to show hardness for (2), as hardness for (3) then follows from Section 4, and both (2) and (3) are special cases of (1) and (4). We show hardness of (2) in Theorem 10.

Most of this section is dedicated to establish a decision procedure (which is in PSPACE) for (3). This is done in Lemmas 4 through 4. Using Section 4 reduces (4) to (3), and (2) is a special case of (4). Case (1) can be reduced to case (3) by considering a labeling of the words with the states of the leading TS. $◀$

For the PSPACE upper bound, as justified by the reduction to (3) of Theorem 9, we focus on a loopshift-stable FNFA $ℱ=(𝒯,𝒩)$ with trivial $𝒯$. So there is only one progress NFA $𝒩=(\mathrm{\Sigma },Q,\delta ,\iota ,F)$, which accepts some language $P=L_{\ast }(𝒩)$ satisfying $uv\in P\iff vu\in P$ as $ℱ$ is loopshift-stable. Since $𝒯$ is trivial, the UP-language $L$ of $ℱ$ is prefix-independent and is of the form $L=\{u\cdot v^{\omega }\mid (u,v)\in {𝖫}_{\mathrm{𝗇𝗈𝗋𝗆}}(ℱ)\}={\mathrm{\Sigma }}^{\ast }\cdot \omega -\mathrm{𝖯𝗈𝗐}(P)$ (recall that $\omega -\mathrm{𝖯𝗈𝗐}(P)=\{v^{\omega }:v\in P\}$). Our goal is to decide whether $L$ is UP-regular.

As the semantics is existential, it can happen that some representations of a word $v^{\omega }\in \omega -\mathrm{𝖯𝗈𝗐}(P)$ are not in $P$. This makes the problem non-trivial even in the prefix-independent case as witnessed by the language $P=\{a^{i}b{a}^j\mid i+j\ge 1\}$, which consists of all words with exactly one $b$ and at least one $a$ over the alphabet $\mathrm{\Sigma }=\{a,b\}$. Clearly, $P$ is regular, but $L={\mathrm{\Sigma }}^{\ast }\cdot \{{\left(a^{i}b{a}^j\right)}^{\omega }\mid i+j\ge 1\}$ is not UP-regular.

We now define a congruence relation ${\approx }_P$: for $x,y\in {\mathrm{\Sigma }}^{\ast }$,

As $L={\mathrm{\Sigma }}^{\ast }\cdot \omega -\mathrm{𝖯𝗈𝗐}(P)$ is prefix-independent, ${\approx }_P$ is the syntactic congruence of $L$ defined in [5], and also corresponds to the definition of the progress congruence of the syntactic FORC [29] and to the periodic progress congruence from [3] (where the latter two are only defined for regular $\omega$-languages). It follows from results in [13, 2] that $L$ is UP-regular if, and only if, ${\approx }_P$ has finite index.

By Section 4, to determine whether or not the UP-language of $ℱ$ is UP-regular, we only need to check whether ${\approx }_P$ has finite index. To this end, we introduce the transition profile of a finite word $x\in {\mathrm{\Sigma }}^{+}$, which captures the behavior of $x$ in a TS or automaton, in this case the progress NFA $𝒩$. Formally, $\tau$ is given as a mapping $\tau :Q\to Q$ if $𝒩$ is deterministic and $\tau :Q\to 2^Q$ if it is nondeterministic, with $q\mapsto {\delta }^{\ast }(q,x)$, and we write ${\tau }_{𝒩}$ for the function that assigns to a finite word its transition profile in $𝒩$. There are at most ${|Q|}^{|Q|}$ and $2^{{|Q|}^2}$ different mappings for deterministic and nondeterministic automata, respectively. We now refine ${\approx }_P$ using the transition profile by introducing

Clearly, ${\approx }_P$ has finite index if, and only if, ${\approx }_{𝒩}$ has finite index.

Transition profiles are useful, because they offer sufficient criteria for a word $x$ to be in the power language: we can directly check from ${\tau }_{𝒩}(x)$ whether or not there is some power $j>0$ such that $x^j\in P$. This, of course, entails $x^{\omega }\in \omega -\mathrm{𝖯𝗈𝗐}(P)$. We call such transition profiles accepting and transition profiles, where no power of $x$ is accepted, rejecting. Note that ${\tau }_{𝒩}(x)$ is called accepting if some power of $x$ is accepted, not necessarily $x$ itself. Correspondingly, ${\tau }_{𝒩}(x)$ is rejecting if all powers of $x$ are rejected.

Note that there can be words $x$ such that $x^{\omega }\in \omega -\mathrm{𝖯𝗈𝗐}(P)$ but no power of $x$ is in $P$. For instance, let $P=\{b^{i}a{b}^j:i+j\ge 0\}$ be a loopshift-stable regular language: clearly ${(ab\cdot ab)}^{\omega }\in \omega -\mathrm{𝖯𝗈𝗐}(P)$ but ${(ab\cdot ab)}^i\notin P$ for all $i>0$.

Recall that the root $\sqrt{x}$ is the shortest word $u$ such that $u^{\omega }=x^{\omega }$. To get a feeling for the properties of transition profiles, for a word $x$ with $x=\sqrt{x}$, $x^{\omega }\in \omega -\mathrm{𝖯𝗈𝗐}(P)$ can only hold if some power of $x$ is in $P$, which we can read from ${\tau }_{𝒩}(x)$.

We call a transition profile $\tau$ terminal if it is accepting, but ${\tau }^i$ is rejecting for some power $i$. (Note that ${\tau }_{𝒩}(x^i)$ is the function obtained from iterating ${\tau }_{𝒩}(x)$ $i$ times. However, we can take the power of a transition profile directly without knowing $x$, and even for transition profiles that do not correspond to a word.)

We call a word $x$ such that ${\tau }_{𝒩}(x)$ is terminal, a terminal word and write $𝖳𝖾𝗋(P)$ for the set of terminal words in $P$. So $x$ is a terminal word if some power $x^j$ is in $P$, and there is $i>1$ such that $x^{ik}\notin P$ for all $k\ge 1$. Note that if $x$ is a terminal word, then so is $\sqrt{x}$. The following lemma expresses finite index of ${\approx }_P$ in terms of a property of $𝖳𝖾𝗋(P)$ that we use in our decision procedure.

We show that, if there are infinitely many roots in $𝖳𝖾𝗋(P)$, then we can construct from them an arbitrary number of words that are distinguished by ${\approx }_P$; ${\approx }_P$ therefore has infinite index.

Conversely, if there are finitely many roots $r_1,\mathrm{\dots },r_n$ in $𝖳𝖾𝗋(P)$, then two words $x,y$ are identified equivalent by ${\approx }_P$ if they define the same transition profile ${\tau }_{𝒩}(x)={\tau }_{𝒩}(y)$ and for all $z\in {\mathrm{\Sigma }}^{\ast }$ ${\tau }_{𝒩}(xz)$ is accepting or there is a root $r_i\in 𝖳𝖾𝗋(P)$ such that ${(xz)}^{\omega }=r_i^{\omega }$ iff there is a root $r_j\in 𝖳𝖾𝗋(P)$ such that ${(yz)}^{\omega }=r_j^{\omega }$ where $1\le i,j\le n$.

These are all regular properties, and ${\approx }_P$ is therefore finite. $◀$

We now show that infinitely many roots of $𝖳𝖾𝗋(P)$ are witnessed by transition profiles with specific properties, called good witnesses, as defined below.

We say that a word $x$ visits ${\tau }_g$ first if (a) ${\tau }_{𝒩}(x)={\tau }_g$ holds and (b) no true prefix $y$ of $x$ satisfies ${\tau }_{𝒩}(y)={\tau }_g$. If there is a word $x$ that visits ${\tau }_g$ first, we say that $u$ recurs to ${\tau }_g$ if $u\ne \epsilon$ and (a) ${\tau }_{𝒩}(xu)={\tau }_g$ holds and (b) no true non-empty prefix $v$ of $u$ satisfies ${\tau }_{𝒩}(xv)={\tau }_g$.

We say that ${\tau }_g$ is a good witness if it is terminal and one of the following holds:

1. 1.

   there are infinitely many words $x$ that visit ${\tau }_g$ first, or

2. 2.

   there is a word $x$ that visits ${\tau }_g$ first and a word $u$ that recurs on ${\tau }_g$ that have different roots.

If $𝖳𝖾𝗋(P)$ has infinitely many roots, then infinitely many of them refer to one witness. We show that they cannot all be constructed from one word $x$ that visits ${\tau }_g$ first and one word $u$ that recurs on ${\tau }_g$ and has the same root as ${\tau }_g$, so that one of the two cases must hold.

Reversely, if ${\tau }_g$ is a good witness we distinguish case (1), where we argue that the infinitely many words that visit ${\tau }_g$ first must have different roots (and roots of terminal words are terminal). For the other case, we build infinitely many roots with the terminal transition profile ${\tau }_g$ from a word $x$ that visits ${\tau }_g$ first and a word $u$ that recurs on ${\tau }_g$ and has a different root than $x$. $◀$

Checking if there is a good witness can be done on the succinctly defined TS whose state space are the transition profiles that tracks the transition profiles of finite words.

We observe that tracing the transition profiles is done by a TS ${𝒯}^{\prime }$ of size exponential in $𝒩$, but succinctly represented by $𝒩$ (and in ${\tau }_g$ for checking that ${\tau }_g$ is terminal). Checking the conditions of a good transition profile are a number of reachability problems in this transition profile, and all of them are in NL the size of ${𝒯}^{\prime }$. $◀$

This finishes the proof for the PSPACE upper bound. We now show the lower bound for case (2) of Theorem 9.

Assume that we are given $p$ DFAs ${𝒟}_1,{𝒟}_2,\mathrm{\cdots },{𝒟}_p$ that do not accept the empty word; we assume that $p$ is prime (and otherwise pad) and that $\mathrm{\#}\notin \mathrm{\Sigma }$. We define $L_1={\mathrm{\#}}^{+}{\mathrm{\Sigma }}^{+}{\mathrm{\#}}^{\ast }$, $L_p=L_1^{}{}_{}{}^p$, and $L_{\cap }={\bigcap }_{i=1}^p{L}_{\ast }({𝒟}_i)$. Deciding if $L_{\cap }=\mathrm{\varnothing }$ is the PSPACE-hard problem we reduce from.

We build two DFAs $𝒟$ and ${𝒟}^{\prime }$ using the states of ${𝒟}_1,\mathrm{\dots },{𝒟}_p$ plus $p+1$ extra states. ${𝒟}^{\prime }$ accepts a word $w$ if it is in $L_p$ and of the form $w={\mathrm{\#}}^{+}{w}_1{\mathrm{\#}}^{+}{w}_2\mathrm{\dots }{\mathrm{\#}}^{+}{w}_p{\mathrm{\#}}^{\ast }$ s.t. $w_i\in {\mathrm{\Sigma }}^{+}$ holds for all $i\le p$ and $w_i\notin L_{\ast }({𝒟}_i)$ holds for some $i\le p$. We call its language $L^{\prime }$.

$𝒟$ accepts a word $w$ if $w\in L_p^{}{}_{}{}^{\ast }\cdot L^{\prime }\cdot L_p^{}{}_{}{}^{\ast }$ or $w\in L_1^{}{}_{}{}^i$ and $p$ does not divide $i$.

If $L_{\cap }\ne \mathrm{\varnothing }$, then every word $v\in {\mathrm{\#}}^{+}{L}_{\cap }$ is terminal for $P=L_{\ast }(𝒟)$, because $v^p$ defines a rejecting transition profile. These words are all roots, and the ${\mathrm{\#}}^{+}$ part ensures that there are infinitely many of them.

For the case $L_{\cap }=\mathrm{\varnothing }$ we assume towards a contradiction that $𝖳𝖾𝗋(P)$ contains a root $u$. Then $u\in L_1^{}{}_{}{}^i{\mathrm{\#}}^{\ast }$ for some $i$. If $p$ divides $i$, then either all powers of $u$ are accepted or no power of $u$ is accepted (contradiction). If $p$ does not divide $i$, then $u^j$ is accepted if $p$ divides $j$ (because all $i$ words in ${\mathrm{\Sigma }}^{+}$ are rejected by some ${𝒟}_k$ due to $L_{\cap }=\mathrm{\varnothing }$), and $u^j$ is accepted if $p$ does not divide $j$, because then $p$ does not divide $ij$ and $u^j\in L_1^{}{}_{}{}^{ij}$ (contradiction).

For showing the second part of the theorem, we use the DFA $𝒟$ as progress automaton for an FDFA with trivial leading TS, and then use Section 4 and Section 4. These lemmas require the language that is accepted to be loopshift-stable. While $𝒟$ does not recognize a loopshift-stable regular language $P$, it is not hard to see that the loopshift-stable language $P^{\prime }=\{xy\mid x,y\in {(\mathrm{\Sigma }\cup \{\mathrm{\#}\})}^{\ast },yx\in P\}$ we obtain by the construction from Section 4 also satisfies that $𝖳𝖾𝗋(P^{\prime })=\mathrm{\varnothing }$ if $L_{\cap }=\mathrm{\varnothing }$. Since $𝖳𝖾𝗋(P)\subseteq 𝖳𝖾𝗋(P^{\prime })$, we also get that $𝖳𝖾𝗋(P^{\prime })$ contains infinitely many roots if $L_{\cap }\ne \mathrm{\varnothing }$. Furthermore $P^{\prime }$ and $P$ define the same UP-language, and thus deciding if this UP-language is UP-regular is the same as deciding if $𝖳𝖾𝗋(P)$ has finitely many roots. $◀$

We represent mappings $\{1,\mathrm{\dots },n\}\to \{1,\mathrm{\dots },n\}$ as words over an alphabet of constant size. The language $L_n$ contains a word $w$ if it has infinitely many infixes $\mathrm{\#}u\mathrm{\#}$ such that $1$ is a fixpoint of the mapping represented by $u$. A saturated FDWA can wait for an occurrence of $\mathrm{\#}$ and then keep track of the number that $1$ is mapped to, which is possible with $n+2$ states. As the progress automaton of this FDWA has only a single accepting state which is a sink, it is almost saturated when viewed as FDFA. By Lemma 2, a saturated FDFA must be loopshift-stable, and therefore cannot wait for an occurrence of $\mathrm{\#}$ before following a single number. Thus, it has to memorize the full mapping encoded by the word read so far, for which it needs at least $n^n$ states. $◀$

The size of an almost saturated FDFA is, in general, incomparable to the size of a saturated FDWA, and there may be an exponential blowup in either direction, which the following lemma formalizes.

The alphabet of $L_n$ consists of non-empty subsets of $\{1,\mathrm{\dots },2n\}$. A word is in $L_n$ if some number $i$ is member of only finitely many symbols, meaning $L_n$ is prefix-independent. Due to its limit behavior, a saturated FDWA can test on the loop for an occurrence of each number in sequence, leading to a progress automaton with $2n+1$ states. But one can show that for all $X,Y\subseteq \{1,\mathrm{\dots },2n\}$ with $X\ne Y$ and $|X|=|Y|=n$, either $X$ and $Y$, or their complements must lead to different states from the initial state of the progress automaton of any almost saturated FDFA for $L_n$.

The language $L_n^{\prime }$ is defined over the alphabet $\{0,1\}$, and contains all words with infinitely many infixes $0u0$ such that $|u|=n-1$, which is clearly prefix-independent. When using a trivial leading TS, an FDWA or almost saturated FDFA can simply guess the start of an infix $0u0$ and verify that $|u|=n-1$, which can be done with $n+3$ states. This is not possible in a saturated FDWA since it has to be invariant under loopshifts. Similarly, in the progress automaton of any almost saturated FDFA for the complement of $L_n^{\prime }$, distinct words of length $n$ must lead to different states. $◀$

The following bounds were already known in the literature (c.f. [22, Section 5] and [3, Theorem 2]). We include them for the purpose of completeness, and provide families of languages achieving them in a systematic way.

We consider words of the form $u_1\mathrm{\#}{u}_2\mathrm{\#}\mathrm{\dots }$ where each $u_i$ encodes a mapping $m_{u_i}$ from $\{1,\mathrm{\dots },n\}$ to itself, akin to Section 5. Such a word is in $L_n$ if infinitely many $u_i$ represent a mapping such that $1$ is a fixpoint. A small saturated FDFA $(𝒯,𝒟)$ tracks in its leading TS $𝒯$ the number that $1$ is sent to under the mapping encoded by the word read since the last $\mathrm{\#}$. This leads to $n$ progress DFAs of size $2n$ each, and ${𝒟}_i$ accepts words of the form $x\mathrm{\#}y$ where $m_x$ maps $i$ to $1$ and $m_y$ maps $1$ to $i$. The syntactic FDFA on the other hand has a trivial leading TS and in its progress DFA, any words encoding distinct mappings have to lead to different states. For the second claim, we slightly modify $L_n$ to force the leading TS of the syntactic FDFA to be roughly of the shape of $𝒯$, which means the each progress DFA is of linear size. A fully saturated FDFA for $L^{\prime }$, however, cannot simply ignore words if they do not loop on a state of the leading TS, which forces it to track all $n^n$ mappings. $◀$