A Pumping-Like Lemma for Languages
over Infinite Alphabets

Finite-memory automata [18, 19] generalize classical Rabin-Scott finite-state automata [29] to infinite alphabets. By equipping the automata with a finite set of registers (called in [18, 19] windows), which store letters from the infinite alphabet during computation, and restricting the power of the automaton to comparing the input letters with register contents and copying input letters to registers, the automaton retains a fixed finite-memory of input letters. Consequently, the languages accepted by finite-memory automata possess properties similar to regular languages and are, thus, termed quasi-regular languages.

An important facet of finite-memory automata is a certain indistinguishability view of the infinite alphabet embedded in the modus operandi of the automaton. The language accepted by an automaton is invariant under permutations of the infinite alphabet. Thus, the actual symbols occurring in the input are of no real significance. Only the initial and repetition patterns matter.

Automata over infinite alphabets have gained increasing importance in computer science as they provide formal models for analyzing systems that operate over unbounded data domains. Such models are essential for specifying and verifying properties of XML documents, database queries, and programs with variables over infinite domains. The ability to reason about infinite alphabets while maintaining decidability of key properties makes these models particularly valuable for the formal verification of data-aware systems.

Over the years, many models of automata over infinite alphabets have been proposed (see surveys in [32, 20, 6]), though most of these models are incomparable. In the absence of a definitive model for managing infinite alphabets, evaluating a formalism requires consideration of its desirable properties, including: expressive power, closure and regular properties, decidability and complexity of classical problems, and applicability of the model.

Finite-memory automata provide a structured way to reason about such systems by focusing on patterns and repetitions of data values rather than their specific identities. This perspective is particularly useful in applications where the exact values of data are less important than their relative behavior over time. Note that quasi-regular languages are a particular case of nominal sets (also known as sets with atoms or Fraenkel-Mostowski sets) [3], and finite-memory automata themselves are expressively equivalent to nominal automata (also known as orbit-finite automata) [4].

However, the non-emptiness problem for finite-memory automata is NP-complete [30] and the universality problem is undecidable for automata with two (or more) registers [27].

Nevertheless, when restricted to a single register, the emptiness problem is decidable for the alternating variant of finite-memory automata [9, 12, 15], albeit with non-primitive recursive complexity [9]. Since alternation extends the power of nondeterministic automata by introducing existential and universal states, effectively allowing the automaton to explore multiple computation paths in parallel [5], the universality and containment problems are decidable for these automata as well.

The restriction of finite-memory automata to a single register (while still allowing a finite set of constant symbols) is of significance: it preserves a Parikh-like theorem [17], the existence of a deterministic equivalent automaton is decidable [7], and, for ordered alphabets, the intersection of nondeterministic and co-nondeterministic one-register languages lies within the deterministic class [23].

This paper deals with alternating finite-memory automata with one register. Such automata are tightly related to the linear and branching temporal logics with the freeze quantifier. In particular, the satisfiability problem for formulas in linear temporal logic with forward operators and one freeze quantifier is decidable, see [9]. In addition, these models are particularly robust and possess many regular properties, being closed under Boolean operations and subsuming various other automata models, such as top-view pebble automata and weak two-pebble automata [33]. Recently, it was shown in [8] that the boundness problem for these models is also decidable, by proving an extension lemma for sufficiently long words. Also, there is a strong connection to alternating timed automata with one clock, such that complexity and decidability results transfer back and forth between these models [12].

A fundamental property of classical finite-state automata is their regularity, which is often characterized using the pumping lemma. The pumping lemma serves as a crucial tool for proving that certain languages are not regular by identifying structural constraints on words within the language.

For general many-register finite-memory automata, it is well known that the classical pumping lemma does not necessarily hold, see [19, Example 3]. Therefore, in any suitable pumping lemma for languages over infinite alphabets, the pumped paterns are not, necesseryly, identical, but, insteasd, are equivalent modulo some permutation of the infinite alphabet. A pumping lemma of this kind has been proven for finite-memory automata in [26], though it does not involve the action of permutations on repeated subwords and only establishes the existence of such pumped patterns.

The main result of this paper is a kind of pumping lemma for languages accepted by one-register alternating finite-memory automata. As a corollary, we obtain that the set of lengths of words in such languages is semi-linear.

This paper is organized as follows. In the next section, we recall the definition of finite-memory automata from [19] and, in Section 3, we prove a pumping lemma for these automata. Sections 4 and 5, respectively, contain the definition of alternating finite-memory automata and the statement of the pumping lemma for theses automata, that is the main result of our paper. In Section 6, we present some applications of the pumping lemma, including the semi-linearity result. Due to space constraints, the full proof of the pumping lemma is omitted and can be found in the full version of this article. We provide the proof overview and the main methods in Section 7. Finally, Section 8 contains some remarks concerning the complexity of computing the pumping lemma parameter and possible extensions for ordered alphabets and timed automata.

