Friedrich-Alexander-Universität Erlangen-Nürnberg,
Germanyhenning.urbat@fau.dehttps://orcid.org/0000-0002-3265-7168Supported by
Deutsche Forschungsgemeinschaft (DFG) under project SCHR 1118/15-1 Gothenburg
University,
Swedendaniel.hausmann@fau.dehttps://orcid.org/0000-0002-0935-8602Supported by
Deutsche Forschungsgemeinschaft (DFG) under project MI 717/7-1 and by the
European Research Council (ERC) under project 772459 Friedrich-Alexander-
Universität Erlangen-Nürnberg, Germanymail@stefan-
milius.euhttps://orcid.org/0000-0002-2021-1644Supported by Deutsche
Forschungsgemeinschaft (DFG) under project MI 717/7-1 Friedrich-Alexander-
Universität Erlangen-Nürnberg,
Germanylutz.schroeder@fau.dehttps://orcid.org/0000-0002-3146-5906Supported by
Deutsche Forschungsgemeinschaft (DFG) under project SCHR 1118/15-1 Henning
Urbat, Daniel Hausmann, Stefan Milius, Lutz Schröder[500]Theory of computation
Automata over infinite objects

# Nominal Büchi Automata with Name Allocation

Henning Urbat  Daniel Hausmann  Stefan Milius  Lutz Schröder

###### Abstract

Infinite words over infinite alphabets serve as models of the temporal
development of the allocation and (re-)use of resources over linear time. We
approach $\omega$-languages over infinite alphabets in the setting of nominal
sets, and study languages of _infinite bar strings_ , i.e. infinite sequences
of names that feature binding of fresh names; binding corresponds roughly to
reading letters from input words in automata models with registers. We
introduce _regular nominal nondeterministic Büchi automata_ (_Büchi RNNAs_),
an automata model for languages of infinite bar strings, repurposing the
previously introduced _RNNAs_ over finite bar strings. Our machines feature
explicit binding (i.e. resource-allocating) transitions and process their
input via a Büchi-type acceptance condition. They emerge from the abstract
perspective on name binding given by the theory of nominal sets. As our main
result we prove that, in contrast to most other nondeterministic automata
models over infinite alphabets, language inclusion of Büchi RNNAs is decidable
and in fact elementary. This makes Büchi RNNAs a suitable tool for
applications in model checking.

###### keywords:

Data languages, infinite words, nominal sets, inclusion checking

##  1 Introduction

Classical automata models and formal languages for finite words over finite
alphabets have been extended to infinity in both directions: Infinite words
model the long-term temporal development of systems, while infinite alphabets
model _data_ , such as nonces [19], object identities [14], or abstract
resources [5]. We approach _data $\omega$-languages_, i.e. languages of
infinite words over infinite alphabets, in the setting of nominal sets [25]
where elements of sets are thought of as carrying (finitely many) _names_ from
a fixed countably infinite reservoir. Following the paradigm of nominal
automata theory [3], we take the set of names as the alphabet; we work with
infinite words containing explicit name binding in the spirit of previous work
on nominal formalisms for finite words such as nominal Kleene algebra [11] and
regular nondeterministic nominal automata (RNNAs) [26]. Name binding may be
viewed as the allocation of resources, or (yet) more abstractly as an
operation that reads fresh names from the input. We refer to such infinite
words as _infinite bar strings_ , in honour of the vertical bar notation we
employ for name binding. In the present paper, we introduce a notion of
nondeterministic nominal automata over infinite bar strings, and show that it
admits inclusion checking in elementary complexity.

Specifically, we reinterpret the mentioned RNNAs to accept infinite rather
than finite bar strings by equipping them with a Büchi acceptance condition;
like over finite alphabets, automata with more expressive acceptance
conditions including Muller acceptance can be translated into the basic
(nondeterministic) Büchi model. Our mentioned main result then states that
language inclusion of Büchi RNNAs is decidable in parametrized polynomial
space [27], with a parameter that may be thought as the number of registers.
This is in sharp contrast to other nondeterministic automata models for
infinite words over infinite alphabets, which sometimes have decidable
emptiness problems but whose inclusion problems are typically either
undecidable or of prohibitively high complexity even under heavy restrictions
(inclusion is not normally reducible to emptiness since nondeterministic
models typically do not determinize, and in fact tend to fail to be closed
under complement); details are in the related work section.

Infinite bar strings can be concretized to infinite strings of names (i.e.
essentially to data words) by interpreting name binding as reading either
globally fresh letters (in which case Büchi RNNAs may essentially be seen as a
variant of session automata [4] for infinite words) or locally fresh letters.
Both interpretations arise from disciplines of $\alpha$-renaming as known from
$\lambda$-calculus [1], with global freshness corresponding to a discipline of
_clean_ naming where bound names are never shadowed, and local freshness
corresponding to an unrestricted naming discipline that does allow shadowing.
The latter implies that local freshness can only be enforced w.r.t. names that
are expected to be seen again later in the word. It is precisely this fairly
reasonable-sounding restriction that buys the comparatively low computational
complexity of the model, which on the other hand allows full nondeterminism
(and, e.g., accepts the language ‘some letter occurs infinitely often’, which
is not acceptable by deterministic register-based models) and unboundedly many
registers. Büchi RNNAs thus provide a reasonably expressive automata model for
infinite data words whose main reasoning problems are decidable in elementary
complexity.

### Related Work

Büchi RNNAs generally adhere to the paradigm of register automata, which in
their original incarnation over finite words [16] are equivalent to the
nominal automaton model of nondeterministic orbit-finite automata [3]. Ciancia
and Sammartino [5] study _deterministic_ nominal Muller automata accepting
infinite strings of names, and show Boolean closure and decidability of
inclusion. This model is incomparable to ours; details are in Section 7. For
alternating register automata over infinite data words, emptiness is
undecidable even when only one register is allowed (which over finite data
words does ensure decidability) [9]. For the one-register safety fragment of
the closely related logic Freeze LTL, inclusion (i.e. refinement) is
decidable, but even the special case of validity is not primitive recursive
[21], in particular not elementary.

Many automata models and logics for data words deviate rather substantially
from the register paradigm, especially models in the vicinity of data automata
[2], whose emptiness problem is decidable but at least as hard as Petri net
reachability, which by recent results is not elementary [7], in fact
Ackermann-complete [22, 8]. For weak Büchi data automata [17], the emptiness
problem is decidable in elementary complexity. Similarly, Büchi generalized
data automata [6] have a decidable emptiness problem; their Büchi component is
deterministic. (Throughout, nothing appears to be said about inclusion of data
automata.) Variable finite automata [15] apply to both finite and infinite
words; in both versions, the inclusion problem of the nondeterministic variant
is undecidable.

##  2 Preliminaries: Nominal Sets