Throughout this paper, we employ the following conventions.

• $\mathrm{■}$

  $\mathrm{\Sigma }$ is a fixed infinite alphabet.

• $\mathrm{■}$

  Symbols in $\mathrm{\Sigma }$ are denoted by $\sigma$, $\theta$, etc., sometimes indexed or primed.

• $\mathrm{■}$

  Bold low-case Greek letters $𝝈$, $𝜽$, etc., also sometimes indexed or primed, denote words over $\mathrm{\Sigma }$.

• $\mathrm{■}$

  Symbols that occur in a word denoted by a boldface letter are always denoted by the same non-boldface letter with an appropriate subscript. For example, the letters that occur in ${𝝈}^{\prime }$ are denoted by ${\sigma }_i^{\prime }$.

• $\mathrm{■}$

  For word $𝝈={\sigma }_1{\sigma }_2\mathrm{\cdots }{\sigma }_n\in {\mathrm{\Sigma }}^{\ast }$, we denote by $[𝝈]$ the set of letters occurring in $𝝈$:

  $$[𝝈]=\{{\sigma }_1,{\sigma }_2,\mathrm{\dots },{\sigma }_n\}$$

  and call this set the contents of $𝝈$.

• $\mathrm{■}$

  For a subset $\mathrm{\Phi }$ of $\mathrm{\Sigma }$ and a positive integer $r$, we denote by ${\mathrm{\Phi }}^{r_{\ne }}$ the subset of ${\mathrm{\Phi }}^r$ whose elements do not contain repeated letters:

  $${\mathrm{\Phi }}^{r_{\ne }}=\{{\sigma }_1\mathrm{\dots }{\sigma }_r\in {\mathrm{\Phi }}^r:\text{for all}i\text{and}j,\text{such that}i\ne j,{\sigma }_i\ne {\sigma }_j\}.$$

• $\mathrm{■}$

  The length of a word $𝝈\in {\mathrm{\Sigma }}^{\ast }$ is denoted by $|𝝈|$ and the cardinality of a finite set $X$ is denoted by $\Vert X\Vert$.

Next, we recall the definition of finite-memory automata from [18, 19] in which a fixed finite number of distinct letters can be stored in the automaton memory during a computation.

A configuration of $𝑨$ is a pair in $S\times {\left(\mathrm{\Sigma }\setminus \mathrm{\Delta }\right)}^{r_{\ne }}$, where the state component of the pair is the current state and the letters’ components are the letters stored in the registers. The configuration $(s_0,{𝜽}_0)$ is the initial configuration, and the configurations with the first component in $F$ are accepting (or final) configurations.

For configurations $(s,𝜽)$ and $(s^{\prime },{𝜽}^{\prime })$, where $𝜽={\theta }_1{\theta }_2\mathrm{\cdots }{\theta }_r$ and ${𝜽}^{\prime }={\theta }_1^{\prime }{\theta }_2^{\prime }\mathrm{\cdots }{\theta }_r^{\prime }$, we write $(s,𝜽)\stackrel{𝜎}{⟶}(s^{\prime },{𝜽}^{\prime })$, if one of the following holds.

• $\mathrm{■}$

  $\sigma \in \mathrm{\Delta }$, $s^{\prime }\in {\mu }_{\mathrm{\Delta }}(s,\sigma )$, and ${𝜽}^{\prime }=𝜽$.

• $\mathrm{■}$

  For some $i=1,2,\mathrm{\dots },r$, $\sigma ={\theta }_i$, $s^{\prime }\in {\mu }_{=}(s,i)$, and ${𝜽}^{\prime }=𝜽$.

• $\mathrm{■}$

  $\sigma \notin \mathrm{\Delta }\cup [𝜽]$ and either $s^{\prime }\in {\mu }_{{\ne }_{\text{skip}}}(s)$, and ${𝜽}^{\prime }=𝜽$, or for some $i=1,2,\mathrm{\dots },r$, $(s^{\prime },i)\in {\mu }_{{\ne }_{\text{replace}}}(s)$, and, for $j=1,2,\mathrm{\dots },r$,

A run of $𝑨$ on a word $𝝈={\sigma }_1{\sigma }_2\mathrm{\cdots }{\sigma }_n$ is a sequence of configurations $c_0,c_1,\mathrm{\dots },c_n$ such that for all $i=1,2,\mathrm{\dots },n$, $c_{i-1}\stackrel{{\sigma }_i}{⟶}{c}_i$. In such a case, we shall also write $c_0\stackrel{𝝈}{⟶}{c}_n$.

A run is accepting, if it starts from the initial configuration $(s_0,{𝜽}_0)$ and ends in a final configuration. A word is accepted by $𝑨$, if there exists an accepting run of $𝑨$ on it. The language of all accepted words is denoted by $L\left(𝑨\right)$.

The pumping lemmas in this paper involve the following definitions.

The proof of Proposition 6 is similar to that of [19, Lemma 1] and is omitted.

It has been shown in [19, Example 3] that the pumping lemma for regular languages [29, Lemma 8] does not hold for the quasi-regular ones. A variant of the pumping lemma for quasi-regular languages was later published in [26], although it had previously been obtained independently by two groups [22].⁴⁴4The author in [22] also posed the question of whether their pumping lemma extends to alternating automata. However, it does not apply directly to this setting; see the discussion in Section 5.1. The pumping lemma presented below refines these results in which

• $\mathrm{■}$

  the pumped patterns are generated by a fixed finite-ordered permutation, and

• $\mathrm{■}$

  an explicit upper bound is given on the order of that permutation.

Even though the classical pumping lemma does not hold for quasi-regular languages, as shows Corollary 8 below, some sufficiently long words in a quasi-regular language possess periodicity properties.

In this section, we recall the definition of alternating finite-memory automata and state some of its basic properties. We restrict ourselves to one-register automata with which we deal in this paper.

Like in the case of (non-alternating) finite-memory automata, a configuration of $𝑨$ is a pair in $S\times (\mathrm{\Sigma }\setminus \mathrm{\Delta })$.

The transition functions ${\mu }_{\mathrm{\Delta }}$, ${\mu }_{=}$, and ${\mu }_{\ne }$ induce the following transition function ${\mu }^{𝒄}$ on a configuration $(s,\theta )$ and an input letter $\sigma$, as follows,

• $\mathrm{■}$

  If $\sigma \in \mathrm{\Delta }$, then ${\mu }^{𝒄}((s,\theta ),\sigma )=\{Q\times \{\theta \}:Q\in {\mu }_{\mathrm{\Delta }}(s,\sigma )\}$.

• $\mathrm{■}$

  If $\sigma =\theta$, then ${\mu }^{𝒄}((s,\theta ),\sigma )=\{Q\times \{\theta \}:Q\in {\mu }_{=}(s)\}$.

• $\mathrm{■}$

  If $\sigma \notin \mathrm{\Delta }\cup \{\theta \}$, then ${\mu }^{𝒄}((s,\theta ),\sigma )=\{Q^{\prime }\times \{\theta \}\cup Q^{\prime \prime }\times \{\sigma \}:(Q^{\prime },Q^{\prime \prime })\in {\mu }_{\ne }(s)\}$.

Next, we extend ${\mu }^{𝒄}$ to finite sets of configurations in the standard “alternating” manner. Let $C=\{c_1,c_2,\mathrm{\dots },c_k\}$ be a set of configurations, $\sigma \in \mathrm{\Sigma }$, and let ${\mu }^{𝒄}(c_i,\sigma )=\{C_{i,1},C_{i,2},\mathrm{\dots },C_{i,m_i}\}$, $i=1,2,\mathrm{\dots },k$. Then ${\mu }^{𝒄}(C,\sigma )$ consists of all finite sets of configurations of the form $\bigcup _{i=1}^k{C}_{i,j_i}$, $j_i=1,2,\mathrm{\dots },m_i$. That is, $C^{\prime }\in {\mu }^{𝒄}(C,\sigma )$, if there is a set of finite sets of configurations $\{C_{1,j_1},C_{2,j_2},\mathrm{\dots },C_{k,j_k}\}$, $C_{i,j_i}\in {\mu }^{𝒄}(c_i,\sigma )$, $i=1,2,\mathrm{\dots },k$, such that $C^{\prime }=\bigcup _{i=1}^k{C}_{i,j_i}$. Like in the case of (non-alternating) finite-memory automata, we write $C\stackrel{𝜎}{⟶}{C}^{\prime }$ for $C^{\prime }\in {\mu }^{𝒄}(C,\sigma )$.

Now, we can define the notion of a run of $𝑨$. Let $𝝈={\sigma }_1{\sigma }_2\mathrm{\cdots }{\sigma }_n\in {\mathrm{\Sigma }}^{\ast }$. A run of $𝑨$ on $𝝈$ is a sequence of finite sets of configurations $C_0,C_1,\mathrm{\dots },C_n$, where