Nominal sets form a convenient formalism for dealing with names and freshness;
for our present purposes, names play the role of data. We briefly recall basic
notions and facts and refer to [25] for a comprehensive introduction. Fix a
countably infinite set $\mathbb{A}$ of _names_ , and let
$\mathsf{Perm}(\mathbb{A})$ denote the group of finite permutations on
$\mathbb{A}$, which is generated by the _transpositions_ $(a\,b)$ for $a\neq
b\in\mathbb{A}$ (recall that $(a\,b)$ just swaps $a$ and $b$). A _nominal set_
is a set $X$ equipped with a (left) group action
$\mathsf{Perm}(\mathbb{A})\times X\to X$, denoted $(\pi,x)\mapsto\pi\cdot x$,
such that every element $x\in X$ has a finite _support_
$S\subseteq\mathbb{A}$, i.e. $\pi\cdot x=x$ for every
$\pi\in\mathsf{Perm}(\mathbb{A})$ such that $\pi(a)=a$ for all $a\in S$. Every
element $x$ of a nominal set $X$ has a least finite support, denoted
$\operatorname{\mathsf{supp}}(x)$. Intuitively, one should think of $X$ as a
set of syntactic objects (e.g. strings, $\lambda$-terms, programs), and of
$\operatorname{\mathsf{supp}}(x)$ as the set of names needed to describe an
element $x\in X$. A name $a\in\mathbb{A}$ is _fresh_ for $x$, denoted
$a\mathbin{\\#}x$, if $a\notin\operatorname{\mathsf{supp}}(x)$. The _orbit_ of
an element $x\in X$ is given by $\\{\pi\cdot
x:\pi\in\mathsf{Perm}(\mathbb{A})\\}$. The orbits form a partition of $X$. The
nominal set $X$ is _orbit-finite_ if it has only finitely many orbits.

Putting $\pi\cdot a=\pi(a)$ makes $\mathbb{A}$ into a nominal set. Moreover,
$\mathsf{Perm}(\mathbb{A})$ acts on subsets $A\subseteq X$ of a nominal set
$X$ by $\pi\cdot A=\\{\pi\cdot x:x\in A\\}$. A subset $A\subseteq X$ is
_equivariant_ if $\pi\cdot A=A$ for all $\pi\in\mathsf{Perm}(\mathbb{A})$.
More generally, it is _finitely supported_ if it has finite support w.r.t.
this action, i.e. there exists a finite set $S\subseteq\mathbb{A}$ such that
$\pi\cdot A=A$ for all $\pi\in\mathsf{Perm}(\mathbb{A})$ such that $\pi(a)=a$
for all $a\in S$. The set $A$ is _uniformly finitely supported_ if
$\bigcup_{x\in A}\operatorname{\mathsf{supp}}(x)$ is a finite set. This
implies that $A$ is finitely supported, with least support
$\operatorname{\mathsf{supp}}(A)=\bigcup_{x\in
A}\operatorname{\mathsf{supp}}(x)$ [10, Theorem 2.29]. (The converse does not
hold, e.g. the set $\mathbb{A}$ is finitely supported but not uniformly
finitely supported.) Uniformly finitely supported orbit-finite sets are always
finite (since an orbit-finite set contains only finitely many elements with a
given finite support). We respectively denote by
$\mathcal{P}_{\mathsf{ufs}}(X)$ and $\mathcal{P}_{\mathsf{fs}}(X)$ the nominal
sets of (uniformly) finitely supported subsets of a nominal set $X$.

A map $f\colon X\to Y$ between nominal sets is _equivariant_ if $f(\pi\cdot
x)=\pi\cdot f(x)$ for all $x\in X$ and $\pi\in\mathsf{Perm}(\mathbb{A})$.
Equivariance implies
$\operatorname{\mathsf{supp}}(f(x))\subseteq\operatorname{\mathsf{supp}}(x)$
for all $x\in X$. The function $\operatorname{\mathsf{supp}}$ itself is
equivariant, i.e. $\operatorname{\mathsf{supp}}(\pi\cdot
x)=\pi\cdot\operatorname{\mathsf{supp}}(x)$ for
$\pi\in\mathsf{Perm}(\mathbb{A})$. Hence
$|\operatorname{\mathsf{supp}}(x_{1})|=|\operatorname{\mathsf{supp}}(x_{2})|$
whenever $x_{1}$, $x_{2}$ are in the same orbit of a nominal set.

We denote by $\operatorname{\mathbf{Nom}}$ the category of nominal sets and
equivariant maps. The object maps $X\mapsto\mathcal{P}_{\mathsf{ufs}}(X)$ and
$X\mapsto\mathcal{P}_{\mathsf{fs}}(X)$ extend to endofunctors
$\mathcal{P}_{\mathsf{ufs}}\colon\operatorname{\mathbf{Nom}}\to\operatorname{\mathbf{Nom}}$
and
$\mathcal{P}_{\mathsf{fs}}\colon\operatorname{\mathbf{Nom}}\to\operatorname{\mathbf{Nom}}$
sending an equivariant map $f\colon X\to Y$ to the map $A\mapsto f[A]$.

The coproduct $X+Y$ of nominal sets $X$ and $Y$ is given by their disjoint
union with the group action inherited from the two summands. Similarly, the
product $X\times Y$ is given by the cartesian product with the componentwise
group action; we have
$\operatorname{\mathsf{supp}}(x,y)=\operatorname{\mathsf{supp}}(x)\cup\operatorname{\mathsf{supp}}(y)$.
Given a nominal set $X$ equipped with an equivariant equivalence relation,
i.e. an equivalence relation $\sim$ that is equivariant as a subset
$\mathord{\sim}\subseteq X\times X$, the quotient $X/\mathord{\sim}$ is a
nominal set under the expected group action defined by
$\pi\cdot[x]_{\sim}=[\pi\cdot x]_{\sim}$.

A key role in the technical development is played by _abstraction sets_ ,
which provide a semantics for binding mechanisms [12]. Given a nominal set
$X$, an equivariant equivalence relation $\sim$ on $\mathbb{A}\times X$ is
defined by $(a,x)\sim(b,y)$ iff $(a\,c)\cdot x=(b\,c)\cdot y$ for some
(equivalently, all) fresh $c$. The _abstraction set_ $[\mathbb{A}]X$ is the
quotient set $(\mathbb{A}\times X)/\mathord{\sim}$. The $\sim$-equivalence
class of $(a,x)\in\mathbb{A}\times X$ is denoted by $\langle a\rangle
x\in[\mathbb{A}]X$. We may think of $\sim$ as an abstract notion of
$\alpha$-equivalence, and of $\langle a\rangle$ as binding the name $a$.
Indeed we have $\operatorname{\mathsf{supp}}(\langle a\rangle
x)=\operatorname{\mathsf{supp}}(x)\setminus\\{a\\}$ (while
$\operatorname{\mathsf{supp}}(a,x)=\\{a\\}\cup\operatorname{\mathsf{supp}}(x)$),
as expected in binding constructs.

The object map $X\mapsto[\mathbb{A}]X$ extends to an endofunctor
$[\mathbb{A}]\colon\operatorname{\mathbf{Nom}}\to\operatorname{\mathbf{Nom}}$
sending an equivariant map $f\colon X\to Y$ to the equivariant map
$[\mathbb{A}]f\colon[\mathbb{A}]X\to[\mathbb{A}]Y$ given by $\langle a\rangle
x\mapsto\langle a\rangle f(x)$ for $a\in\mathbb{A}$ and $x\in X$.

##  3 The Notion of $\boldsymbol{\alpha}$-Equivalence for Bar Strings

In the following we investigate automata consuming input words over the
infinite alphabet

$\overline{\mathbb{A}}:=\mathbb{A}\cup\\{{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a:a\in\mathbb{A}\\}.$

A _finite bar string_ is a finite word $\sigma_{1}\sigma_{2}\cdots\sigma_{n}$
over $\overline{\mathbb{A}}$, and _infinite bar string_ is an infinite word
$\sigma_{1}\sigma_{2}\sigma_{3}\cdots$ over $\overline{\mathbb{A}}$. We denote
the sets of finite and infinite bar strings by $\overline{\mathbb{A}}^{*}$ and
$\overline{\mathbb{A}}^{\omega}$, respectively. Given
$w\in\overline{\mathbb{A}}^{*}\cup\overline{\mathbb{A}}^{\omega}$ the set of
_names_ in $w$ is defined by

$\mathsf{N}(w)=\\{a\in\mathbb{A}:\text{the letter $a$ or ${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$ occurs in
$w$}\\}.$

An infinite bar string $w$ is _finitely supported_ if $\mathsf{N}(w)$ is a
finite set; we let
$\overline{\mathbb{A}}^{\omega}_{\mathsf{fs}}\subseteq\overline{\mathbb{A}}^{\omega}$
denote the set of finitely supported infinite bar strings. Note that
$\overline{\mathbb{A}}^{*}$ and $\overline{\mathbb{A}}^{\omega}_{\mathsf{fs}}$
are nominal sets w.r.t. the group action defined pointwise. The least support
of a bar string is its set of names.

A bar string containing only letters from $\mathbb{A}$ is called a _data
word_. We denote by $\mathbb{A}^{*}\subseteq\overline{\mathbb{A}}^{*}$,
$\mathbb{A}^{\omega}\subseteq\overline{\mathbb{A}}^{\omega}$ and
$\mathbb{A}^{\omega}_{\mathsf{fs}}\subseteq\overline{\mathbb{A}}^{\omega}_{\mathsf{fs}}$
the sets of finite data words, infinite data words, and finitely supported
infinite data words, respectively.

We interpret ${\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a$ as binding the name $a$ to the right. Accordingly, a name
$a\in\mathbb{A}$ is said to be _free_ in a bar string
$w\in\overline{\mathbb{A}}^{*}\cup\overline{\mathbb{A}}^{\omega}$ if (i) the
letter $a$ occurs in $w$, and (ii) the first occurrence of $a$ is not preceded
by any occurrence of ${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$. For
instance, the name $a$ is free in $a{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}aba$ but not
free in ${\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}aaba$, while the name $b$ is free in both bar strings. We put

$\mathsf{FN}(w)=\\{a\in\mathbb{A}:\text{$a$ is free in $w$}\\}.$

We obtain a natural notion of $\alpha$-equivalence for both finite and
infinite bar strings; the finite case is taken from [26].

######  Definition  ($\alpha$-equivalence).

Let $=_{\alpha}$ be the least equivalence relation on
$\overline{\mathbb{A}}^{*}$ such that

$x{\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}av=_{\alpha}x{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}bw\qquad\text{for all $a,b\in\mathbb{A}$ and
$x,v,w\in\overline{\mathbb{A}}^{*}$ such that $\langle a\rangle v=\langle
b\rangle w$}.$

This extends to an equivalence relation $=_{\alpha}$ on
$\overline{\mathbb{A}}^{\omega}$ given by

$v=_{\alpha}w\qquad\text{iff}\qquad v_{n}=_{\alpha}w_{n}\quad\text{for all
$n\in{\mathbb{N}}$},$

where $v_{n}$ and $w_{n}$ are the prefixes of length $n$ of $v$ and $w$. We
denote by $\overline{\mathbb{A}}^{*}/\mathord{=_{\alpha}}$ and
$\overline{\mathbb{A}}^{\omega}/\mathord{=_{\alpha}}$ the sets of
$\alpha$-equivalence classes of finite and infinite bar strings, respectively,
and we write $[w]_{\alpha}$ for the $\alpha$-equivalence class of
$w\in\overline{\mathbb{A}}^{*}\cup\overline{\mathbb{A}}^{\omega}$.

######  Remark .

  1. 1.

For any $v,w\in\overline{\mathbb{A}}^{*}$ the condition $\langle a\rangle
v=\langle b\rangle w$ holds if and only if

$a=b$ and $v=w$, or $b\mathbin{\\#}v$ and $(a\,b)\cdot v=w$.

  2. 2.

The $\alpha$-equivalence relation is a _left congruence_ :

$v=_{\alpha}w\quad\text{implies}\quad xv=_{\alpha}xw\qquad\qquad\text{for all
$v,w\in\overline{\mathbb{A}}^{*}\cup\overline{\mathbb{A}}^{\omega}$ and
$x\in\overline{\mathbb{A}}^{*}$.}$

Moreover, the _right cancellation property_ holds:

$vx=_{\alpha}wx\quad\text{implies}\quad v=_{\alpha}w\qquad\qquad\text{for all
$v,w\in\overline{\mathbb{A}}^{*}$ and
$x\in\overline{\mathbb{A}}^{*}\cup\overline{\mathbb{A}}^{\omega}$.}$

  3. 3.

The equivalence relation $=_{\alpha}$ is equivariant. Therefore, both
$\overline{\mathbb{A}}^{*}/{=_{\alpha}}$ and
$\overline{\mathbb{A}}^{\omega}_{\mathsf{fs}}/{=_{\alpha}}$ are nominal sets
with the group action $\pi\cdot[w]_{\alpha}=[\pi\cdot w]_{\alpha}$ for
$\pi\in\mathsf{Perm}(\mathbb{A})$ and
$w\in\overline{\mathbb{A}}^{*}\cup\overline{\mathbb{A}}^{\omega}_{\mathsf{fs}}$.
The least support of $[w]_{\alpha}$ is the set $\mathsf{FN}(w)$ of free names
of $w$.

######  Remark .

Our notion of $\alpha$-equivalence on infinite bar strings differs from the
equivalence relation generated by relating $x{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}av$ and
$x{\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}bw$
whenever $\langle a\rangle v=\langle b\rangle w$ (as in Section 3 but now for
infinite bar strings $v,w\in\overline{\mathbb{A}}^{\omega}_{\mathsf{fs}}$):
The latter equivalence relates two bar strings iff they can be transformed
into each other by finitely many $\alpha$-renamings, while the definition of
$\alpha$-equivalence as per Section 3 allows infinitely many simultaneous
$\alpha$-renamings; e.g. the infinite bar string $(|aa)^{\omega}={\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}aa{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}aa{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}aa{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}aa\cdots$ is
$\alpha$-equivalent to $(|aa|bb)^{\omega}={\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}aa{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}bb{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}aa{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}bb\cdots$.

######  Definition .

A _literal language_ , _bar language_ or _data language_ is a subset of
$\overline{\mathbb{A}}^{*}$, $\overline{\mathbb{A}}^{*}/{=_{\alpha}}$ or
$\mathbb{A}^{*}$, respectively. Similarly, a _literal $\omega$-language_, _bar
$\omega$-language_ or _data $\omega$-language_ is a subset of
$\overline{\mathbb{A}}^{\omega}$,
$\overline{\mathbb{A}}^{\omega}/{=_{\alpha}}$ or $\mathbb{A}^{\omega}$,
respectively.

######  Notation .

Given a finite or infinite bar string
$w\in\overline{\mathbb{A}}^{*}\cup\overline{\mathbb{A}}^{\omega}$ we let
$\mathsf{ub}(w)$ denote the data word obtained by replacing every occurrence
of ${\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$
in $w$ by $a$; e.g. $\mathsf{ub}({\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}aa{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}bb)=aaabb$. To
every bar ($\omega$-)language $L$ we associate the data ($\omega$-)language
$D(L)$ given by

$D(L)=\\{\mathsf{ub}(w):[w]_{\alpha}\in L\\}.$

######  Definition .

A finite or infinite bar string $w$ is _clean_ if for each
$a\in\mathsf{FN}(w)$ the letter ${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$ does not
occur in $w$, and for each $a\not\in\mathsf{FN}(w)$ the letter ${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$ occurs at
most once.

######  Lemma 3.1.

Every bar string
$w\in\overline{\mathbb{A}}^{*}\cup\overline{\mathbb{A}}^{\omega}_{\mathsf{fs}}$
is $\alpha$-equivalent to a (not necessarily finitely supported) clean bar
string.

######  Proof 3.2.

Since $w$ has finite support, for every occurrence of the letter ${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$ for which
$a$ or ${\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a$ has already occurred before, one can replace ${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$ by ${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}b$ for some
fresh name $b$ and replace the suffix $v$ after ${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$ by
$(a\,b)v$. Iterating this yields a clean bar string $\alpha$-equivalent to
$w$.

######  Example 3.3.

  1. 1.

The finitely supported infinite bar string ${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}aa{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}bb{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}aa{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}bb\cdots$ is
$\alpha$-equivalent to the clean bar string ${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a_{1}a_{1}{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a_{2}a_{2}{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a_{3}a_{3}{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a_{4}a_{4}\cdots$ where the $a_{i}$ are pairwise distinct names.
Note that ${\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}aa{\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}bb{\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}aa{\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}bb\cdots$ is not $\alpha$-equivalent to any finitely supported clean
bar string.

  2. 2.

For non-finitely supported bar strings the lemma generally fails: if
$\mathbb{A}=\\{a_{1},a_{2},a_{3},\cdots\\}$ then the bar string $a_{1}{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a_{1}a_{2}a_{3}a_{4}a_{5}a_{6}a_{7}\cdots$ is not
$\alpha$-equivalent to any other bar string, in particular not to a clean one.

For readers familiar with the theory of coalgebras we note that on infinite
bar strings with finite support, $\alpha$-equivalence naturally emerges from a
coinductive point of view. Kurz et al. [20] use coinduction to devise a
general notion of $\alpha$-equivalence for infinitary terms over a binding
signature, which form the final colgebra for an associated endofunctor on
$\operatorname{\mathbf{Nom}}$. The following is the special case for the
endofunctors

$GX=\overline{\mathbb{A}}\times X\cong\mathbb{A}\times X+\mathbb{A}\times
X\qquad\text{and}\qquad FX=\mathbb{A}\times X+[\mathbb{A}]X.$

Let $\nu F$ and $\nu G$ denote their respective final coalgebras. The
coalgebra $\nu G$ is carried by the nominal set
$\overline{\mathbb{A}}^{\omega}_{\mathsf{fs}}$ with the usual coalgebra
structure
$\langle\mathsf{hd},\mathsf{tl}\rangle\colon\overline{\mathbb{A}}^{\omega}_{\mathsf{fs}}\to\overline{\mathbb{A}}\times\overline{\mathbb{A}}^{\omega}_{\mathsf{fs}}$
decomposing an infinite string into its head and tail. The natural
transformation

$\sigma_{X}\colon GX\twoheadrightarrow FX\qquad\text{given
by}\qquad(a,x)\mapsto(a,x),\quad({\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a,x)\mapsto\langle a\rangle x,$

then induces a canonical map
$e_{\alpha}\colon\overline{\mathbb{A}}^{\omega}_{\mathsf{fs}}\to\nu F$, viz.
the unique homomorphism from the $F$-coalgebra $\nu
G\xrightarrow{\leavevmode\nobreak\
\langle\mathsf{hd},\mathsf{tl}\rangle\leavevmode\nobreak\ }G(\nu
G)\xrightarrow{\leavevmode\nobreak\ \sigma_{\nu G}\leavevmode\nobreak\ }F(\nu
G)$ into the final coalgebra $\nu F$.

######  Proposition 3.4.

For every $v,w\in\overline{\mathbb{A}}^{\omega}_{\mathsf{fs}}$ we have
$v=_{\alpha}w$ if and only if $e_{\alpha}(v)=e_{\alpha}(w)$.

##  4 Automata over Infinite Bar Strings

We proceed to introduce Büchi RNNAs, our nominal automaton model for bar
$\omega$-languages and data $\omega$-languages. It modifies regular nominal
nondeterministic automata (RNNAs) [26], originally introduced for bar
languages and data languages of finite words, to accept infinite words.
Roughly, Büchi RNNAs are to RNNAs what classical Büchi automata [13] are to
nondeterministic finite automata. We first recall:

######  Definition 1 (RNNA [26]).

  1. 1.

An _RNNA_ $A=(Q,R,q_{0},F)$ is given by an orbit-finite nominal set $Q$ of
_states_ , an equivariant relation $R\subseteq
Q\times\overline{\mathbb{A}}\times Q$ specifying _transitions_ , an _initial
state_ $q_{0}\in Q$ and an equivariant set $F\subseteq Q$ of _final states_.
We write $q\xrightarrow{\leavevmode\nobreak\ \sigma\leavevmode\nobreak\
}q^{\prime}$ if $(q,\sigma,q^{\prime})\in R$. The transitions are subject to
two conditions:

    1. (1)

_$\alpha$ -invariance_: if $q\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }q^{\prime}$ and $\langle a\rangle
q^{\prime}=\langle b\rangle q^{\prime\prime}$, then
$q\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}b\leavevmode\nobreak\ }q^{\prime\prime}$.

    2. (2)

_Finite branching up to $\alpha$-invariance:_ For each $q\in Q$ the sets
$\\{(a,q^{\prime}):q\xrightarrow{\leavevmode\nobreak\ a\leavevmode\nobreak\
}q^{\prime}\\}$ and $\\{\langle a\rangle
q^{\prime}:q\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }q^{\prime}\\}$ are finite (equivalently,
uniformly finitely supported).

The _degree_ of $A$, denoted $\mathsf{deg}(A)$, is the maximum of all
$|\operatorname{\mathsf{supp}}(q)|$ where $q\in Q$.

  2. 2.

Given a finite bar string
$w=\sigma_{1}\sigma_{2}\cdots\sigma_{n}\in\overline{\mathbb{A}}^{*}$ and a
state $q\in Q$, a _run_ for $w$ from $q$ is a sequence of transitions

$q\xrightarrow{\leavevmode\nobreak\ \sigma_{1}\leavevmode\nobreak\
}q_{1}\xrightarrow{\leavevmode\nobreak\ \sigma_{2}\leavevmode\nobreak\
}\cdots\xrightarrow{\leavevmode\nobreak\ \sigma_{n}\leavevmode\nobreak\
}q_{n}.$

The run is _accepting_ if $q_{n}$ is final. The state $q$ _accepts_ $w$ if
there exists an accepting run for $w$ from $q$, and the automaton $A$
_accepts_ $w$ if its initial state $q_{0}$ accepts $w$. We define

$\displaystyle L_{0}(A)$
$\displaystyle=\\{w\in\overline{\mathbb{A}}^{*}:\text{$A$ accepts $w$}\\},$
the literal language accepted by $A$, $\displaystyle L_{\alpha}(A)$
$\displaystyle=\\{[w]_{\alpha}:w\in\overline{\mathbb{A}}^{*},\,\text{$A$
accepts $w$}\\},$ the bar language accepted by $A$, $\displaystyle D(A)$
$\displaystyle=D(L_{\alpha}(A)),$ $\displaystyle\text{the \emph{data language
accepted by $A$}}.$

######  Remark 2.

Equivalently, an RNNA is an orbit-finite coalgebra

$Q\longrightarrow 2\times\mathcal{P}_{\mathsf{ufs}}(\mathbb{A}\times
Q)\times\mathcal{P}_{\mathsf{ufs}}([\mathbb{A}]Q)$

for the functor $FX=2\times\mathcal{P}_{\mathsf{ufs}}(\mathbb{A}\times
X)\times\mathcal{P}_{\mathsf{ufs}}([\mathbb{A}]X)$ on
$\operatorname{\mathbf{Nom}}$, with an initial state $q_{0}\in Q$.

######  Definition 3 (Büchi RNNA).

A _Büchi RNNA_ is an RNNA $A=(Q,R,q_{0},F)$ used to recognize infinite bar
strings as follows. Given
$w=\sigma_{1}\sigma_{2}\sigma_{3}\cdots\in\overline{\mathbb{A}}^{\omega}$ and
a state $q\in Q$, a _run_ for $w$ from $q$ is an infinite sequence of
transitions

$q_{0}\xrightarrow{\leavevmode\nobreak\ \sigma_{1}\leavevmode\nobreak\
}q_{1}\xrightarrow{\leavevmode\nobreak\ \sigma_{2}\leavevmode\nobreak\
}q_{2}\xrightarrow{\leavevmode\nobreak\ \sigma_{3}\leavevmode\nobreak\
}\cdots.$

The run is _accepting_ if $q_{n}$ is final for infinitely many
$n\in{\mathbb{N}}$. The state $q$ _accepts_ $w$ if there exists an accepting
run for $w$ from $q$, and the automaton $A$ _accepts_ $w$ if its initial state
$q_{0}$ accepts $w$. We define

$\displaystyle L_{0,\omega}(A)$
$\displaystyle=\\{w\in\overline{\mathbb{A}}^{\omega}:\text{$A$ accepts
$w$}\\},$ the literal $\omega$-language accepted by $A$, $\displaystyle
L_{\alpha,\omega}(A)$
$\displaystyle=\\{[w]_{\alpha}:w\in\overline{\mathbb{A}}^{\omega},\,\text{$A$
accepts $w$}\\},$ the bar $\omega$-language accepted by $A$, $\displaystyle
D_{\omega}(A)$ $\displaystyle=D(L_{\alpha,\omega}(A)),$
$\displaystyle\text{the \emph{data $\omega$-language accepted by $A$}}.$

######  Example 4.1.

Consider the Büchi RNNA $A$ with states
$\\{q_{0}\\}\cup\mathbb{A}\times\\{0,1\\}$ and transitions as displayed below,
where $a,b$ range over distinct names in $\mathbb{A}$. Note that the second
node represents the orbit $\mathbb{A}\times\\{0\\}$ and the third one the
orbit $\mathbb{A}\times\\{1\\}$.

$q_{0}$start$(a,0)$$(a,1)$${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$$a$${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}b$${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}b$$a$

The data $\omega$-language $D_{\omega}(A)$ consists of all infinite words
$w\in\mathbb{A}^{\omega}$ where some name $a\in\mathbb{A}$ occurs infinitely
often.

######  Remark 4.

For automata consuming infinite words over infinite alphabets, a slightly
subtle point is whether to admit arbitrary infinite words as inputs or
restrict to finitely supported ones. For the bar language semantics of Büchi
RNNAs this choice is inconsequential: we shall see in 4.3 below that modulo
$\alpha$-equivalence all infinite bar strings accepted by Büchi RNNA are
finitely supported. However, for the data language semantics admitting strings
with infinite support is important for the decidability of language inclusion,
see 8.

######  Lemma 4.2 ([26, Lem. 5.4]).

Let $A=(Q,R,q_{0},F)$ be an RNNA, $q,q^{\prime}\in Q$ and $a\in\mathbb{A}$.

  1. 1.

If $q\xrightarrow{\leavevmode\nobreak\ a\leavevmode\nobreak\ }q^{\prime}$ then
$\operatorname{\mathsf{supp}}(q^{\prime})\cup\\{a\\}\subseteq\operatorname{\mathsf{supp}}(q)$.

  2. 2.

If $q\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }q^{\prime}$ then
$\operatorname{\mathsf{supp}}(q^{\prime})\subseteq\operatorname{\mathsf{supp}}(q)\cup\\{a\\}$.

  3. 3.

For every bar string
$w\in\overline{\mathbb{A}}^{*}\cup\overline{\mathbb{A}}^{\omega}$ with a run
from $q$ one has $\mathsf{FN}(w)\subseteq\operatorname{\mathsf{supp}}(q)$.

The next proposition will turn out to be crucial in the development that
follows. It asserts that, up to $\alpha$-equivalence, one can always restrict
the inputs of a Büchi RNNA to bar strings with a finite number of names,
bounded by the degree of the automaton.

######  Proposition 4.3.

Let $A$ be a Büchi RNNA accepting the infinite bar string
$w\in\overline{\mathbb{A}}^{\omega}$. Then it also accepts some
$w^{\prime}\in\overline{\mathbb{A}}^{\omega}_{\mathsf{fs}}$ such that

$w^{\prime}=_{\alpha}w\qquad\text{and}\qquad|\operatorname{\mathsf{supp}}(q_{0})\cup\mathsf{N}(w^{\prime})|\leq\mathsf{deg}(A)+1.$

######  Proof 4.4 (Proof sketch).

Put $m:=\mathsf{deg}(A)$, and choose $m+1$ pairwise distinct names
$a_{1},\ldots,a_{m+1}$ such that
$\operatorname{\mathsf{supp}}(q_{0})\subseteq\\{a_{1},\ldots,a_{m+1}\\}$.

  1. 1.

One first shows that for every finite bar string
$\sigma_{1}\sigma_{2}\cdots\sigma_{n}\in\overline{\mathbb{A}}^{*}$ and every
run

$q_{0}\xrightarrow{\leavevmode\nobreak\ \sigma_{1}\leavevmode\nobreak\
}q_{1}\xrightarrow{\leavevmode\nobreak\ \sigma_{2}\leavevmode\nobreak\
}q_{2}\xrightarrow{\leavevmode\nobreak\ \sigma_{3}\leavevmode\nobreak\
}\cdots\xrightarrow{\leavevmode\nobreak\ \sigma_{n}\leavevmode\nobreak\
}q_{n}$

in $A$ there exists
$\sigma_{1}^{\prime}\sigma_{2}^{\prime}\cdots\sigma_{n}^{\prime}\in\overline{\mathbb{A}}^{*}$
and a run

$q_{0}\xrightarrow{\leavevmode\nobreak\
\sigma_{1}^{\prime}\leavevmode\nobreak\
}q_{1}^{\prime}\xrightarrow{\leavevmode\nobreak\
\sigma_{2}^{\prime}\leavevmode\nobreak\
}q_{2}^{\prime}\xrightarrow{\leavevmode\nobreak\
\sigma_{3}^{\prime}\leavevmode\nobreak\
}\cdots\xrightarrow{\leavevmode\nobreak\
\sigma_{n}^{\prime}\leavevmode\nobreak\ }q_{n}^{\prime}$ (4.1)

such that (1) $q_{i}$ and $q_{i}^{\prime}$ lie in the same orbit for
$i=1,\ldots,n$, (2)
$\sigma_{1}^{\prime}\sigma_{2}^{\prime}\cdots\sigma_{n}^{\prime}=_{\alpha}\sigma_{1}\sigma_{2}\cdots\sigma_{n}$,
and (3)
$\mathsf{N}(\sigma_{1}^{\prime}\sigma_{2}^{\prime}\cdots\sigma_{n}^{\prime})\subseteq\\{a_{1},\ldots,a_{m+1}\\}$.
The proof is by induction on $n$ and rests on the observation that for every
state $q$ at least one of the names $a_{1},\ldots,a_{m+1}$ is fresh for $q$.

  2. 2.

Now suppose that the infinite bar string
$w=\sigma_{1}\sigma_{2}\sigma_{3}\cdots\in\overline{\mathbb{A}}^{\omega}$ is
accepted by $A$ via the accepting run

$q_{0}\xrightarrow{\leavevmode\nobreak\ \sigma_{1}\leavevmode\nobreak\
}q_{1}\xrightarrow{\leavevmode\nobreak\ \sigma_{2}\leavevmode\nobreak\
}q_{2}\xrightarrow{\leavevmode\nobreak\ \sigma_{3}\leavevmode\nobreak\
}\cdots$

Consider the set of all partial runs (4.1) satisfying the above conditions
(1)–(3). This set organizes into a tree with the edge relation given by
extension of runs; its nodes of depth $n$ are exactly the runs (4.1). By part
1 at least one such run exists for each $n\in{\mathbb{N}}$, i.e. the tree is
infinite. It is finitely branching because
$\operatorname{\mathsf{supp}}(q_{i}^{\prime})\subseteq\\{a_{1},\ldots,a_{m+1}\\}$
for all $i$ by 4.2, i.e. there are only finitely many runs (4.1) for each $n$.
Hence, by Kőnig’s lemma the tree contains an infinite path. This yields an
infinite run

$q_{0}\xrightarrow{\leavevmode\nobreak\
\sigma_{1}^{\prime}\leavevmode\nobreak\
}q_{1}^{\prime}\xrightarrow{\leavevmode\nobreak\
\sigma_{2}^{\prime}\leavevmode\nobreak\
}q_{2}^{\prime}\xrightarrow{\leavevmode\nobreak\
\sigma_{3}^{\prime}\leavevmode\nobreak\ }\cdots$

such that $q_{i}^{\prime}$ and $q_{i}$ lie in the same orbit for each $i$ and
$\sigma_{1}^{\prime}\cdots\sigma_{n}^{\prime}=_{\alpha}\sigma_{1}\cdots\sigma_{n}$
for each $n$. It follows that the Büchi RNNA $A$ accepts the infinite bar
string

$w^{\prime}=\sigma_{1}^{\prime}\sigma_{2}^{\prime}\sigma_{3}^{\prime}\cdots.$

Moreover $w^{\prime}=_{\alpha}w$ and
$\operatorname{\mathsf{supp}}(q_{0})\cup\mathsf{N}(w^{\prime})\subseteq\\{a_{1},\ldots,a_{m+1}\\}$
as required.

##  5 Name-Dropping Modification

Although the transitions of a Büchi RNNA are $\alpha$-invariant, its literal
$\omega$-language generally fails to be closed under $\alpha$-equivalence. For
instance, consider the Büchi RNNA with states
$\\{q_{0}\\}\cup\mathbb{A}\cup\mathbb{A}^{2}$ and transitions displayed below,
where $a,b$ range over distinct names in $\mathbb{A}$:

$q_{0}$start$a$$(a,b)$${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}b$${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}b$

The automaton accepts the infinite bar string ${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}b{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}b{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}b{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}b{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}b\cdots$ for
$a\neq b$ but does not accept the $\alpha$-equivalent ${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a\cdots$: the
required transitions $a\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }(a,b)$ and
$(a,b)\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }(a,b)$ do not exist since $a$ is in the least
support of the state $(a,b)$, which prevents $\alpha$-renaming of the given
transitions $a\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}b\leavevmode\nobreak\ }(a,b)$ and
$(a,b)\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}b\leavevmode\nobreak\ }(a,b)$. A possible fix is to add a new state
“$(\bot,b)$” that essentially behaves like $(a,b)$ but has the name $a$
dropped from its least support.

This idea can be generalized: We will show below how to transform any Büchi
RNNA $A$ into a Büchi RNNA $\widetilde{A}$ such that
$L_{0,\omega}(\widetilde{A})$ is the closure of $L_{0,\omega}(A)$ under
$\alpha$-equivalence, using the _name-dropping modification_ (6). The latter
simplifies a construction of the same name previously given for RNNA over
finite words [26], and it is the key to the decidability of bar language
inclusion proved later on. First, some technical preparations:

######  Remark 5 (Strong nominal sets).

A nominal set $Y$ is called _strong_ [28] if for every
$\pi\in\mathsf{Perm}(\mathbb{A})$ and $y\in Y$ one has $\pi\cdot y=y$ if and
only if $\pi(a)=a$ for all $a\in\operatorname{\mathsf{supp}}(y)$. (Note that
“if” holds in all nominal sets.) As shown in [24, Lem. 2.4.2] or [23, Cor.
B.27(2)] strong nominal sets are up to isomorphism precisely the nominal sets
of the form $Y=\sum_{i\in I}\mathbb{A}^{\\#X_{i}}$ where $X_{i}$ is a finite
set and $\mathbb{A}^{\\#X}$ denotes the nominal set of all injective maps from
$X$ to $\mathbb{A}$, with the group action defined pointwise;
$\mathbb{A}^{\\#X}$ may be seen as the set of possible configurations of an
$X$-indexed set of registers containing pairwise distinct names. The set of
orbits of $Y$ is in bijection with $I$; in particular, $Y$ is orbit-finite iff
$I$ is finite. Strong nominal sets can be regarded as analogues of free
algebras in categories of algebraic structures:

  1. 1.

For every nominal set $Z$ there exists a strong nominal set $Y$ and a
surjective equivariant map $e\colon Y\twoheadrightarrow Z$ that is
_$\operatorname{\mathsf{supp}}$ -nondecreasing_, i.e.
$\operatorname{\mathsf{supp}}(e(y))=\operatorname{\mathsf{supp}}(y)$ for all
$y\in Y$ [23, Cor. B.27.1]. (Recall that
$\operatorname{\mathsf{supp}}(e(y))\subseteq\operatorname{\mathsf{supp}}(y)$
always holds for equivariant maps.) Specifically, one can choose $Y=\sum_{i\in
I}\mathbb{A}^{\\#n_{i}}$ where $I$ is the set of orbits of $Z$ and $n_{i}$ is
the size of the support of any element of the orbit $i$. In particular, if $Z$
is orbit-finite then $Y$ is orbit-finite with the same number of orbits.

  2. 2.

Strong nominal sets are _projective_ w.r.t.
$\operatorname{\mathsf{supp}}$-nondecreasing quotients [23, Lem. B.28]: given
a strong nominal set $Y$, an equivariant map $h\colon Y\to Z$ and a
$\operatorname{\mathsf{supp}}$-nondecreasing quotient $e\colon
X\twoheadrightarrow Z$, there exists an equivariant map $g\colon Y\to X$ such
that $h=e\cdot g$.

######  Proposition 5.1.

For every Büchi RNNA there exists a Büchi RNNA accepting the same literal
$\omega$-language whose states form a strong nominal set.

######  Proof 5.2 (Proof sketch).

Given a Büchi RNNA viewed as a coalgebra

$Q\xrightarrow{\leavevmode\nobreak\ \gamma\leavevmode\nobreak\
}2\times\mathcal{P}_{\mathsf{ufs}}(\mathbb{A}\times
Q)\times\mathcal{P}_{\mathsf{ufs}}([\mathbb{A}]Q),$

express the nominal set $Q$ of states as a
$\operatorname{\mathsf{supp}}$-nondecreasing quotient $e\colon
P\twoheadrightarrow Q$ of an orbit-finite strong nominal set $P$ using 5. Note
that the type functor
$F(\mathop{-})=2\times\mathcal{P}_{\mathsf{ufs}}(\mathbb{A}\times\mathop{-})\times\mathcal{P}_{\mathsf{ufs}}([\mathbb{A}](\mathop{-}))$
preserves $\operatorname{\mathsf{supp}}$-nondecreasing quotients because all
the functors
$\mathcal{P}_{\mathsf{ufs}}(\mathop{-}),\mathbb{A}\times\mathop{-}$ and
$[\mathbb{A}](\mathop{-})$ do. Therefore, the right vertical arrow in the
square below is $\operatorname{\mathsf{supp}}$-nondecreasing, so projectivity
of $P$ yields an equivariant map $\beta$ making it commute:

${P}$${2\times\mathcal{P}_{\mathsf{ufs}}(\mathbb{A}\times
P)\times\mathcal{P}_{\mathsf{ufs}}([\mathbb{A}]P)}$${Q}$${2\times\mathcal{P}_{\mathsf{ufs}}(\mathbb{A}\times
Q)\times\mathcal{P}_{\mathsf{ufs}}([\mathbb{A}]Q)}$$\scriptstyle{e}$$\scriptstyle{\beta}$$\scriptstyle{2\times\mathcal{P}_{\mathsf{ufs}}(\mathbb{A}\times
e)\times\mathcal{P}_{\mathsf{ufs}}({[\mathbb{A}]}e)}$$\scriptstyle{\gamma}$

Thus $e$ is a coalgebra homomorphism from $(P,\beta)$ to $(Q,\gamma)$. It is
not difficult to verify that for every $p\in P$ the states $p$ and $e(p)$
accept the same literal $\omega$-language. In particular, equipping $P$ with
an initial state $p_{0}\in P$ such that $e(p_{0})=q_{0}$ we see that the Büchi
RNNAs $P$ and $Q$ accept the same literal $\omega$-language.

A Büchi RNNA with states $Q=\sum_{i\in I}\mathbb{A}^{\\#X_{i}}$ can be
interpreted as an automaton with a finite set $I$ of control states each of
which comes equipped with an $X_{i}$-indexed set of registers. The following
construction shows how to modify such an automaton, preserving the accepted
bar $\omega$-language, to become lossy in the sense that after each transition
some of the register contents may be nondeterministically erased. Technically,
this involves replacing $Q$ with $\widetilde{Q}=\sum_{i\in
I}\mathbb{A}^{\$X_{i}}$ where $\mathbb{A}^{\$X_{i}}$ is a the nominal set of
_partial_ injective maps from $X_{i}$ to $\mathbb{A}$, again with the
pointwise group action. (Note that while $\mathbb{A}^{\\#X_{i}}$ has only one
orbit, $\mathbb{A}^{\$X_{i}}$ has one orbit for every subset of $X_{i}$.) We
represent elements of $\widetilde{Q}$ as pairs $(i,r)$ where $i\in I$ and
$r\colon X_{i}\to\mathbb{A}$ is a partial injective map. The least support of
$(i,r)$ is given by

$\operatorname{\mathsf{supp}}(i,r)=\operatorname{\mathsf{supp}}(r)=\\{r(x):x\in\mathsf{dom}(r)\\},$

where $\mathsf{dom}(r)$ is the _domain_ of $r$, i.e. the set of all $x\in
X_{i}$ for which $r(x)$ is defined. We say that a partial map
$\overline{r}\colon X_{i}\to\mathbb{A}$ _extends_ $r$ if
$\mathsf{dom}(r)\subseteq\mathsf{dom}(\overline{r})$ and
$r(x)=\overline{r}(x)$ for all $x\in\mathsf{dom}(r)$.

######  Definition 6 (Name-dropping modification).

Let $A$ be a Büchi RNNA whose states form a strong nominal set $Q=\sum_{i\in
I}\mathbb{A}^{\\#X_{i}}$ (with $I$ and all $X_{i}$ finite). The _name-dropping
modification_ of $A$ is the Büchi RNNA $\widetilde{A}$ defined as follows:

  1. 1.

The states are given by $\widetilde{Q}=\sum_{i\in I}\mathbb{A}^{\$X_{i}}$.

  2. 2.

The initial state of $\widetilde{A}$ is equal to the initial state of $A$.

  3. 3.

$(i,r)$ is final in $\widetilde{A}$ iff some (equivalently, every111This is
due to the equivariance of the subset $F\subseteq Q$ of final states.) state
$(i,\mathop{-})$ in $A$ is final.

  4. 4.

$(i,r)\xrightarrow{\leavevmode\nobreak\ a\leavevmode\nobreak\ }(j,s)$ in
$\widetilde{A}$ iff
$\operatorname{\mathsf{supp}}(s)\cup\\{a\\}\subseteq\operatorname{\mathsf{supp}}(r)$
and $(i,\overline{r})\xrightarrow{\leavevmode\nobreak\ a\leavevmode\nobreak\
}(j,\overline{s})$ in $A$ for some $\overline{r},\overline{s}$ extending
$r,s$.

  5. 5.

$(i,r)\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }(j,s)$ in $\widetilde{A}$ iff
$\operatorname{\mathsf{supp}}(s)\subseteq\operatorname{\mathsf{supp}}(r)\cup\\{a\\}$
and $(i,\overline{r})\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}b\leavevmode\nobreak\ }(j,\overline{s})$ in $A$ for some
$b\mathbin{\\#}s$ and some $\overline{r},\overline{s}$ extending $r,(a\,b)s$.

######  Theorem 5.3.

For every Büchi RNNA $A$, the literal $\omega$-language of $\widetilde{A}$ is
the closure of that of $A$ under $\alpha$-equivalence.

######  Proof 5.4 (Proof sketch).

  1. 1.

One first verifies that the literal $\omega$-language of $\widetilde{A}$ is
closed under $\alpha$-equivalence. To this end, one proves more generally that
given $\alpha$-equivalent infinite bar strings
$w=\sigma_{1}\sigma_{2}\sigma_{3}\cdots$ and
$w^{\prime}=\sigma_{1}^{\prime}\sigma_{2}^{\prime}\sigma_{3}^{\prime}\cdots$
and a run

$(i_{0},r_{0})\xrightarrow{\leavevmode\nobreak\ \sigma_{1}\leavevmode\nobreak\
}(i_{1},r_{1})\xrightarrow{\leavevmode\nobreak\ \sigma_{2}\leavevmode\nobreak\
}(i_{2},r_{2})\xrightarrow{\leavevmode\nobreak\ \sigma_{3}\leavevmode\nobreak\
}\cdots$

for $w$ in $\widetilde{A}$ there exists a run of the form

$(i_{0},r_{0}^{\prime})\xrightarrow{\leavevmode\nobreak\
\sigma_{1}^{\prime}\leavevmode\nobreak\
}(i_{1},r_{1}^{\prime})\xrightarrow{\leavevmode\nobreak\
\sigma_{2}^{\prime}\leavevmode\nobreak\
}(i_{2},r_{2}^{\prime})\xrightarrow{\leavevmode\nobreak\
\sigma_{3}^{\prime}\leavevmode\nobreak\ }\cdots.$

for $w^{\prime}$ in $\widetilde{A}$. In particular, by definition of the final
states of $\widetilde{A}$, the first run is accepting iff the second one is.
Similar to the proof of 4.3, one first establishes the corresponding statement
for finite runs by induction on their length, and then extends to the infinite
case via Kőnig’s lemma.

  2. 2.

In view of part 1 it remains to prove that $A$ and $\widetilde{A}$ accept the
same bar $\omega$-language. Again, this follows from a more general
observation: for every infinite run

$(i_{0},r_{0})\xrightarrow{\leavevmode\nobreak\ \sigma_{1}\leavevmode\nobreak\
}(i_{1},r_{1})\xrightarrow{\leavevmode\nobreak\ \sigma_{2}\leavevmode\nobreak\
}(i_{2},r_{2})\xrightarrow{\leavevmode\nobreak\ \sigma_{3}\leavevmode\nobreak\
}\cdots$

in $A$ there exists an infinite run of the form

$(i_{0},r_{0}^{\prime})\xrightarrow{\leavevmode\nobreak\
\sigma_{1}^{\prime}\leavevmode\nobreak\
}(i_{1},r_{1}^{\prime})\xrightarrow{\leavevmode\nobreak\
\sigma_{2}^{\prime}\leavevmode\nobreak\
}(i_{2},r_{2}^{\prime})\xrightarrow{\leavevmode\nobreak\
\sigma_{3}^{\prime}\leavevmode\nobreak\ }\cdots$

in $\widetilde{A}$ such that
$\sigma_{1}^{\prime}\sigma_{2}^{\prime}\sigma_{3}^{\prime}\cdots=_{\alpha}\sigma_{1}\sigma_{2}\sigma_{3}\cdots$.
Moreover, the symmetric statement holds where the roles of $A$ and
$\widetilde{A}$ are swapped. As before, one first shows the corresponding
statement for finite bar strings and then invokes Kőnig’s lemma.

##  6 Decidability of Inclusion

With the preparations given in the previous sections, we arrive at our main
result: language inclusion of Büchi RNNA is decidable, both under bar language
semantics and data language semantics. The main ingredients of our proofs
below are the name-dropping modification (Theorem 5.3) and the name
restriction property stated in 4.3. We will employ them to show that the
language inclusion problems for Büchi RNNA reduce to the inclusion problem for
ordinary Büchi automata over finite alphabets. The latter is well-known to be
decidable with elementary complexity; in fact, it is
$\mathrm{PSPACE}$-complete [18].

######  Remark 7.

For algorithms deciding properties of Büchi RNNAs, a finite representation of
the underlying nominal sets of states and transitions is required. A standard
representation of a single orbit $X$ is given by picking an arbitrary element
$x\in X$ with $\operatorname{\mathsf{supp}}(x)=\\{a_{1},\ldots,a_{m}\\}$ and
forming the subgroup $G_{X}\subseteq\mathsf{Perm}(\\{a_{1},\ldots,a_{m}\\})$
of all permutations
$\pi\colon\\{a_{1},\ldots,a_{m}\\}\to\\{a_{1},\ldots,a_{m}\\}$ such that
$\pi\cdot x=x$. The finite group $G_{X}$ determines $X$ up to isomorphism [25,
Thm. 5.13]. More generally, an orbit-finite nominal set consisting of the
orbits $X_{1},\ldots,X_{n}$ is represented by a list of $n$ finite permutation
groups $G_{X_{1}},\ldots,G_{X_{n}}$.

We first consider the bar language semantics:

######  Theorem 6.1.

Bar $\omega$-language inclusion of Büchi RNNAs is decidable in parametrized
polynomial space.

######  Proof 6.2.

Let $A$ and $B$ be Büchi RNNAs; the task is to decide whether
$L_{\alpha,\omega}(A)\subseteq L_{\alpha,\omega}(B)$. Put $m=\mathsf{deg}(A)$,
and choose a set $S\subseteq\mathbb{A}$ of $m+1$ distinct names containing
$\operatorname{\mathsf{supp}}(q_{0})$, where $q_{0}$ is the initial state of
$A$. Moreover, form the finite alphabet $\overline{S}=S\cup\\{{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}s:s\in S\\}.$

  1. 1.

We claim that

$L_{\alpha,\omega}(A)\subseteq L_{\alpha,\omega}(B)\qquad\text{iff}\qquad
L_{0,\omega}(A)\cap\overline{S}^{\omega}\subseteq
L_{0,\omega}(\widetilde{B})\cap\overline{S}^{\omega},$ (6.1)

where $\widetilde{B}$ is the name-dropping modification of $B$.

($\Rightarrow$) Suppose that $L_{\alpha,w}(A)\subseteq L_{\alpha,\omega}(B)$.
Then $L_{0,\omega}(A)\subseteq L_{0,\omega}(\widetilde{B})$ because
$L_{0,\omega}(\widetilde{B})$ is the closure of $L_{0,\omega}(B)$ under
$\alpha$-equivalence by Theorem 5.3. In particular,
$L_{0,\omega}(A)\cap\overline{S}^{\omega}\subseteq
L_{0,\omega}(\widetilde{B})\cap\overline{S}^{\omega}$.

($\Leftarrow$) Suppose that $L_{0,\omega}(A)\cap\overline{S}^{\omega}\subseteq
L_{0,\omega}(\widetilde{B})\cap\overline{S}^{\omega}$, and let
$[w]_{\alpha}\in L_{\alpha,\omega}(A)$. Thus, $w=_{\alpha}v$ for some $v\in
L_{0,\omega}(A)$. By 4.3 we know that there exists
$v^{\prime}\in\overline{S}^{\omega}$ accepted by $A$ such that
$v^{\prime}=_{\alpha}v$. Then

$v^{\prime}\in L_{0,\omega}(A)\cap\overline{S}^{\omega}\subseteq
L_{0,\omega}(\widetilde{B})\cap\overline{S}^{\omega}\subseteq
L_{0,\omega}(\widetilde{B}).$

Thus $[w]_{\alpha}=[v]_{\alpha}=[v^{\prime}]_{\alpha}\in
L_{\alpha,\omega}(\widetilde{B})=L_{\alpha,\omega}(B)$, proving
$L_{\alpha,\omega}(A)\subseteq L_{\alpha,\omega}(B)$.

  2. 2.

Now observe that both $L_{0,\omega}(A)\cap\overline{S}^{\omega}$ and
$L_{0,\omega}(\widetilde{B})\cap\overline{S}^{\omega}$ are $\omega$-regular
languages over the alphabet $\overline{S}$: they are accepted by the Büchi
automata obtained by restricting the Büchi RNNAs $A$ and $B$, respectively, to
the finite set of states with support contained in $S$ and transitions labeled
by elements of $\overline{S}$. Inclusion of $\omega$-regular languages is
decidable in polynomial space [18]. Let $k_{A}/k_{B}$ and $m_{A}/m_{B}$ denote
the number of orbits and the degree of $A$/$B$. Since the support of every
state of the Büchi automaton derived from $A$ is contained in the set $S$ and
the latter has $(m_{A}+1)!$ permutations, there are at most

$k_{A}\cdot(m_{A}+1)!\in\mathcal{O}(k_{A}\cdot 2^{(m_{A}+1)\log(m_{A}+1)})$

states. The Büchi automaton derived from $\widetilde{B}$ has at most

$k_{B}\cdot 2^{m_{B}}\cdot(m_{A}+1)!\in\mathcal{O}(k_{B}\cdot
2^{m_{B}+(m_{A}+1)\log(m_{A}+1)})$

states since $\widetilde{B}$ has at most $k_{B}\cdot 2^{m_{B}}$ orbits. Thus,
the space required for the inclusion check is polynomial in $k_{A},k_{B}$ and
exponential in $m_{B}+(m_{A}+1)\log(m_{A}+1)$.

Next, we turn to the data language semantics.

######  Notation 6.3.

Given infinite bar strings $w=\sigma_{1}\sigma_{2}\sigma_{3}\cdots$ and
$w^{\prime}=\sigma_{1}^{\prime}\sigma_{2}^{\prime}\sigma_{3}^{\prime}\cdots$
we write $w\sqsubseteq w^{\prime}$ if, for all $a\in\mathbb{A}$ and
$n\in{\mathbb{N}}$,

$\sigma_{n}=a\quad\text{implies}\quad\sigma_{n}^{\prime}\in\\{a,{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a\\}\qquad\text{and}\qquad\sigma_{n}={\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a\quad\text{implies}\quad\sigma_{n}^{\prime}={\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a.$

Thus, $w^{\prime}$ arises from $w$ by arbitrarily putting bars in front of
letters in $w$.

######  Lemma 6.4.

If $v=_{\alpha}w$ and $v\sqsubseteq v^{\prime}$, then there exists
$w^{\prime}\in\overline{\mathbb{A}}^{\omega}$ such that $w\sqsubseteq
w^{\prime}$ and $v^{\prime}=_{\alpha}w^{\prime}$.

######  Proof 6.5.

Let
$v^{\prime}=\sigma_{1}^{\prime}\sigma_{2}^{\prime}\sigma_{3}^{\prime}\cdots$
and $w=\rho_{1}\rho_{2}\rho_{3}\cdots$. We define $w^{\prime}$ to be the
following modification of $w$: for every $n\in{\mathbb{N}}$, if $\rho_{n}=a$
and $\sigma_{n}^{\prime}={\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}b$ for some
$a,b\in\mathbb{A}$, replace $\rho_{n}$ by ${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$. Then
$w\sqsubseteq w^{\prime}$ and $v^{\prime}=_{\alpha}w^{\prime}$ as required.

In the following, we write $D(w)$ for $D(\\{[w]_{\alpha}\\})$; thus, $D(w)$ is
the set of all $\mathsf{ub}(v)\in\mathbb{A}^{\omega}$ where $v=_{\alpha}w$
(cf. Section 3).

######  Lemma 6.6.

Let $L$ be a bar $\omega$-language accepted by some Büchi RNNA and let
$w\in\overline{\mathbb{A}}^{\omega}_{\mathsf{fs}}$. Then $D(w)\subseteq D(L)$
if and only if there exists $w^{\prime}\sqsupseteq w$ such that
$[w^{\prime}]_{\alpha}\in L$.

######  Corollary 6.7.

Let $K$ and $L$ be bar $\omega$-languages accepted by Büchi RNNA. Then
$D(K)\subseteq D(L)$ if and only if for every
$w\in\overline{\mathbb{A}}^{\omega}_{\mathsf{fs}}$ with $[w]_{\alpha}\in K$
there exists $w^{\prime}\sqsupseteq w$ such that $[w^{\prime}]_{\alpha}\in L$.

######  Proof 6.8.

This follows from 6.6 using that $D(K)=\bigcup_{[w]_{\alpha}\in K}D(w)$ and
that every $\alpha$-equivalence class $[w]_{\alpha}\in K$ has a finitely
supported representative by 4.3.

######  Theorem 6.9.

Data $\omega$-language inclusion of Büchi RNNAs is decidable in parametrized
polynomial space.

######  Proof 6.10.

Let $A$ and $B$ be Büchi RNNAs; the task is to decide whether
$D_{\omega}(A)\subseteq D_{\omega}(B)$. Put $m=\mathsf{deg}(A)$, and choose a
set $S\subseteq\mathbb{A}$ of $m+1$ distinct names containing
$\operatorname{\mathsf{supp}}(q_{0})$, where $q_{0}$ is the initial state of
$A$. Moreover, form the finite alphabet $\overline{S}=S\cup\\{{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}s:s\in S\\}.$

  1. 1.

For every language $L\subseteq\overline{S}^{\omega}$ let $L{\downarrow}$
denote the downward closure of $L$ with respect to $\sqsubseteq$:

$L{\downarrow}=\\{v\in\overline{S}^{\omega}:\text{there exists $w\in L$ such
that }v\sqsubseteq w\\}.$

Every Büchi automaton accepting $L$ can be turned into a Büchi automaton
accepting $L{\downarrow}$ by adding the transition
$q\xrightarrow{\leavevmode\nobreak\ a\leavevmode\nobreak\ }q^{\prime}$ for
every transition $q\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }q^{\prime}$ where $a\in S$.

  2. 2.

We claim that

$D_{\omega}(A)\subseteq D_{\omega}(B)\qquad\text{iff}\qquad
L_{0,\omega}(A)\cap\overline{S}^{\omega}\subseteq(L_{0,\omega}(\widetilde{B})\cap\overline{S}^{\omega}){\downarrow},$
(6.2)

where $\widetilde{B}$ is the name-dropping modification of $B$.

($\Rightarrow$) Suppose that $D_{\omega}(A)\subseteq D_{\omega}(B)$, that is
$D(L_{\alpha,w}(A))\subseteq D(L_{\alpha,\omega}(B))$, and let $w\in
L_{0,\omega}(A)\cap\overline{S}^{\omega}$. Then $[w]_{\alpha}\in
L_{\alpha,\omega}(A)$, hence by 6.7 there exists $w^{\prime}\sqsupseteq w$
such that $[w^{\prime}]_{\alpha}\in L_{\alpha,\omega}(B)$. Then $w^{\prime}\in
L_{0,\omega}(\widetilde{B})\cap\overline{S}^{\omega}$ because
$L_{0,\omega}(\widetilde{B})$ is the closure of $L_{0,\omega}(B)$ under
$\alpha$-equivalence by Theorem 5.3. Thus
$w\in(L_{0,\omega}(\widetilde{B})\cap\overline{S}^{\omega}){\downarrow}$,
which proves
$L_{0,\omega}(A)\cap\overline{S}^{\omega}\subseteq(L_{0,\omega}(\widetilde{B})\cap\overline{S}^{\omega}){\downarrow}$.

($\Leftarrow$) Suppose that
$L_{0,\omega}(A)\cap\overline{S}^{\omega}\subseteq(L_{0,\omega}(\widetilde{B})\cap\overline{S}^{\omega}){\downarrow}$.
To prove $D_{\omega}(A)\subseteq D_{\omega}(B)$, that is
$D(L_{\alpha,\omega}(A))\subseteq D(L_{\alpha,\omega}(B))$, we use 6.7. Thus,
let $[w]_{\alpha}\in L_{\alpha,\omega}(A)$. Then $w=_{\alpha}v$ for some $v\in
L_{0,\omega}(A)$. By 4.3 we may assume that $v\in\overline{S}^{\omega}$. By
hypothesis this implies
$v\in(L_{0,\omega}(\widetilde{B})\cap\overline{S}^{\omega}){\downarrow}$, that
is, there exists $v^{\prime}\sqsupseteq v$ such that $v^{\prime}\in
L_{0,\omega}(\widetilde{B})$. By 6.4, there exists $w^{\prime}\sqsupseteq w$
such that $w^{\prime}=_{\alpha}v^{\prime}$. Then
$[w^{\prime}]_{\alpha}=[v^{\prime}]_{\alpha}\in
L_{\alpha,\omega}(\widetilde{B})=L_{\alpha,\omega}(B)$, as required.

  3. 3.

The decidability of $D_{\omega}(A)\subseteq D_{\omega}(B)$ now follows from
part 1 and (6.2) in complete analogy to the proof of Theorem 6.1.

######  Remark 8.

In the above theorem it is crucial to admit non-finitely supported data words:
it is an open problem whether the inclusion
$D_{\omega}(A)\cap\mathbb{A}^{\omega}_{\mathsf{fs}}\subseteq
D_{\omega}(B)\cap\mathbb{A}^{\omega}_{\mathsf{fs}}$ is decidable. In fact, our
decidability proof relies on 6.7 as a key ingredient, and the latter fails if
the condition $D(K)\subseteq D(L)$ is replaced by the weaker condition
$D(K)\cap\mathbb{A}^{\omega}_{\mathsf{fs}}\subseteq
D(L)\cap\mathbb{A}^{\omega}_{\mathsf{fs}}$.

To see this, let $K$ and $L$ be the bar $\omega$-languages accepted by the two
Büchi RNNAs displayed below, where $a,b$ range over names in $\mathbb{A}$ and
$a\neq b$:

$q_{0}$start${\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a$$q_{0}$start$a$$q_{f}$${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}b$$a$${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$

We have $D(K)=\mathbb{A}^{\omega}$ and $D(L)$ consists of all data words in
$\mathbb{A}^{\omega}$ in which some name occurs at least twice. Thus,
$D(K)\cap\mathbb{A}^{\omega}_{\mathsf{fs}}=D(L)\cap\mathbb{A}^{\omega}_{\mathsf{fs}}=\mathbb{A}^{\omega}_{\mathsf{fs}}$,
in particular the inclusion
$D(K)\cap\mathbb{A}^{\omega}_{\mathsf{fs}}\subseteq
D(L)\cap\mathbb{A}^{\omega}_{\mathsf{fs}}$ holds. Consider the infinite bar
string $w={\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a{\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a{\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a\cdots$ and note that $w^{\prime}\sqsupseteq w$ implies
$w^{\prime}=w$. Then $[w]_{\alpha}\in K$ but $[w]_{\alpha}\not\in L$ since
every bar string accepted by the right-hand automaton contains some letter
from $\mathbb{A}$. Thus, “only if” fails in 6.7.

##  7 Relation to Other Automata Models

We conclude this paper by comparing Büchi RNNA with two related automata
models over infinite words. Ciancia and Sammartino [5] consider deterministic
nominal automata accepting data $\omega$-languages
$L\subseteq\mathbb{A}^{\omega}$ via a Muller acceptance condition. More
precisely, a _nominal deterministic Muller automaton_ (nDMA)
$A=(Q,\delta,q_{0},\mathcal{F})$ is given by an orbit-finite nominal set $Q$
of states, and equivariant map $\delta\colon Q\times\mathbb{A}\to Q$
representing transitions, an initial state $q_{0}\in Q$, and a set
$\mathcal{F}\subseteq\mathcal{P}(\mathsf{orb}(Q))$ where $\mathsf{orb}(Q)$ is
the finite set of orbits of $Q$. Every input word
$w=a_{1}a_{2}a_{3}\cdots\in\mathbb{A}^{\omega}$ has a unique run
$q_{0}\xrightarrow{\leavevmode\nobreak\ a_{1}\leavevmode\nobreak\
}q_{1}\xrightarrow{\leavevmode\nobreak\ a_{2}\leavevmode\nobreak\
}q_{2}\xrightarrow{\leavevmode\nobreak\ a_{3}\leavevmode\nobreak\ }\cdots$
where $q_{i+1}=\delta(q_{i},a_{i+1})$ for $i=0,1,2,\ldots$. The word $w$ is
_accepted_ if the set $\\{O\in\mathsf{orb}(Q):\text{$q_{n}\in O$ for
infinitely many $n$}\\}$ lies in $\mathcal{F}$. The data $\omega$-language
_accepted_ by the automaton is the set of all words $w\in\mathbb{A}^{\omega}$
whose run is accepting.

As for Büchi RNNA, language inclusion is decidable for nDMA [5, Thm. 4]. In
terms of expressive power the two models are incomparable, as witnessed by the
data $\omega$-languages

$\displaystyle K$ $\displaystyle=\\{w\in\mathbb{A}^{\omega}:\text{some
$a\in\mathbb{A}$ occurs infinitely often in $w$}\\},$ $\displaystyle L$
$\displaystyle=\\{w\in\mathbb{A}^{\omega}:\text{$w$ does not have the suffix
$a^{\omega}$ for any $a\in\mathbb{A}$}\\}.$

######  Proposition 7.1.

  1. 1.

The language $K$ is accepted by a Büchi RNNA but not by any nDMA.

  2. 2.

The language $L$ is accepted by an nDMA but not by any Büchi RNNA.

######  Proof 7.2.

  1. 1.

We have seen in 4.1 that the language $K$ is accepted by a Büchi RNNA. We
claim that $K$ is not accepted by any nDMA. Since the class of languages
accepted by nDMA is closed under complement, it suffices to show that the
language

$\overline{K}=\\{w\in\mathbb{A}^{\omega}:\text{each $a\in\mathbb{A}$ occurs
only finitely often in $w$}\\}$

is not accepted by any nDMA. Suppose towards a contradiction that
$A=(Q,\delta,q_{0},\mathcal{F})$ is an nDMA accepting $\overline{K}$. Let $m$
be the maximum of all $|\operatorname{\mathsf{supp}}(q)|$ where $q\in Q$. Fix
$m+1$ pairwise distinct names $a_{1},\ldots,a_{m+1}\in\mathbb{A}$ and an
arbitrary word $w_{0}\in\overline{K}$.

Choose a factorization $w_{0}=v_{1}w_{1}$
($v_{1}\in\mathbb{A}^{*},w_{1}\in\mathbb{A}^{\omega})$ such that all
occurrences of $a_{1},\ldots,a_{m+1}$ in $w_{0}$ lie in the finite prefix
$v_{1}$. Let $q_{1}$ be the state reached from $q_{0}$ on input $v_{1}$. Then
$\operatorname{\mathsf{supp}}(q_{1})$ does not contain all of the names
$a_{1},\ldots,a_{m+1}$, say $a_{i}\mathbin{\\#}q_{1}$. Choose any name
$a\in\mathbb{A}$ occurring in $w_{1}$ such that $a\\#q_{1}$. Then
$q_{1}=(a\,a_{i})q_{1}$ accepts $(a\,a_{i})w_{1}$ since by equivariance the
run of $(a\,a_{i})w_{1}$ from $q_{1}$ visits the same orbits as the run of
$w_{1}$.

Now repeat the same process with $q_{1}$ and $(a\,a_{i})w_{1}$ in lieu of
$q_{0}$ and $w_{0}$, and let $(a\,a_{i})w_{1}=v_{2}w_{2}$ denote the
corresponding factorization; note that $v_{2}$ is nonempty because
$(a\,a_{i})w_{1}$ contains the name $a_{i}$. Continuing in this fashion yields
an infinite word $v=v_{1}v_{2}v_{3}\ldots$ such that each $v_{i}$ $(i>1)$
contains at least one of the letters $a_{1},\ldots,a_{m+1}$, and the run of
$v$ traverses the same orbits (in the same order) as the run of $w$. Thus $v$
is accepted by the nDMA $A$ although $v\not\in\overline{K}$, a contradiction.

  2. 2.

The language $L$ is accepted by the nDMA with states
$\\{q_{0}\\}\cup\mathbb{A}\times\\{0,1\\}$ and transitions as displayed below,
where $a,b$ range over distinct names in $\mathbb{A}$. The acceptance
condition is given by
$\mathcal{F}=\\{\\{\mathbb{A}\times\\{0\\},\mathbb{A}\times\\{1\\}\\}\\}$.

$q_{0}$start$(a,0)$$(b,1)$$a$$a$$b$$b$$a$

We claim that $L$ is not accepted by any Büchi RNNA. Suppose to the contrary
that $A=(Q,R,q_{0},F)$ is a Büchi RNNA with $D_{\omega}(A)=L$. By Theorem 5.3
we may assume that $L_{0,\omega}(A)$ is closed under $\alpha$-equivalence. Fix
an arbitrary word $w=a_{1}a_{2}a_{3}\cdots$ whose names are pairwise distinct
and not contained in $\operatorname{\mathsf{supp}}(q_{0})$. Then $w\in L$, so
there exists $v\in L_{0,\omega}(A)$ such that $\mathsf{ub}(v)=w$. We claim
that $v={\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a_{1}{\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a_{2}{\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a_{3}\cdots$. Indeed, if the $n$th letter of $v$ is $a_{n}$, then in
an accepting run for $v$ in $A$ the state $q$ reached before reading $a_{n}$
must have $a_{n}\in\operatorname{\mathsf{supp}}(q)$ by 4.2.3. But this is
impossible because
$\operatorname{\mathsf{supp}}(q)\subseteq\operatorname{\mathsf{supp}}(q_{0})\cup\\{a_{1},\ldots,a_{n-1}\\}$
again by 4.2.

Thus $v=_{\alpha}{\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a{\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a{\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a\cdots$. This implies $a^{\omega}\in D_{\omega}(A)$ although
$a^{\omega}\not\in L$, a contradiction.

Let us note that the above result does not originate in weakness of the Büchi
acceptance condition. One may generalize Büchi RNNA to _Muller RNNA_ where the
final states $F\subseteq Q$ are replaced by a set
$\mathcal{F}\subseteq\mathcal{P}(\mathsf{orb}(Q))$, and a bar string
$w\in\overline{\mathbb{A}}^{\omega}$ is said to be _accepted_ if there exists
a run for $w$ such that the set of orbits visited infinitely often lies in
$\mathcal{F}$. However, as for classical nondeterministic Büchi and Muller
automata, this does not affect expressivity:

######  Proposition 7.3.

A literal $\omega$-language is accepted by a Büchi RNNA if and only if it is
accepted by a Muller RNNA.

Finally, we mention a tight connection between Büchi RNNA and _session
automata_ [4]. The data ($\omega$-)language associated to a (Büchi) RNNA uses
a _local freshness_ semantics in the sense that its definition considers
possibly non-clean bar strings accepted by $A$. In some applications, e.g.
nonce generation, a more suitable semantics is given by _global freshness_
where only clean bar strings are admitted, i.e. one associates to $A$ the data
languages

$\displaystyle D_{\\#}(A)$
$\displaystyle=\\{\mathsf{ub}(w):\text{$w\in\overline{\mathbb{A}}^{*}$ clean
and $[w]_{\alpha}\in L_{\alpha}(A)$}\\},$ $\displaystyle D_{\omega,\\#}(A)$
$\displaystyle=\\{\mathsf{ub}(w):\text{$w\in\overline{\mathbb{A}}^{\omega}$
clean and $[w]_{\alpha}\in L_{\alpha,\omega}(A)$}\\}.$

For instance, for the Büchi RNNA $A$ from 4.1 the language $D_{\omega,\\#}(A)$
consists of all infinite words $w\in\mathbb{A}^{\omega}$ where exactly one
name $a\in\mathbb{A}$ occurs infinitely often and every name $b\neq a$ occurs
at most once.

Under global freshness semantics, it has been observed in previous work [26]
that a data language $L\subseteq\mathbb{A}^{*}$ is accepted by some session
automaton iff $L=D_{\\#}(A)$ for some RNNA $A$ whose initial state $q_{0}$ has
empty support. An analogous correspondence holds for Büchi RNNA and data
$\omega$-languages $L\subseteq\mathbb{A}^{\omega}$ if the original notion of
session automata is generalized to infinite words with a Büchi acceptance
condition.

##  8 Conclusions and Future Work

We have introduced _Büchi regular nondeterministic nominal automata_ (Büchi
RNNAs), an automaton model for languages of infinite words over infinite
alphabets. Büchi RNNAs allow for inclusion checking in elementary complexity
(parametrized polynomial space) despite the fact that they feature full
nondeterminism and do not restrict the number of registers (contrastingly,
even for register automata over finite words [16], inclusion checking becomes
decidable only if the number of registers is bounded to at most $2$).

An important further step will be to establish a logic-automata correspondence
of Büchi RNNAs with a suitable form of linear temporal logic on infinite data
words.

A natural direction for generalization is to investigate RNNAs over infinite
trees with binders, modeled as coalgebras of type
$\mathcal{P}_{\mathsf{ufs}}F$ for a functor $F$ associated to a binding
signature and equipped with the ensuing notion of $\alpha$-equivalence due to
Kurz et al. [20].

Finally, we would like to explore the bar language and data language semantics
of Büchi RNNA from the perspective of coalgebraic trace semantics [29], where
infinite behaviours emerge as solutions of (nested) fixed point equations in
Kleisli categories.

## References

  * [1] Hendrik Pieter Barendregt.  The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics.  North-Holland, 1985.
  * [2] Mikołaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin.  Two-variable logic on data words.  ACM Trans. Comput. Log., 12(4):27:1–27:26, 2011.  doi:10.1145/1970398.1970403.
  * [3] Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota.  Automata theory in nominal sets.  Log. Methods Comput. Sci., 10(3), 2014.  doi:10.2168/LMCS-10(3:4)2014.
  * [4] Benedikt Bollig, Peter Habermehl, Martin Leucker, and Benjamin Monmege.  A robust class of data languages and an application to learning.  Log. Meth. Comput. Sci., 10(4), 2014.  doi:10.2168/LMCS-10(4:19)2014.
  * [5] Vincenzo Ciancia and Matteo Sammartino.  A class of automata for the verification of infinite, resource-allocating behaviours.  In Trustworthy Global Computing, TGC 2014, volume 8902 of LNCS, pages 97–111. Springer, 2014.  doi:10.1007/978-3-662-45917-1_7.
  * [6] Thomas Colcombet and Amaldev Manuel.  Generalized data automata and fixpoint logic.  In Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, volume 29 of LIPIcs, pages 267–278. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2014.  doi:10.4230/LIPIcs.FSTTCS.2014.267.
  * [7] Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, and Filip Mazowiecki.  The reachability problem for Petri nets is not elementary.  J. ACM, 68(1):7:1–7:28, 2021.  doi:10.1145/3422822.
  * [8] Wojciech Czerwiński and Lukasz Orlikowski.  Reachability in vector addition systems is Ackermann-complete.  CoRR, 2021.  arXiv:2104.13866.
  * [9] Stéphane Demri and Ranko Lazić.  LTL with the freeze quantifier and register automata.  ACM Trans. Comput. Log., 10(3):16:1–16:30, 2009.  doi:10.1145/1507244.1507246.
  * [10] Murdoch J. Gabbay.  Foundations of nominal techniques: logic and semantics of variables in abstract syntax.  Bull. Symb. Log., 17(2):161–229, 2011.  doi:10.2178/bsl/1305810911.
  * [11] Murdoch J. Gabbay and Vincenzo Ciancia.  Freshness and name-restriction in sets of traces with names.  In Foundations of Software Science and Computation Structures, FOSSACS 2011, volume 6604 of LNCS, pages 365–380. Springer, 2011.  doi:10.1007/978-3-642-19805-2.
  * [12] Murdoch J. Gabbay and Andrew M. Pitts.  A new approach to abstract syntax involving binders.  In Logic in Computer Science, LICS 1999, pages 214–224. IEEE Computer Society, 1999.  doi:10.1109/LICS.1999.782617.
  * [13] Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors.  Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of LNCS. Springer, 2002.  doi:10.1007/3-540-36387-4.
  * [14] Radu Grigore, Dino Distefano, Rasmus Petersen, and Nikos Tzevelekos.  Runtime verification based on register automata.  In Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2013, volume 7795 of LNCS, pages 260–276. Springer, 2013\.  doi:10.1007/978-3-642-36742-7_19.
  * [15] Orna Grumberg, Orna Kupferman, and Sarai Sheinvald.  Variable automata over infinite alphabets.  In Language and Automata Theory and Applications, LATA 2010, volume 6031 of LNCS, pages 561–572. Springer, 2010.  doi:10.1007/978-3-642-13089-2.
  * [16] Michael Kaminski and Nissim Francez.  Finite-memory automata.  Theor. Comput. Sci., 134(2):329–363, 1994.  doi:10.1016/0304-3975(94)90242-9.
  * [17] Ahmet Kara, Thomas Schwentick, and Tony Tan.  Feasible automata for two-variable logic with successor on data words.  In Language and Automata Theory and Applications, LATA 2012, volume 7183 of LNCS, pages 351–362. Springer, 2012.  doi:10.1007/978-3-642-28332-1_30.
  * [18] Orna Kupferman and Moshe Y. Vardi.  Verification of fair transisiton systems.  In Computer Aided Verification, CAV 1996, volume 1102 of LNCS, pages 372–382. Springer, 1996.  doi:10.1007/3-540-61474-5_84.
  * [19] Klaas Kürtz, Ralf Küsters, and Thomas Wilke.  Selecting theories and nonce generation for recursive protocols.  In Formal methods in security engineering, FMSE 2007, pages 61–70. ACM, 2007.  doi:10.1145/1314436.1314445.
  * [20] Alexander Kurz, Daniela Petrisan, Paula Severi, and Fer-Jan de Vries.  Nominal coalgebraic data types with applications to lambda calculus.  Log. Methods Comput. Sci., 9(4), 2013.  doi:10.2168/LMCS-9(4:20)2013.
  * [21] Ranko Lazić.  Safely freezing LTL.  In Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2006, volume 4337 of LNCS, pages 381–392. Springer, 2006\.  doi:10.1007/11944836_35.
  * [22] Jérôme Leroux.  The reachability problem for Petri nets is not primitive recursive.  CoRR, 2021.  arXiv:2104.12695.
  * [23] Stefan Milius and Henning Urbat.  Equational axiomatization of algebras with structure.  In Foundations of Software Science and Computation Structures, FOSSACS 2019, volume 11425 of LNCS, pages 400–417. Springer, 2019.  Full version available at https://arxiv.org/abs/1812.02016.  doi:10.1007/978-3-030-17127-8_23.
  * [24] Daniela Petrişan.  Investigations into Algebra and Topology over Nominal Sets.  PhD thesis, University of Leicester, 2011.
  * [25] Andrew Pitts.  Nominal Sets: Names and Symmetry in Computer Science.  Cambridge University Press, 2013.
  * [26] Lutz Schröder, Dexter Kozen, Stefan Milius, and Thorsten Wißmann.  Nominal automata with name binding.  In Foundations of Software Science and Computation Structures, FOSSACS 2017, volume 10203 of LNCS, pages 124–142, 2017.  doi:10.1007/978-3-662-54458-7_8.
  * [27] Christoph Stockhusen and Till Tantau.  Completeness results for parameterized space classes.  In Parameterized and Exact Computation, IPEC 2013, volume 8246 of LNCS, pages 335–347. Springer, 2013.  doi:10.1007/978-3-319-03898-8.
  * [28] Nikos Tzevelekos.  Nominal Game Semantics.  PhD thesis, University of Oxford, 2008.
  * [29] Natsuki Urabe, Shunsuke Shimizu, and Ichiro Hasuo.  Coalgebraic trace semantics for buechi and parity automata.  In Concurrency Theory, CONCUR 2016, volume 59 of LIPIcs, pages 24:1–24:15. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2016.  doi:10.4230/LIPIcs.CONCUR.2016.24.

## Appendix: Omitted Proofs

This appendix provides all proofs omitted for space reasons.

##  Appendix A Details for Section 3

## Proof of 3.4

The functor $F=\mathbb{A}\times(\mathop{-})+[\mathbb{A}](\mathop{-})$
preserves limits of $\omega^{\mathsf{op}}$-chains since such limits commute
with $\times$ and $+$ (like in $\mathsf{Set}$) and the functor
$[\mathbb{A}](\mathop{-})$ is a right adjoint [25, Thm. 4.12], i.e. preserves
all limits. Therefore, the final coalgebra $\nu F$ arises as the limit of the
final $\omega^{\mathsf{op}}$-chain of $F$:

$\nu F=\lim_{n\in{\mathbb{N}}}F^{n}1.$

We prove by induction that

$F^{n}1\cong\overline{\mathbb{A}}^{n}/{=_{\alpha}}\qquad\text{for every
$n\in{\mathbb{N}}$},$

where $=_{\alpha}$ is $\alpha$-equivalence restricted to bar strings of length
$n$. The claim is obvious for $n=0$. For the induction step $n\to n+1$ we
compute

$F^{n+1}1=F(F^{n}1)\cong
F(\overline{\mathbb{A}}^{n}/{=_{\alpha}})=\mathbb{A}\times(\overline{\mathbb{A}}^{n}/{=_{\alpha}})+[\mathbb{A}](\overline{\mathbb{A}}^{n}/{=_{\alpha}})\cong\overline{\mathbb{A}}^{n+1}/{=_{\alpha}}.$

Here, the first isomorphism uses the induction hypothesis and the second one
is given by

$(a,[w]_{\alpha})\mapsto[aw]_{\alpha}\qquad\text{and}\qquad\langle
a\rangle[w]_{\alpha}\mapsto[{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}aw]_{\alpha}\qquad\text{for $a\in\mathbb{A}$ and
$w\in\overline{\mathbb{A}}^{n}$.}$

This is clearly well-defined according to the definition of
$\alpha$-equivalence for finite words.

Finally, we observe that the canonical map $e_{\alpha,n}\colon\nu G\to
F^{n}1\cong\overline{\mathbb{A}}^{n}/{=_{\alpha}}$ sends
$w\in\overline{\mathbb{A}}^{\omega}_{\mathsf{fs}}$ to the $\alpha$-equivalence
class of $w_{n}$ Since $e_{\alpha}$ merges two words iff each $e_{\alpha,n}$
does, we are done.

##  Appendix B Details for Section 4

## Details for 4.3

Put $m:=\mathsf{deg}(A)$.

  1. 1.

Two finite runs

$r_{0}\xrightarrow{\leavevmode\nobreak\ \sigma_{1}\leavevmode\nobreak\
}r_{1}\xrightarrow{\leavevmode\nobreak\ \sigma_{2}\leavevmode\nobreak\
}r_{2}\xrightarrow{\leavevmode\nobreak\ \sigma_{3}\leavevmode\nobreak\
}\cdots\xrightarrow{\leavevmode\nobreak\ \sigma_{n}\leavevmode\nobreak\
}r_{n}\quad\text{and}\quad r_{0}^{\prime}\xrightarrow{\leavevmode\nobreak\
\sigma_{1}^{\prime}\leavevmode\nobreak\
}r_{1}^{\prime}\xrightarrow{\leavevmode\nobreak\
\sigma_{2}^{\prime}\leavevmode\nobreak\
}r_{2}^{\prime}\xrightarrow{\leavevmode\nobreak\
\sigma_{3}^{\prime}\leavevmode\nobreak\
}\cdots\xrightarrow{\leavevmode\nobreak\
\sigma_{n}^{\prime}\leavevmode\nobreak\ }r_{n}^{\prime}$

in $A$ of the same length are called _equivalent_ if for each $i=0,\ldots,n$
the states $r_{i}$ and $r_{i}^{\prime}$ lie in the same orbit. We claim that

($\ast$) For every $q\in Q$ and $w\in\overline{\mathbb{A}}^{*}$, if there
exists a run of $w$ starting in $q$ then there exists an equivalent run
starting in $q$ whose label $w^{\prime}\in\overline{\mathbb{A}}^{*}$ satisfies

$w^{\prime}=_{\alpha}w\qquad\text{and}\qquad|\operatorname{\mathsf{supp}}(q)\cup\mathsf{N}(w^{\prime})|\leq\mathsf{deg}(A)+1.$

The proof of ($\ast$) is by induction on the length of $w$. The base case
$w=\varepsilon$ is obvious.

For the induction step, suppose $w=\sigma v$ where
$\sigma\in\overline{\mathbb{A}}$ and $v\in\overline{\mathbb{A}}^{*}$, and let
$q\xrightarrow{\leavevmode\nobreak\ \sigma\leavevmode\nobreak\ }r$ be the
first transition of a run of $w$ from $q$. Then $v$ has a run from $r$, so by
induction there exists $v^{\prime}\in\overline{\mathbb{A}}^{*}$ with an
equivalent run from $r$ such that $v^{\prime}=_{\alpha}v$ and
$|\operatorname{\mathsf{supp}}(r)\cup\mathsf{N}(v^{\prime})|\leq m+1$. Choose
$m+1$ pairwise distinct names $a_{1},\ldots,a_{m+1}$ such that

$\operatorname{\mathsf{supp}}(r)\cup\mathsf{N}(v^{\prime})\subseteq\\{a_{1},\ldots,a_{m+1}\\}.$

We have $\sigma=a$ or $\sigma={\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$ for some
$a\in\mathbb{A}$ and consider the two cases separately:

Case 1: $\sigma=a$. Choose $m+1$ pairwise distinct names
$b_{1},\ldots,b_{m+1}$ such that

$\operatorname{\mathsf{supp}}(q)\subseteq\\{b_{1},\ldots,b_{m+1}\\},$

Since $q\xrightarrow{\leavevmode\nobreak\ a\leavevmode\nobreak\ }r$ we have
$\operatorname{\mathsf{supp}}(r)\subseteq\operatorname{\mathsf{supp}}(q)$ by
4.2.1. Extend the inclusion map
$\operatorname{\mathsf{supp}}(r)\hookrightarrow\operatorname{\mathsf{supp}}(q)$
to a bijection
$\pi\colon\\{a_{1},\ldots,a_{m+1}\\}\to\\{b_{1},\ldots,b_{m+1}\\}$. Then
$\pi\cdot v^{\prime}$ has a run from $\pi\cdot r=r$ by equivariance, and
$\pi\cdot v^{\prime}=_{\alpha}v^{\prime}$ because $\pi$ fixes all free names
of $v^{\prime}$ (which are contained in $\operatorname{\mathsf{supp}}(r)$ by
4.2.3). Put

$w^{\prime}:=a(\pi\cdot v^{\prime}).$

Then $w^{\prime}$ has a run from $q$ equivalent to the given run of $w$:
compose the transition $q\xrightarrow{\leavevmode\nobreak\
a\leavevmode\nobreak\ }r$ with the above run of $\pi\cdot v^{\prime}$ from
$r$. Moreover

$w^{\prime}=_{\alpha}av^{\prime}=_{\alpha}av=w$

and

$\operatorname{\mathsf{supp}}(q)\cup\mathsf{N}(w^{\prime})=\operatorname{\mathsf{supp}}(q)\cup\mathsf{N}(\pi\cdot
v^{\prime})\cup\\{a\\}\subseteq\\{b_{1},\ldots,b_{m+1}\\}$

using that $a\in\operatorname{\mathsf{supp}}(q)$ because
$q\xrightarrow{\leavevmode\nobreak\ a\leavevmode\nobreak\ }r$.

Case 2: $\sigma={\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a$. If $a\in\\{a_{1},\ldots,a_{m+1}\\}$ one can choose
$w^{\prime}:={\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}av^{\prime}$: composing the transition
$q\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }r$ with the given run of $v^{\prime}$ from
$r$ yields a run of $w^{\prime}$ with the required properties. Thus suppose
$a\not\in\\{a_{1},\ldots,a_{m+1}\\}$. Then $a\mathbin{\\#}r$ because
$\operatorname{\mathsf{supp}}(r)\subseteq\\{a_{1},\ldots,a_{m+1}\\}$.
Moreover, $a_{i}\mathbin{\\#}r$ for some $i$ because
$|\operatorname{\mathsf{supp}}(r)|\leq m$. We claim that the bar string

$w^{\prime}:={\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a_{i}v^{\prime}$

has the required properties. Indeed, we have the transition
$q\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a_{i}\leavevmode\nobreak\ }r$ in $A$ by $\alpha$-invariance because
$q\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }r$ and $\langle a\rangle r=\langle
a_{i}\rangle r$. Composing this transition with the given run of $v^{\prime}$
from $r$ yields a run of $w^{\prime}$ from $q$ equivalent to the given run of
$w$. Finally, note that the names $a$ and $a_{i}$ are not free in $v^{\prime}$
because $\mathsf{FN}(v^{\prime})\subseteq\operatorname{\mathsf{supp}}(r)$ by
4.2.3, so $v^{\prime}=_{\alpha}(a\,a_{i})v^{\prime}$. This implies

$w^{\prime}={\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a_{i}v^{\prime}=_{\alpha}{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a(a\,a_{i})v^{\prime}=_{\alpha}{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}av^{\prime}=_{\alpha}{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}av=w.$

  2. 2.

We are ready to prove the proposition. Let
$w=\sigma_{1}\sigma_{2}\sigma_{3}\cdots$ and suppose that

$q_{0}\xrightarrow{\leavevmode\nobreak\ \sigma_{1}\leavevmode\nobreak\
}q_{1}\xrightarrow{\leavevmode\nobreak\ \sigma_{2}\leavevmode\nobreak\
}q_{2}\xrightarrow{\leavevmode\nobreak\ \sigma_{3}\leavevmode\nobreak\
}\cdots$

is an accepting run for $w$. Choose $m+1$ pairwise distinct names
$a_{1},\ldots,a_{m+1}$ such that
$\operatorname{\mathsf{supp}}(q_{0})\subseteq\\{a_{1},\ldots,a_{m+1}\\}$.
Consider the set of all partial runs

$q_{0}\xrightarrow{\leavevmode\nobreak\
\sigma_{1}^{\prime}\leavevmode\nobreak\
}q_{1}^{\prime}\xrightarrow{\leavevmode\nobreak\
\sigma_{2}^{\prime}\leavevmode\nobreak\
}q_{2}^{\prime}\xrightarrow{\leavevmode\nobreak\
\sigma_{3}^{\prime}\leavevmode\nobreak\
}\cdots\xrightarrow{\leavevmode\nobreak\
\sigma_{n}^{\prime}\leavevmode\nobreak\ }q_{n}^{\prime}$ (B.1)

where (1) $n\in{\mathbb{N}}$, (2) $q_{i}^{\prime}$ and $q_{i}$ lie in the same
orbit for $i=1,\ldots,n$, (3)
$\sigma_{1}^{\prime}\cdots\sigma_{n}^{\prime}=_{\alpha}\sigma_{1}\cdots\sigma_{n}$,
and (4)
$\mathsf{N}(\sigma_{1}^{\prime}\cdots\sigma_{n}^{\prime})\subseteq\\{a_{1},\ldots
a_{m+1}\\}$. This set organizes into a tree with the edge relation given by
extension of runs. Thus, the nodes of depth $n$ are exactly the runs (B.1). By
($\ast$) in part 1 of the proof, at least one such run exist for each
$n\in{\mathbb{N}}$, i.e. the tree is infinite. It is finitely branching
because
$\operatorname{\mathsf{supp}}(q_{i}^{\prime})\subseteq\\{a_{1},\ldots,a_{m+1}\\}$
for all $i$ by 4.2, i.e. there are only finitely many runs (B.1) for each $n$.
By Kőnig’s lemma, the tree contains an infinite path, which yields an infinite
run

$q_{0}\xrightarrow{\leavevmode\nobreak\
\sigma_{1}^{\prime}\leavevmode\nobreak\
}q_{1}^{\prime}\xrightarrow{\leavevmode\nobreak\
\sigma_{2}^{\prime}\leavevmode\nobreak\
}q_{2}^{\prime}\xrightarrow{\leavevmode\nobreak\
\sigma_{3}^{\prime}\leavevmode\nobreak\ }\cdots$

such that $q_{i}^{\prime}$ and $q_{i}$ lie in the same orbit for each $i$ and
$\sigma_{1}^{\prime}\cdots\sigma_{n}^{\prime}=_{\alpha}\sigma_{1}\cdots\sigma_{n}$
for each $n$. Thus, putting

$w^{\prime}=\sigma_{1}^{\prime}\sigma_{2}^{\prime}\sigma_{3}^{\prime}\cdots$

we see that $A$ accepts $w^{\prime}$. Moreover, $w^{\prime}=_{\alpha}w$ and
$\operatorname{\mathsf{supp}}(q_{0})\cup\mathsf{N}(w^{\prime})\subseteq\\{a_{1},\ldots,a_{m+1}\\}$.

##  Appendix C Details for Section 5

## Proof of 5.1

  1. 1.

Given a Büchi RNNA viewed as a coalgebra

$Q\xrightarrow{\leavevmode\nobreak\ \gamma\leavevmode\nobreak\
}2\times\mathcal{P}_{\mathsf{ufs}}(\mathbb{A}\times
Q)\times\mathcal{P}_{\mathsf{ufs}}([\mathbb{A}]Q),$

express the nominal set $Q$ of states as a
$\operatorname{\mathsf{supp}}$-nondecreasing quotient $e\colon
P\twoheadrightarrow Q$ of an orbit-finite strong nominal set $P$ using 5. Note
that the type functor
$F(\mathop{-})=2\times\mathcal{P}_{\mathsf{ufs}}(\mathbb{A}\times\mathop{-})\times\mathcal{P}_{\mathsf{ufs}}([\mathbb{A}](\mathop{-}))$
preserves $\operatorname{\mathsf{supp}}$-nondecreasing quotients because the
functors $\mathcal{P}_{\mathsf{ufs}}(\mathop{-}),\mathbb{A}\times\mathop{-}$
and $[\mathbb{A}](\mathop{-})$ do. Therefore, the right vertical arrow in the
diagram below is $\operatorname{\mathsf{supp}}$-nondecreasing, and
projectivity of $P$ yields an equivariant map $\beta$ making the diagram
commute.

${P}$${2\times\mathcal{P}_{\mathsf{ufs}}(\mathbb{A}\times
P)\times\mathcal{P}_{\mathsf{ufs}}([\mathbb{A}]P)}$${Q}$${2\times\mathcal{P}_{\mathsf{ufs}}(\mathbb{A}\times
Q)\times\mathcal{P}_{\mathsf{ufs}}([\mathbb{A}]Q)}$$\scriptstyle{e}$$\scriptstyle{\beta}$$\scriptstyle{2\times\mathcal{P}_{\mathsf{ufs}}(\mathbb{A}\times
e)\times\mathcal{P}_{\mathsf{ufs}}({[\mathbb{A}]}e)}$$\scriptstyle{\gamma}$
(C.1)

Thus $e$ is a coalgebra homomorphism from $(P,\beta)$ to $(Q,\gamma)$. The
latter implies that the following three properties hold for each $p\in P$ and
$\sigma\in\overline{\mathbb{A}}$:

    1. (1)

If $p\xrightarrow{\leavevmode\nobreak\ \sigma\leavevmode\nobreak\ }r$ in $P$
then $e(p)\xrightarrow{\leavevmode\nobreak\ \sigma\leavevmode\nobreak\ }e(r)$
in $Q$.

    2. (2)

If $e(p)\xrightarrow{\leavevmode\nobreak\ \sigma\leavevmode\nobreak\ }q$ in
$Q$ then there exists $r\in P$ such that $p\xrightarrow{\leavevmode\nobreak\
\sigma\leavevmode\nobreak\ }r$ in $P$ and $e(r)=q$.

    3. (3)

The state $p$ is final in $P$ iff $e(p)$ is final in $Q$.

Indeed, clearly commutativity of the left component of (C.1) yields (3), and
commutativity of the central component yields (1) and (2) for
$\sigma\in\mathbb{A}$. It remains to show that commutativity of the right
component yields (1) and (2) for $\sigma={\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a\in\overline{\mathbb{A}}$. Let

$\beta_{r}\colon
P\to\mathcal{P}_{\mathsf{ufs}}([\mathbb{A}]P)\qquad\text{and}\qquad\gamma_{r}\colon
Q\to\mathcal{P}_{\mathsf{ufs}}([\mathbb{A}]Q)$

denote the right components of $\beta$ and $\gamma$.

Ad (1). If $p\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }r$ in $P$ we have $\langle a\rangle
r\in\beta_{r}(p)$. Thus, $\langle a\rangle e(r)=[\mathbb{A}]e(\langle a\rangle
r)\in\gamma_{r}(e(p))$ by (C.1). This shows
$e(p)\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }e(r)$ in $Q$.

Ad (2). If $e(p)\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }q$ in $Q$ we have $\langle a\rangle
q\in\gamma_{r}(e(p))$. From (C.1) it follows that there exists
$b\in\mathbb{A}$ and $r\in P$ such that $\langle b\rangle r\in\beta_{r}(p)$
and $\langle a\rangle q=\langle b\rangle e(r)$. If $a=b$, this implies
$p\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }r$ in $P$ and $q=e(r)$, and we are done. If
$a\neq b$, we have $a\mathbin{\\#}e(r)$ because
$\operatorname{\mathsf{supp}}(q)\setminus\\{a\\}=\operatorname{\mathsf{supp}}(e(r))\setminus\\{b\\}$.
Since $e$ is $\operatorname{\mathsf{supp}}$-nondecreasing, this implies
$a\mathbin{\\#}r$. Therefore $\langle a\rangle(a\,b)r=\langle b\rangle
r\in\beta_{r}(p)$, i.e. $p\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }(a\,b)r$ in $P$. Moreover, we have $\langle
a\rangle q=\langle b\rangle e(r)=\langle a\rangle(a\,b)e(r)=\langle a\rangle
e((a\,b)r)$ and therefore $e((a\,b)r)=q$, as required.

  2. 2.

Choose $p_{0}\in P$ such that $e(p_{0})=q_{0}$. The coalgebra $(P,\beta)$ can
be viewed as a Büchi RNNA equipped with the initial state $p_{0}$. We claim
that the Büchi RNNAs $P$ and $Q$ accept the same literal ($\omega$-)language.
In fact, this is immediate from part 1: by (1) and (2) we see that for every
run

$p_{0}\xrightarrow{\leavevmode\nobreak\ \sigma_{1}\leavevmode\nobreak\
}p_{1}\xrightarrow{\leavevmode\nobreak\ \sigma_{2}\leavevmode\nobreak\
}p_{2}\xrightarrow{\leavevmode\nobreak\ \sigma_{3}\leavevmode\nobreak\
}\cdots$

in $P$ there exists a corresponding run

$q_{0}\xrightarrow{\leavevmode\nobreak\ \sigma_{1}\leavevmode\nobreak\
}q_{1}\xrightarrow{\leavevmode\nobreak\ \sigma_{2}\leavevmode\nobreak\
}q_{2}\xrightarrow{\leavevmode\nobreak\ \sigma_{3}\leavevmode\nobreak\
}\cdots$

in $Q$ with $e(p_{i})=q_{i}$ for all $i$, and vice versa. Moreover, by (3) the
first run above is accepting iff the second one is. This concludes the proof.

## Details for Theorem 5.3

######  Lemma C.1.

The automaton $\widetilde{A}$ is an RNNA.

######  Proof C.2.

  1. 1.

Transitions are equivariant: Let $\pi\in\mathsf{Perm}(\mathbb{A})$ and
$a\in\mathbb{A}$.

Suppose that $(i,r)\xrightarrow{\leavevmode\nobreak\ a\leavevmode\nobreak\
}(j,s)$ in $\widetilde{A}$. Then
$(i,\overline{r})\xrightarrow{\leavevmode\nobreak\ a\leavevmode\nobreak\
}(j,\overline{s})$ in $A$ for some $\overline{r},\overline{s}$ extending
$r,s$. By equivariance of transitions in $A$ we get
$(i,\pi\cdot\overline{r})\xrightarrow{\leavevmode\nobreak\
\pi(a)\leavevmode\nobreak\ }(j,\pi\cdot\overline{s})$ in $A$. Then
$\pi\cdot\overline{r},\pi\cdot\overline{s}$ extends $\pi\cdot{r},\pi\cdot s$
and moreover

$\operatorname{\mathsf{supp}}(\pi\cdot
s)\cup\\{\pi(a)\\}=\pi(\operatorname{\mathsf{supp}}(s)\cup\\{a\\})\subseteq\pi(\operatorname{\mathsf{supp}}(r))=\operatorname{\mathsf{supp}}(\pi\cdot
r).$

Thus $(i,\pi\cdot{r})\xrightarrow{\leavevmode\nobreak\
\pi(a)\leavevmode\nobreak\ }(j,\pi\cdot{s})$ in $\widetilde{A}$.

Similarly, if $(i,r)\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }(j,s)$ in $\widetilde{A}$ we have
$(i,\overline{r})\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}b\leavevmode\nobreak\ }(j,\overline{s})$ in $A$ for some
$b\mathbin{\\#}s$ and $\overline{r},\overline{s}$ extending $r,(a\,b)s$. By
equivariance of transitions in $A$ it follows that

$(i,\pi\cdot\overline{r})\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}\pi(b)\leavevmode\nobreak\ }(j,\pi\cdot\overline{s})\qquad\text{in
$A$.}$

Then $\pi(b)\mathbin{\\#}\pi\cdot s$ and
$\pi\cdot\overline{r},\pi\cdot\overline{s}$ extends
$\pi\cdot{r},(\pi(a)\,\pi(b))\pi\cdot s$. Moreover

$\operatorname{\mathsf{supp}}(\pi\cdot
s)=\pi(\operatorname{\mathsf{supp}}(s))\subseteq\pi(\operatorname{\mathsf{supp}}(r)\cup\\{a\\})=\operatorname{\mathsf{supp}}(\pi\cdot
r)\cup\\{\pi(a)\\},$

and so we conclude $(i,\pi\cdot{r})\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}\pi(a)\leavevmode\nobreak\ }(j,\pi\cdot{s})$ in $\widetilde{A}$.

  2. 2.

Transitions are $\alpha$-invariant: Suppose that
$(i,r)\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }(j,s)$ in $\widetilde{A}$ and $\langle
a\rangle(j,s)=\langle a^{\prime}\rangle(j,s^{\prime})$ for some
$a^{\prime}\neq a$ and some $s^{\prime}$. The former means that
$(i,\overline{r})\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}b\leavevmode\nobreak\ }(j,\overline{s})$ in $A$ for some
$b\mathbin{\\#}s$ and some $\overline{r},\overline{s}$ extending $r,(a\,b)s$,
and the latter that $s^{\prime}=(a\,a^{\prime})s$ and
$a^{\prime}\mathbin{\\#}s$. Then $\overline{s}$ extends
$(a^{\prime}\,b)s^{\prime}$. Since $A$ is $\alpha$-invariant, we may assume
that $b\neq a^{\prime}$, i.e. $b\mathbin{\\#}s^{\prime}$. Moreover,

$\operatorname{\mathsf{supp}}(s^{\prime})\subseteq\operatorname{\mathsf{supp}}(s)\setminus\\{a\\}\cup\\{a^{\prime}\\}\subseteq(\operatorname{\mathsf{supp}}(r)\cup\\{a\\})\setminus\\{a\\}\cup\\{a^{\prime}\\}\subseteq\operatorname{\mathsf{supp}}(r)\cup\\{a^{\prime}\\}.$

Thus, $(i,r)\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a^{\prime}\leavevmode\nobreak\ }(j,s^{\prime})$ in $\widetilde{A}$.

  3. 3.

Transitions are finitely branching: Let $(i,r)$ be a state of $\widetilde{A}$.

For every outgoing transition $(i,r)\xrightarrow{\leavevmode\nobreak\
a\leavevmode\nobreak\ }(j,s)$ one has $a\in\operatorname{\mathsf{supp}}(r)$
and $\operatorname{\mathsf{supp}}(s)\subseteq\operatorname{\mathsf{supp}}(r)$.
Thus, there are only finitely many choices for $a$ (since
$\operatorname{\mathsf{supp}}(r)$ is finite) and for $s$ (since $X_{j}$ and
$\operatorname{\mathsf{supp}}(r)$ are finite). Moreover, there are only
finitely many choices for $j$, since $I$ is finite.

Similarly, for every outgoing transition
$(i,r)\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }(j,s)$ one has
$\operatorname{\mathsf{supp}}(s)\subseteq\operatorname{\mathsf{supp}}(r)\cup\\{a\\}$.
The equivalence class $\langle a\rangle s$ is uniquely determined by (1) the
position $x_{a}\in X_{j}$ such that $s(x_{a})=a$ (if any) and (2) the domain
restriction $s^{\prime}$ of $s$ to $\mathsf{dom}(s)\setminus\\{x_{a}\\}$.
There are only finitely many possible choices for (1), and since
$\operatorname{\mathsf{supp}}(s^{\prime})\subseteq\operatorname{\mathsf{supp}}(r)$
there are only finitely many possible choices for (2). Moreover, there are,
again, only finitely many choices for $j$, so the set $\\{\langle a\rangle
s:(i,r)\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }(j,s)\\}$ is finite.

We first show the correctness of the name-dropping modification for the case
of finite bar strings:

######  Theorem C.3.

For every RNNA $A$, the literal language $L_{0}(\widetilde{A})$ is the closure
of $L_{0}(A)$ under $\alpha$-equivalence.

This follows from the two lemmas below:

######  Lemma C.4.

The literal language $L_{0}(\widetilde{A})$ is closed under
$\alpha$-equivalence.

######  Proof C.5.

  1. 1.

Let $\sigma_{1}\cdots\sigma_{n}\in\overline{\mathbb{A}}^{*}$ be a finite bar
string and let $S_{i}=\mathsf{FN}(\sigma_{i+1}\cdots\sigma_{n})$ for
$i=0,\ldots,n$. We claim that if

$(i_{0},r_{0})\xrightarrow{\leavevmode\nobreak\ \sigma_{1}\leavevmode\nobreak\
}(i_{1},r_{1})\xrightarrow{\leavevmode\nobreak\ \sigma_{2}\leavevmode\nobreak\
}\cdots\xrightarrow{\leavevmode\nobreak\ \sigma_{n}\leavevmode\nobreak\
}(i_{n},r_{n})$

is a run in $\widetilde{A}$ then also

$(i_{0},r_{0}^{\prime})\xrightarrow{\leavevmode\nobreak\
\sigma_{1}\leavevmode\nobreak\
}(i_{1},r_{1}^{\prime})\xrightarrow{\leavevmode\nobreak\
\sigma_{2}\leavevmode\nobreak\ }\cdots\xrightarrow{\leavevmode\nobreak\
\sigma_{n}\leavevmode\nobreak\ }(i_{n},r_{n}^{\prime})$

is a run in $\widetilde{A}$, where $r_{i}^{\prime}$ is the restriction of
$r_{i}$ to those $x\in\mathsf{dom}(r_{i})$ such that $r_{i}(x)\in S_{i}$.
(Note that $\operatorname{\mathsf{supp}}(r_{i}^{\prime})=S_{i}$ since
$S_{i}\subseteq\operatorname{\mathsf{supp}}(r_{i})$ by 4.2.3.) The proof
proceeds by induction on $n$.

The base case $n=0$ (i.e. $w=\varepsilon$) is trivial.

For the induction step, suppose that $n\geq 1$. If $\sigma_{1}=a$, then
$S_{0}=S_{1}\cup\\{a\\}$ and so
$\operatorname{\mathsf{supp}}(r_{1}^{\prime})\cup\\{a\\}=S_{1}\cup\\{a\\}\subseteq
S_{0}=\operatorname{\mathsf{supp}}(r_{0}^{\prime})$. Thus the transition
$(i_{0},r_{0}^{\prime})\xrightarrow{\leavevmode\nobreak\ a\leavevmode\nobreak\
}(i_{1},r_{1}^{\prime})$ exists in $\widetilde{A}$. Similarly, if
$\sigma_{1}={\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a$ we have $S_{0}=S_{1}\setminus\\{a\\}$, which implies
$S_{1}\subseteq S_{0}\cup\\{a\\}$. Thus
$\operatorname{\mathsf{supp}}(r_{1}^{\prime})=S_{1}\subseteq
S_{0}\cup\\{a\\}=\operatorname{\mathsf{supp}}(r_{0}^{\prime})\cup\\{a\\}$, so
the transition $(i_{0},r_{0}^{\prime})\xrightarrow{\leavevmode\nobreak\
{\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }(i_{1},r_{1}^{\prime})$ exists in
$\widetilde{A}$. Now apply the induction hypothesis.

  2. 2.

Suppose that $w=_{\alpha}w^{\prime}$. We show that every state $(i,r)$ of
$\widetilde{A}$ accepting $w$ also accepts $w^{\prime}$. We may assume
w.l.o.g. that $w={\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}av$ and $w^{\prime}={\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a^{\prime}(a\,a^{\prime})v$ for $a^{\prime}\mathbin{\\#}v$.
Moreover, by part 1 we may assume that the first transition
$(i,r)\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }(j,s)$ of the accepting run for $w$ is such
that $\operatorname{\mathsf{supp}}(s)$ is the set of free names of $v$; in
particular, $a^{\prime}\mathbin{\\#}s$. It follows that $\langle a\rangle
s=\langle a^{\prime}\rangle(a\,a^{\prime})s$, so
$(i,r)\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a^{\prime}\leavevmode\nobreak\ }(j,(a\,a^{\prime})s)$ by
$\alpha$-invariance. Since $(j,s)$ accepts $v$, the state
$(j,(a\,a^{\prime})s)$ accepts $(a\,a^{\prime})v$ by equivariance, and so we
conclude that $(i,r)$ accepts the bar string ${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a^{\prime}(a\,a^{\prime})v$.

######  Lemma C.6.

The RNNAs $A$ and $\widetilde{A}$ accept the same bar language:
$L_{\alpha}(A)=L_{\alpha}(\widetilde{A})$.

######  Proof C.7.

($\subseteq$) We show for every state $(i,r)$ of $A$ and every bar string
$w\in\overline{\mathbb{A}}^{*}$: if $(i,r)$ accepts $w$ in $A$, then $(i,r)$
accepts some $w^{\prime}\in\overline{\mathbb{A}}^{*}$ such that
$w^{\prime}=_{\alpha}w$ in $\widetilde{A}$. The proof is by induction on the
length of $w$.

The base case $w=\varepsilon$ is trivial.

If $w=av$ for $a\in\mathbb{A}$ and $v\in\overline{\mathbb{A}}^{*}$, let
$(i,r)\xrightarrow{\leavevmode\nobreak\ a\leavevmode\nobreak\ }(j,s)$ be the
first transition of an accepting run for $w$ in $A$. Then the same transition
exists in $\widetilde{A}$ and by induction, $(j,s)$ accepts some
$v^{\prime}\in\overline{\mathbb{A}}^{*}$ such that $v^{\prime}=_{\alpha}v$ in
$\widetilde{A}$. Thus $(i,r)$ accepts the word $w^{\prime}=av^{\prime}$ in
$\widetilde{A}$, and we have $w^{\prime}=av^{\prime}=_{\alpha}av=w$.

If $w={\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}bv$ for some $b\in\mathbb{A}$ and $v\in\overline{\mathbb{A}}^{*}$,
let $(i,r)\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}b\leavevmode\nobreak\ }(j,s)$ be the first transition of an
accepting run for $w$ in $A$. Choose $a\in\mathbb{A}$ such that
$a\mathbin{\\#}s,v$. Then we have the transition
$(i,r)\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }(j,(a\,b)s)$ in $\widetilde{A}$. By
induction, the state $(j,s)$ of $\widetilde{A}$ accepts some
$v^{\prime}=_{\alpha}v$. Thus $(j,(a\,b)s)$ accepts $(a\,b)v^{\prime}$ by
equivariance. It follows that $(i,r)$ accepts $w^{\prime}={\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a(a\,b)v^{\prime}$ in $\widetilde{A}$ and moreover $w={\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}bv=_{\alpha}{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a(a\,b)v=_{\alpha}{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a(a\,b)v^{\prime}=w^{\prime}$.

($\supseteq$) We show that for every state $(i,r)$ of $\widetilde{A}$
accepting $w\in\overline{\mathbb{A}}^{*}$, there exists a state
$(i,\overline{r})$ of $A$ such that

  1. 1.

$\overline{r}(x)=r(x)$ for every $x\in\mathsf{dom}(r)$ with $r(x)$ free in
$w$, and

  2. 2.

$(i,\overline{r})$ accepts some $w^{\prime}\in\overline{\mathbb{A}}^{*}$ such
that $w^{\prime}=_{\alpha}w$.

The proof is again by induction on the length of $w$.

The base case $w=\varepsilon$ is trivial.

For the induction step, suppose that $(i,r)$ accepts $w=\sigma v$ for
$\sigma\in\overline{\mathbb{A}}$ and $v\in\overline{\mathbb{A}}^{*}$. Let
$(i,r)\xrightarrow{\leavevmode\nobreak\ \sigma\leavevmode\nobreak\ }(j,s)$ be
the first transition of an accepting run for $w$ in $\widetilde{A}$. By
induction, there exists $(j,\overline{s})$ in $A$ such that

  1. 1.

$\overline{s}(x)=s(x)$ for every $x\in\mathsf{dom}(s)$ with $s(x)$ free in
$v$.

  2. 2.

$(j,\overline{s})$ accepts some $v^{\prime}\in\overline{\mathbb{A}}^{*}$ such
that $v^{\prime}=_{\alpha}v$.

We treat the cases of free and bound transitions separately:

Case $\sigma=a$:
Since $(i,r)\xrightarrow{\leavevmode\nobreak\ a\leavevmode\nobreak\ }(j,s)$ in
$\widetilde{A}$ we have $(i,\overline{r})\xrightarrow{\leavevmode\nobreak\
a\leavevmode\nobreak\ }(j,\overline{s}^{\prime})$ in $A$ for some
$\overline{r},\overline{s}^{\prime}$ extending $r,s$. Then clearly the state
$(i,\overline{r})$ satisfies 1. To prove condition 2, choose a permutation
$\tau\in\mathsf{Perm}(\mathbb{A})$ such that
$\tau\cdot\overline{s}=\overline{s}^{\prime}$; such a $\tau$ exists because
$(j,\overline{s})$ and $(j,\overline{s}^{\prime})$ are states of $A$, so
$\overline{s},\overline{s}^{\prime}\colon X_{j}\to\mathbb{A}$ are total
injective maps, whence elements of $A^{\\#X_{j}}$ which has just one orbit. We
show that the word

$w^{\prime}:=a(\tau\cdot v^{\prime})$

satisfies the desired condition. Indeed, since $(j,\overline{s})$ accepts
$v^{\prime}$, the state $(j,\overline{s}^{\prime})=(j,\tau\cdot\overline{s})$
accepts $\tau\cdot v^{\prime}$ by equivariance and thus $(i,\overline{r})$
accepts $w^{\prime}$. Moreover, since the free variables of $v^{\prime}$
(equivalently, those of $v$) occur at the the same positions of $s$,
$\overline{s}$ and $\overline{s}^{\prime}$, the permutation $\tau$ fixes them.
Thus $\tau\cdot v^{\prime}=_{\alpha}v^{\prime}$ and therefore

$w^{\prime}=a(\tau\cdot v^{\prime})=_{\alpha}av^{\prime}=_{\alpha}av=w.$

Case $\sigma={\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a$:
Since $(i,r)\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}a\leavevmode\nobreak\ }(j,s)$ in $\widetilde{A}$ we have
$(i,\overline{r})\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}b\leavevmode\nobreak\ }(j,\overline{s}^{\prime})$ in $A$ for some
$b\mathbin{\\#}s$ and some $\overline{r},\overline{s}^{\prime}$ extending
$r,(a\,b)s$. Choose a name $c\mathbin{\\#}a,b,\overline{r},v^{\prime}$ and put
$\pi=(a\,c)$. Then we have the transition
$(i,\pi\cdot\overline{r})\xrightarrow{\leavevmode\nobreak\ {\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{4.73611pt}}\hskip
0.86108pt}\pi(b)\leavevmode\nobreak\ }(j,\pi\cdot\overline{s}^{\prime})$ in
${A}$ by equivariance. The state $(i,\pi\cdot\overline{r})$ satisfies
condition 1 because $a$ is not free in $w={\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}av$. To prove
condition 2, choose a permutation $\tau\in\mathsf{Perm}(\mathbb{A})$ such that
$\tau\cdot\overline{s}=\pi\cdot\overline{s}^{\prime}$ and
$a\mathbin{\\#}\tau\cdot v^{\prime}$. This choice is possible because
$a\mathbin{\\#}\pi\cdot\overline{s}^{\prime}$. We show that the word

$w^{\prime}:={\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}\pi(b)(\tau\cdot v^{\prime})$

satisfies the desired. Indeed, since $(j,\overline{s})$ accepts $v^{\prime}$,
the state $(j,\pi\cdot\overline{s}^{\prime})=(j,\tau\cdot\overline{s})$
accepts $\tau\cdot v^{\prime}$ by equivariance and thus
$(i,\pi\cdot\overline{r})$ accepts $w^{\prime}$.

We now prove that

$(a\,\pi(b))\tau\cdot v^{\prime}=_{\alpha}v^{\prime}.$ (C.2)

To see this we will show that the permutation $(a\,\pi(b))\tau$ fixes all free
variables of $v^{\prime}$ (equivalently, those of $v$). Indeed, if $a$ is free
in $v$, then $a$ occurs in $s$; thus, at the same position $a$ occurs in
$\overline{s}$ and $\pi(b)$ occurs at that position in
$\pi\cdot\overline{s}^{\prime}$. Since
$\tau\cdot\overline{s}=\pi\cdot\overline{s}^{\prime}$, we see that $\tau$ maps
$a$ to $\pi(b)$, whence $(a\,\pi(b))\tau$ maps $a$ to $a$. For every other
free variable $a^{\prime}\neq a$ of $v$, the name $a^{\prime}$ occurs in $s$,
$\overline{s}$, $\overline{s}^{\prime},\pi\cdot\overline{s}^{\prime}$ at the
same position. Thus $\tau$ maps $a^{\prime}$ to $a^{\prime}$, which implies
that $(a\,\pi(b))\cdot\tau$ maps $a^{\prime}$ to $a^{\prime}$ because
$a^{\prime}\neq a,\pi(b)$, using that $\pi(b)\in\\{b,c\\}$ and
$b\mathbin{\\#}s$, $c\mathbin{\\#}v^{\prime}$, so both $b,c$ are not free
variables of $v$.

Finally, we obtain

$w^{\prime}={\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}\pi(b)(\tau\cdot v^{\prime})=_{\alpha}{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}a(a\,\pi(b))\tau\cdot
v^{\prime}\overset{\eqref{eq:tau}}{=_{\alpha}}{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip
0.86108pt}av^{\prime}=_{\alpha}{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}av=w,$

where, in the second step, we use the definition of $\alpha$-equivalence and
that $a\mathbin{\\#}\tau\cdot v^{\prime}$.

We are ready to prove the correctness of the name-dropping modification for
Büchi RNNAs (Theorem 5.3). As for the case of finite bar strings established
above (Theorem C.3) we split the proof into two lemmas:

######  Lemma C.8.

The literal $\omega$-language of $\widetilde{A}$ is closed under
$\alpha$-equivalence.

######  Proof C.9.

  1. 1.

Recall from C.4 that $L_{0}(\widetilde{A})$ is closed under
$\alpha$-equivalence; in fact, the proof of that lemma shows that if
$\sigma_{1}\sigma_{1}\cdots\sigma_{n}=_{\alpha}\sigma_{1}^{\prime}\sigma_{2}^{\prime}\cdots\sigma_{n}^{\prime}$
and

$q_{0}\xrightarrow{\leavevmode\nobreak\ \sigma_{1}\leavevmode\nobreak\
}q_{1}\xrightarrow{\leavevmode\nobreak\ \sigma_{2}\leavevmode\nobreak\
}\cdots\xrightarrow{\leavevmode\nobreak\ \sigma_{n}\leavevmode\nobreak\
}q_{n}$

is a run for $\sigma_{1}\sigma_{2}\cdots\sigma_{n}$ in $\widetilde{A}$, then
there exists a run

$q_{0}\xrightarrow{\leavevmode\nobreak\
\sigma_{1}^{\prime}\leavevmode\nobreak\
}q_{1}^{\prime}\xrightarrow{\leavevmode\nobreak\
\sigma_{2}^{\prime}\leavevmode\nobreak\
}\cdots\xrightarrow{\leavevmode\nobreak\
\sigma_{n}^{\prime}\leavevmode\nobreak\ }q_{n}^{\prime}$ (C.3)

in $\widetilde{A}$ such that $q_{i}^{\prime}$ is final iff $q_{i}$ is final
for $i=1,\ldots,n$.

  2. 2.

Let $w=\sigma_{1}\sigma_{1}\sigma_{2}\cdots$ and
$w^{\prime}=\sigma_{1}^{\prime}\sigma_{2}^{\prime}\sigma_{3}^{\prime}\cdots$
be two infinite bar strings such that $w=_{\alpha}w^{\prime}$, and suppose
that $\widetilde{A}$ accepts $w$ via the accepting run

$q_{0}\xrightarrow{\leavevmode\nobreak\ \sigma_{1}\leavevmode\nobreak\
}q_{1}\xrightarrow{\leavevmode\nobreak\ \sigma_{2}\leavevmode\nobreak\
}q_{2}\xrightarrow{\leavevmode\nobreak\ \sigma_{3}\leavevmode\nobreak\
}\cdots.$

We need to construct an accepting run for $w^{\prime}$. Consider the tree
whose nodes are the partial runs (C.3) where $n\in{\mathbb{N}}$ and
$q_{i}^{\prime}$ final iff $q_{i}$ final for $i=1,\ldots,n$, and whose edge
relation is given by extension of runs. Thus, the nodes of depth $n$ are
precisely the runs (C.3). This tree is infinite since a run (C.3) exists for
each $n$ by part 1, but finitely branching since there are only finitely many
such runs for each $n$, using that
$\operatorname{\mathsf{supp}}(q_{i}^{\prime})\subseteq\operatorname{\mathsf{supp}}(q_{0})\cup\mathsf{N}(\sigma_{1}^{\prime}\sigma_{2}^{\prime}\cdots\sigma_{n}^{\prime})$
for $i=1,\ldots,n$ by 4.2 and that the orbit-finite set $\widetilde{Q}$
contains only finitely many elements with a given support. Thus, the tree
contains an infinite path by Kőnig’s lemma. That is, we obtain an infinite run

$q_{0}\xrightarrow{\leavevmode\nobreak\
\sigma_{1}^{\prime}\leavevmode\nobreak\
}q_{1}^{\prime}\xrightarrow{\leavevmode\nobreak\
\sigma_{2}^{\prime}\leavevmode\nobreak\
}q_{2}^{\prime}\xrightarrow{\leavevmode\nobreak\
\sigma_{3}^{\prime}\leavevmode\nobreak\ }\cdots$

with $q_{i}^{\prime}$ final iff $q_{i}$ final for each $i$. This is an
accepting run for $w^{\prime}$, as required.

######  Lemma C.10.

The Büchi RNNAs $A$ and $\widetilde{A}$ accept the same bar $\omega$-language.

######  Proof C.11.

  1. 1.

Recall from C.6 that $L_{\alpha}(A)=L_{\alpha}(\widetilde{A})$. In fact, the
proof of that lemma shows that for every
$\sigma_{1}\sigma_{2}\cdots\sigma_{n}\in\overline{\mathbb{A}}^{*}$ and every
run

$q_{0}\xrightarrow{\leavevmode\nobreak\ \sigma_{1}\leavevmode\nobreak\
}q_{1}\xrightarrow{\leavevmode\nobreak\ \sigma_{2}\leavevmode\nobreak\
}\cdots\xrightarrow{\leavevmode\nobreak\ \sigma_{n}\leavevmode\nobreak\
}q_{n}$

in $\widetilde{A}$ there exist
$\sigma_{1}^{\prime}\sigma_{2}^{\prime}\cdots\sigma_{n}^{\prime}\in\overline{\mathbb{A}}^{*}$
and a run

$q_{0}\xrightarrow{\leavevmode\nobreak\
\sigma_{1}^{\prime}\leavevmode\nobreak\
}q_{1}^{\prime}\xrightarrow{\leavevmode\nobreak\
\sigma_{2}^{\prime}\leavevmode\nobreak\
}\cdots\xrightarrow{\leavevmode\nobreak\
\sigma_{n}^{\prime}\leavevmode\nobreak\ }q_{n}^{\prime}$ (C.4)

in ${A}$ such that
$\sigma_{1}^{\prime}\sigma_{2}^{\prime}\cdots\sigma_{n}^{\prime}=_{\alpha}\sigma_{1}\sigma_{2}\cdots\sigma_{n}$
and $q_{i}^{\prime}$ final in $A$ iff $q_{i}$ final in $\widetilde{A}$ for
$i=1,\ldots,n$; and vice versa with interchanged roles of $A$ and
$\widetilde{A}$.

  2. 2.

To prove $L_{\alpha,\omega}(\widetilde{A})\subseteq L_{\alpha,\omega}(A)$, let
$w=\sigma_{1}\sigma_{2}\sigma_{3}\cdots$ be an infinite bar string in
$L_{0,\omega}(\widetilde{A})$ and

$q_{0}\xrightarrow{\leavevmode\nobreak\ \sigma_{1}\leavevmode\nobreak\
}q_{1}\xrightarrow{\leavevmode\nobreak\ \sigma_{2}\leavevmode\nobreak\
}q_{2}\xrightarrow{\leavevmode\nobreak\ \sigma_{3}\leavevmode\nobreak\
}\cdots$

be an accepting run for $w$ in $\widetilde{A}$; we need to find $w^{\prime}\in
L_{0,\omega}(A)$ such that $w^{\prime}=_{\alpha}w$. Let $m=\mathsf{deg}(A)$
and choose a set $S\subseteq\mathbb{A}$ of $m+1$ distinct names containing
$\operatorname{\mathsf{supp}}(q_{0})$. Consider the tree whose nodes are the
partial runs (C.4) in $A$ where (1) $n\in{\mathbb{N}}$, (2) $q_{i}^{\prime}$
final in $A$ iff $q_{i}$ final in $\widetilde{A}$ for $i=1,\ldots,n$, (3)
$\mathsf{N}(\sigma_{1}^{\prime}\sigma_{2}^{\prime}\cdots\sigma_{n}^{\prime})\subseteq
S$, and (4)
$\sigma_{1}^{\prime}\sigma_{2}^{\prime}\cdots\sigma_{n}^{\prime}=_{\alpha}\sigma_{1}\sigma_{2}\cdots\sigma_{n}$.
The edge relation is given by extension of runs. Thus, the nodes of depth $n$
are precisely the runs (C.4). This tree is infinite since, by part 1 and the
proof of 4.3, for each $n\in{\mathbb{N}}$ there exists a run (C.4) satisfying
the above conditions (2)–(4). It is finitely branching because for every such
run one has $\operatorname{\mathsf{supp}}(q_{i}^{\prime})\subseteq S$ and
$\sigma_{i}^{\prime}\in S$ for each $i$, so there are only finitely many nodes
of depth $n$. Thus, the tree contains an infinite path by Kőnig’s lemma. That
is, we obtain an infinite run

$q_{0}\xrightarrow{\leavevmode\nobreak\
\sigma_{1}^{\prime}\leavevmode\nobreak\
}q_{1}^{\prime}\xrightarrow{\leavevmode\nobreak\
\sigma_{2}^{\prime}\leavevmode\nobreak\
}q_{2}^{\prime}\xrightarrow{\leavevmode\nobreak\
\sigma_{3}^{\prime}\leavevmode\nobreak\ }\cdots$

with $q_{i}^{\prime}$ final iff $q_{i}$ final for each $i$, and
$\sigma_{1}^{\prime}\sigma_{2}^{\prime}\cdots\sigma_{n}^{\prime}=_{\alpha}\sigma_{1}\sigma_{2}\cdots\sigma_{n}$
for each $n$. Putting

$w^{\prime}:=\sigma_{1}^{\prime}\sigma_{2}^{\prime}\sigma_{3}^{\prime}\cdots$

we obtain $w^{\prime}=_{\alpha}w$ and $w\in L_{0,\omega}(A)$, as required.

  3. 3.

The proof of the reverse inclusion $L_{\alpha,\omega}(A)\subseteq
L_{\alpha,\omega}(\widetilde{A})$ is symmetric.

This concludes the proof of Theorem 5.3.

##  Appendix D Details for Section 6

## Proof of 6.6

($\Leftarrow$) Suppose that there exists $w^{\prime}\sqsupseteq w$ such that
$[w^{\prime}]_{\alpha}\in L$, and let $u\in D(w)$. Then there exists
$v\in\overline{\mathbb{A}}^{\omega}$ such that $v=_{\alpha}w$ and
$\mathsf{ub}(v)=u$. By 6.4, there exists $v^{\prime}\sqsupseteq v$ such that
$v^{\prime}=_{\alpha}w^{\prime}$. Thus
$[v^{\prime}]_{\alpha}=[w^{\prime}]_{\alpha}\in L$, so
$u=\mathsf{ub}(v)=\mathsf{ub}(v^{\prime})\in D(L)$.

($\Rightarrow$) Suppose that $D(w)\subseteq D(L)$, and let $A$ be a Büchi RNNA
accepting $L$ with the initial state $q_{0}$. By Theorem 5.3 we may assume
that $L_{0,\omega}(A)$ is closed under $\alpha$-equivalence. Choose a clean
bar string $v\in\overline{\mathbb{A}}^{\omega}$ (3.1) such that $v=_{\alpha}w$
and such that for every $a\in\operatorname{\mathsf{supp}}(q_{0})$ the letter
${\hskip 0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$
does not appear in $v$. Then $\mathsf{ub}(v)\in D(w)\subseteq D(L)$, so there
exists $v^{\prime}\in\overline{\mathbb{A}}^{\omega}$ such that
$\mathsf{ub}(v^{\prime})=\mathsf{ub}(v)$ and $v^{\prime}\in L_{0,\omega}(A)$.

We now prove that $v\sqsubseteq v^{\prime}$. To see this, let
$v=\sigma_{1}\sigma_{2}\sigma_{3}\cdots$ and
$v^{\prime}=\sigma_{1}^{\prime}\sigma_{2}^{\prime}\sigma_{3}^{\prime}\cdots$
and suppose that $\sigma_{n}={\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$ for some
$a\in\mathbb{A}$. Since $\mathsf{ub}(v^{\prime})=\mathsf{ub}(v)$ we know that
$\sigma_{n}^{\prime}\in\\{a,{\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a\\}$, and we
need to prove that $\sigma_{n}^{\prime}={\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$. Suppose to
the contrary that $\sigma_{n}^{\prime}=a$. Then
$a\mathbin{\\#}\operatorname{\mathsf{supp}}(q_{0})$ by the above choice of
$v$. By 4.2.3 the name $a$ cannot occur freely in $v^{\prime}$. This implies
that there exists $m<n$ such that $\sigma^{\prime}_{m}={\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$. Thus,
$\mathsf{ub}(v^{\prime})$ has the name $a$ at position $m$ and $n$. On the
other hand, since $\sigma_{n}={\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$ and $v$ is
clean, $\sigma_{m}$ is not equal to $a$ or ${\hskip
0.86108pt{\rule[-0.43057pt]{0.6pt}{7.10411pt}}\hskip 0.86108pt}a$, that is,
$\mathsf{ub}(v^{\prime})$ has distinct names at position $m$ and $n$. Thus
$\mathsf{ub}(v^{\prime})\neq\mathsf{ub}(v)$, a contradiction.

Since $v=_{\alpha}w$ and $v\sqsubseteq v^{\prime}$, by 6.4 there exists
$w^{\prime}\sqsupseteq w$ such that $w^{\prime}=_{\alpha}v^{\prime}$. Then
$[w^{\prime}]_{\alpha}=[v^{\prime}]_{\alpha}\in L$, as required.

##  Appendix E Details for Section 7

## Proof of 7.3

We show how to convert a Büchi RNNA into an equivalent Muller RNNA and vice
versa. The two constructions are completely analogous to the classical ones.

  1. 1.

If $A=(Q,R,q_{0},F)$ is a Büchi RNNA accepting $L$, then the Muller RNNA
$A^{\prime}=(Q,R,q_{0},\mathcal{F})$ where $\mathcal{F}=\\{X\subseteq Q:X\cap
F\neq\emptyset\\}$ accepts $L$.

  2. 2.

Suppose that $A=(Q,R,q_{0},\mathcal{F})$ is a Büchi RNNA accepting $L$. Let
$\mathcal{F}=\\{F_{1},\ldots,F_{n}\\}$ where $F_{i}\subseteq\mathsf{orb}(Q)$,
and denote by $\overline{F_{i}}\subseteq Q$ the union $\bigcup_{O\in F_{i}}O$.
Then the following Büchi RNNA $A^{\prime}=(Q^{\prime},R^{\prime},q_{0},F)$
accepts $L$:

     * •

$Q^{\prime}=Q\cup\bigcup_{i=1}^{n}\\{i\\}\times\overline{F_{i}}\times\mathcal{P}(F_{i})$.

     * •

For each transition $q\xrightarrow{\leavevmode\nobreak\
\sigma\leavevmode\nobreak\ }q^{\prime}$ in $A$ we have the following
transitions in $A^{\prime}$:

       1. (1)

$q\xrightarrow{\leavevmode\nobreak\ \sigma\leavevmode\nobreak\ }q^{\prime}$;

       2. (2)

$q\xrightarrow{\leavevmode\nobreak\ \sigma\leavevmode\nobreak\
}(i,q^{\prime},\emptyset)$ for all $i$ such that
$q^{\prime}\in\overline{F_{i}}$;

       3. (3)

$(i,q,R)\xrightarrow{\leavevmode\nobreak\ \sigma\leavevmode\nobreak\
}(i,q^{\prime},R\cup\\{q^{\prime}\\})$ for all $i$ with
$q,q^{\prime}\in\overline{F_{i}}$ and all $R\subseteq F_{i}$ with $R\neq
F_{i}$;

       4. (4)

$(i,q,F_{i})\xrightarrow{\leavevmode\nobreak\ \sigma\leavevmode\nobreak\
}(i,q^{\prime},\emptyset)$ for all $i$ such that
$q,q^{\prime}\in\overline{F_{i}}$.

     * •

$F=\\{(i,q,F_{i}):i=1,\ldots,n,\,q\in\overline{F_{i}}\\}$.

While simulating $A$ the automaton $A^{\prime}$ guesses that from some point
on, only states from $\overline{F_{i}}$ for some $i$ will be visited, and uses
the third component of states to make sure that each orbit from $F_{i}$ is
visited infinitely often.