• $\mathrm{■}$

  $C_0=\{(s_0,{\theta }_0)\}$ and

• $\mathrm{■}$

  $C_i\stackrel{{\sigma }_{i+1}}{⟶}{C}_{i+1}$, $i=0,1,\mathrm{\dots },n-1$.

That is $C_0\stackrel{{\sigma }_1}{⟶}{C}_1\stackrel{{\sigma }_2}{⟶}{C}_2\stackrel{{\sigma }_3}{⟶}\mathrm{\cdots }\stackrel{{\sigma }_n}{⟶}{C}_n$ and, like in the case of (non-alternating) finite-memory automata, we also write $C_0\stackrel{𝝈}{⟶}{C}_n$. This run is accepting, if $C_n\subseteq F\times \mathrm{\Sigma }$, i.e., $C_n$ is a set of accepting configurations, and the automaton accepts a word $𝝈\in {\mathrm{\Sigma }}^{\ast }$, if there is an accepting run of $𝑨$ on $𝝈$. The language $L(𝑨)$ consists of all words accepted by $𝑨$.

The proof of Proposition 14 is similar to that of [19, Lemma 1] and is omitted. As a corollary, every run of the automata is mapped by permutations to an “equivalent” run.

Our pumping lemma for alternating finite-memory automata is as follows.

As the section title suggests, this section contains a number of applications of Theorem 16.

In this section, we provide a high-level overview of the proof strategy, highlighting the key techniques and the main challenges involved.

The core difference in proving a pumping lemma for languages over infinite alphabets stems from the unbounded variability of symbols. Unlike classical finite-alphabet automata, we cannot rely on repetitions of identical configurations to enable pumping.

Suppose, ideally, that a run contains two sets of configurations where the latter is a subset of the former. In this case, the subword between them could be pumped directly. However, such inclusion is rare, especially as transitions may introduce fresh symbols into the configurations. This obstacle motivates the need for a more flexible framework for comparing configurations.

The key idea, originally introduced in [19, Appendix A], is to shift from reasoning about concrete sets of configurations to a more structured representation: nonnegative integer vectors. Specifically, we map finite sets of configurations to vectors in ${\mathbb{N}}^{2^{\Vert S\Vert }-1}$, where each coordinate corresponds to a nonempty set of states and counts how many distinct symbols are currently associated with that set.

As a result, we obtain a sequence of $\left(2^{\Vert S\Vert }-1\right)$-dimensional vectors $v_0,v_1,\mathrm{\dots }$ and seek a pair of indices such that $v_j$ is component-wise less than or equal to $v_i$. If such a pair exists, we can find a permutation that maps the symbols of the configuration set related to $v_j$ to those of the configuration set related to $v_i$, while maintaining the correspondence between the respective sets of states they are associated with. Then, the corresponding pattern can be pumped iteratively under that permutation.

Here another (major) problem arises: in an arbitrary sequence $v_0,v_1,\mathrm{\dots }$ of natural-valued vectors, such pair $v_i,v_j$ does not necessarily exist. Therefore, techniques of forward analysis of well-structured transition systems do not apply [13, 14, 2]. This motivates a fundamental shift in perspective. Instead of analyzing the computation forward, we analyze the computation backward, from the final set of configurations toward the initial one.

Reversing the computation introduces a new complication: the number of symbols in the final configuration depends on the input length and, therefore, is unbounded. To address this, we restrict the sets of configurations to only those involving symbols in the suffix of the input. This pruning retains all relevant information for acceptance while ensuring that each configuration involves only symbols drawn from a bounded domain. As a result, the associated vector sequence becomes linearly bounded in its size.

This boundedness is crucial: it places the vector sequence within a well-quasi-ordered space, which guarantees the existence of such a pair of comparable vectors, corresponding to a “pumpable” structure in the original computation.

Our backward analysis technique refines the approach in [8], where configuration sets were truncated with an integer cap. Here, instead we restrict the configuration sets to a finite domain, the set of symbols drawn from the suffix of the word.

The proof of Theorem 16 itself is composed of finding sufficient conditions for a pattern to be pumped. The sufficient condition we need is established step by step. First, we show that pumping is possible, if we already have an appropriate $\mathrm{\Delta }$-permutation of $\mathrm{\Sigma }$ and then, we show that such a permutation exists, if the automaton run meets certain requirements. Finally, we prove that any sufficiently long run meets this requirement, thereby completing the proof of Theorem 16. In the following sections we state the main lemmas associated with each of these three steps.