# Parikh Automata on Infinite Words

Mario Grobler<EMAIL_ADDRESS>University of Bremen, Bremen, Germany
Leif Sabellek<EMAIL_ADDRESS>University of Bremen, Bremen, Germany
Sebastian Siebertz  University of Bremen, Bremen, Germany  siebertz@uni-
bremen.de

###### Abstract

Parikh automata on finite words were first introduced by Klaedtke and Rueß
[Automata, Languages and Programming, 2003]. In this paper, we introduce
several variants of Parikh automata on infinite words and study their
expressiveness. We show that one of our new models is equivalent to
synchronous blind counter machines introduced by Fernau and Stiebe [Fundamenta
Informaticae, 2008]. All our models admit $\varepsilon$-elimination, which to
the best of our knowledge is an open question for blind counter automata. We
then study the classical decision problems of the new automata models.

###### keywords:

Automata theory, Parikh automata, infinite words, epsilon-elimination

††journal: arXiv

###### Contents

  1. 1 Introduction
  2. 2 Preliminaries
    1. 2.1 Finite and infinite words
    2. 2.2 Regular and $\omega$-regular languages
    3. 2.3 Semi-linear sets
    4. 2.4 Parikh-recognizable languages
  3. 3 Parikh automata on infinite words
    1. 3.1 Definitions of Parikh-Büchi Automata
    2. 3.2 Simple Observations.
    3. 3.3 Equivalence of $\varepsilon$-WPBA and $\varepsilon$-SPBA
  4. 4 Schnepsilon-elimination
    1. 4.1 $\varepsilon$-elimination for PPBA
    2. 4.2 $\varepsilon$-elimination for SPBA
  5. 5 Equivalence of PPBA and blind counter machines and their closure properties
  6. 6 Expressiveness of PPBA and SPBA
  7. 7 Decision problems
  8. 8 Conclusion and Outlook

##  1 Introduction

Parikh automata on finite words (PA), originally introduced by Klaedtke and
Rueß in [9], are finite automata enriched with counters. A PA is a non-
deterministic finite automaton that is additionally equipped with a semi-
linear set $C$. Furthermore, every transition is equipped with a $d$-tuple of
non-negative integers and every time a transition is used, the counters are
incremented by the values in the tuple accordingly. An input word is accepted
if the PA ends in a final state and additionally, the resulting $d$-tuple in
the counters lies in $C$. The class of languages recognized by PA contains all
regular languages, but also many more, even languages that are not context-
free, e. g., the language $\\{a^{n}b^{n}c^{n}\mid n\in\mathbb{N}\\}$. On the
other hand, the language of palindromes is context-free, but cannot be
recognized by a PA.

On finite words, Parikh automata have been investigated extensively. As shown
in [9], the class of languages recognized by PA is captured precisely by weak
existential monadic second-order logic of one successor extended with linear
cardinality constraints. Cadilhac, Finkel and McKenzie introduced the variant
of affine Parikh automata [2] and used Parikh automata to characterize bounded
languages [3]. Two-way PA were studied in [4] and PA with a visibly pushdown
stack were studied in [7].

In this paper, we initiate the research on Parikh automata on infinite words.
This research direction was proposed by Klaedtke and Rueß in the conclusion of
their work [9]. Automata on infinite words play an important role in logics
and formal verification, see e.g. the textbook [11]. For example, a non-
terminating system that should distribute resources among three consumers
equally could be modelled using the language $\\{a^{n}b^{n}c^{n}\mid
n\in\mathbb{N}\\}^{\omega}$, which is not $\omega$-regular and not even
$\omega$-context-free. By Büchi’s theorem every regular $\omega$-language can
be characterized as the finite union of $U_{i}V_{i}^{\omega}$, where
$U_{i},V_{i}$ are regular languages. A natural generalization is the class
$\mathcal{L}_{\mathsf{PA}}^{\omega}$ of languages that can be characterized as
the union of $U_{i}V_{i}^{\omega}$, where $U_{i},V_{i}$ are Parikh-
recognizable languages. This class was also mentioned by Fernau and Stiebe
under the name $\mathcal{K}_{*}$ in [5].

We suggest three different definitions for extending Büchi automata [1] with a
Parikh condition, which we call _Parikh-Büchi-automata_ (PBA). All models are
syntactically equal to PA, and they only differ in their semantics. We
consider _PBA with prefix-acceptance condition_ (PPBA), _PBA with strong
reset-acceptance condition_ (SPBA), and _PBA with weak reset-acceptance
condition_ (WPBA). Furthermore, we consider their variants with
$\varepsilon$-transitions and variants where every accepting state is equipped
with its own semi-linear set.

A PPBA accepts its input if there is a run that satisfies the acceptance
condition for infinitely many prefixes of the word, i. e., it happens
infinitely often that the automaton is in an accepting state and the current
sum of the vectors lies in the semi-linear set of the automaton. This model
was proposed by Klaedtke and Rueß [9]. We write
$\mathcal{L}_{\mathsf{Prefix}}$ for the class of PPBA-recognizable languages.
We prove that PPBA are equivalent to synchronous blind counter machines
introduced by Fernau and Stiebe [5]. The main difficulty in this result is to
eliminate $\varepsilon$-transitions in PPBAs, which turns out to be
surprisingly challenging. By this equivalence, PPBA-recognizable languages are
closed under union, but not under intersection or complement. Furthermore, if
$L$ is a Parikh language, then $L^{\omega}$ is not necessarily PPBA-
recognizable, e. g., the language $\\{a^{n}b^{n}\mid
n\in\mathbb{N}\\}^{\omega}$ is not PPBA-recognizable.

This last weakness motivates the definition of PBA-acceptance with the ability
to reset the values of all counters, which leads to the definitions of SPBA
and WPBA. An SPBA is defined like a PPBA, but the current sum of the vectors
_must_ lie in the semi-linear set whenever an accepting state is visited.
After the visit of an accepting state all counters are reset to zero.
Similarly, a WPBA is not forced to, but _may_ reset in an accepting state.
Both automata accept if they reset infinitely often. We prove that both models
have the same expressiveness and we write $\mathcal{L}_{\mathsf{Reset}}$ for
the class of SPBA/WPBA-recongizable $\omega$-languages. One of our main
results is that PBA with a reset condition are strictly more expressive than
PPBA by showing that
$\mathcal{L}_{\mathsf{PA}}^{\omega}\subsetneq\mathcal{L}_{\mathsf{Reset}}$.
Together with the known results for blind counter automata we get

$\mathcal{L}_{\mathsf{Prefix}}\subsetneq\mathcal{L}_{\mathsf{PA}}^{\omega}\subsetneq\mathcal{L}_{\mathsf{Reset}}.$

If $L$ is a Parikh language, then $L^{\omega}$ is SPBA/WPBA-recognizable,
hence, they do not have the weakness of PPBA mentioned above.

Finally, we study the classical decision problems for PPBA and SPBA/WPBA. We
show that for all models, emptiness is $\coNP$-complete and universality (and
hence, inclusion and equivalence) are undecidable.

Organization.  After giving the necessary background in Section 2, we give our
definitions of Parikh automata on infinite words and make some simple
observations in Section 3. In Section 4 we show how to elimination
$\varepsilon$-transitions. In Section 5 we prove the equivalence of PPBA and
blind counter automata and discuss some implications. In Section 6, we prove
$\mathcal{L}_{\mathsf{PA}}^{\omega}\subsetneq\mathcal{L}_{\mathsf{Reset}}$. In
Section 7, we study the decision problems for PPBA and SPBA/WPBA. We conclude
in Section 8.

##  2 Preliminaries

###  2.1 Finite and infinite words

We write $\mathbb{N}$ for the set of non-negative integers including $0$, and
$\mathbb{Z}$ for the set of all integers. Let $\Sigma$ be an alphabet, i. e.,
a finite non-empty set and let $\Sigma^{*}$ be the set of all finite words
over $\Sigma$. For a word $w\in\Sigma^{*}$, we denote by $|w|$ the length of
$w$, and by $|w|_{a}$ the number of occurrences of the letter $a\in\Sigma$ in
$w$. We write $\varepsilon$ for the empty word of length $0$ and
$\Sigma^{+}=\Sigma^{*}\setminus\\{\varepsilon\\}$ for the set of all non-empty
finite words over $\Sigma$.

An _infinite word_ over an alphabet $\Sigma$ is a function
$\alpha:\mathbb{N}\setminus\\{0\\}\rightarrow\Sigma$. We often write
$\alpha_{i}$ instead of $\alpha(i)$. Thus, we can understand an infinite word
as an infinite sequence of symbols
$\alpha=\alpha_{1}\alpha_{2}\alpha_{3}\ldots$ For $m\leq n$, we abbreviate the
finite infix $\alpha_{m}\ldots\alpha_{n}$ by $\alpha[m,n]$. We denote by
$\Sigma^{\omega}$ the set of all infinite words over $\Sigma$. We call a
subset $L\subseteq\Sigma^{\omega}$ an _$\omega$ -language_. Moreover, for
$L\subseteq\Sigma^{*}$, we define $L^{\omega}=\\{w_{1}w_{2}\dots\mid w_{i}\in
L\setminus\\{\varepsilon\\}\\}\subseteq\Sigma^{\omega}$.

###  2.2 Regular and $\omega$-regular languages

A _Nondeterministic Finite Automaton_ (NFA) is a tuple
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F)$, where $Q$ is the finite set of
states, $\Sigma$ is the input alphabet, $q_{0}\in Q$ is the initial state,
$\Delta\subseteq Q\times\Sigma\times Q$ is the set of transitions and
$F\subseteq Q$ is the set of accepting states. A _run_ of $\mathcal{A}$ on a
word $w=w_{1}\cdots w_{n}\in\Sigma^{*}$ is a (possibly empty) sequence of
transitions $r=r_{1}\dots r_{n}$ with $r_{i}=(p_{i-1},w_{i},p_{i})\in\Delta$
such that $p_{0}=q_{0}$. We say $r$ is _accepting_ if $p_{n}\in F$. The empty
run on $\varepsilon$ is accepting if $q_{0}\in F$. We define the _language
recognized by $\mathcal{A}$_ as
$L(\mathcal{A})=\\{w\in\Sigma^{*}\mid\text{there is an accepting run of
$\mathcal{A}$ on $w$}\\}$. If a language $L$ is recognized by some NFA
$\mathcal{A}$, we call $L$ _regular_.

A _Büchi Automaton_ (BA) is an NFA $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F)$
that takes infinite words as input. A _run_ of $\mathcal{A}$ on an infinite
word $\alpha_{1}\alpha_{2}\alpha_{3}\dots$ is an infinite sequence of
transitions $r=r_{1}r_{2}r_{3}\dots$ with
$r_{i}=(p_{i-1},\alpha_{i},p_{i})\in\Delta$ such that $p_{0}=q_{0}$. We say
$r$ is _accepting_ if there are infinitely many $i$ such that $p_{i}\in F$. We
define the _$\omega$ -language recognized by $\mathcal{A}$_ as
$L_{\omega}(\mathcal{A})=\\{\alpha\in\Sigma^{\omega}\mid\text{there is an
accepting run of $\mathcal{A}$ on $\alpha$}\\}$. If an $\omega$-language $L$
is recognized by some BA $\mathcal{A}$, we call $L$ _$\omega$ -regular_.
Büchi’s theorem establishes an important connection between regular and
$\omega$-regular languages:

######  Theorem 2.1 (Büchi).

A language $L\subseteq\Sigma^{\omega}$ is $\omega$-regular if and only if
there are regular languages $U_{1},V_{1},\dots,U_{n},V_{n}\subseteq\Sigma^{*}$
for some $n\geq 1$ such that $L=U_{1}V_{1}^{\omega}\cup\dots\cup
U_{n}V_{n}^{\omega}$.

###  2.3 Semi-linear sets

A _linear set_ of dimension $d$ for $d\geq 1$ is a set of the form
$\\{b_{0}+b_{1}z_{1}+\dots+b_{\ell}z_{\ell}\mid
z_{1},\dots,z_{\ell}\in\mathbb{N}\\}\subseteq\mathbb{N}^{d}$ for
$b_{0},\ldots,b_{\ell}\in\mathbb{N}^{d}$. A _semi-linear set_ is the finite
union of linear sets. For vectors
$\mathbf{u}=(u_{1},\dots,u_{c})\in\mathbb{N}^{c},\mathbf{v}=(v_{1},\dots,v_{d})\in\mathbb{N}^{d}$,
we denote by
$\mathbf{u}\cdot\mathbf{v}=(u_{1},\dots,u_{c},v_{1},\dots,v_{d})\in\mathbb{N}^{c+d}$
the _concatenation of $\mathbf{u}$ and $\mathbf{v}$_. We extend this
definition to sets of vectors. Let $U\subseteq\mathbb{N}^{c}$ and
$V\subseteq\mathbb{N}^{d}$. Then $U\cdot
V=\\{\mathbf{u}\cdot\mathbf{v}\mid\mathbf{u}\in U,\mathbf{v}\in
V\\}\subseteq\mathbb{N}^{c+d}$. We denote by $\mathbf{0}^{d}$ (or simply
$\mathbf{0}$ if $d$ is clear from the context) the all-zero vector, and by
$\mathbf{e}^{d}_{i}$ (or simply $\mathbf{e}_{i})$ the $d$-dimensional vector
where the $i$th entry is $1$ and all other entries are 0.

###  2.4 Parikh-recognizable languages

A _Parikh Automaton_ (PA) is a tuple $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$
where $Q$, $\Sigma$, $q_{0}$, and $F$ are defined as for NFA, $\Delta\subseteq
Q\times\Sigma\times\mathbb{N}^{d}\times Q$ is the set of _labeled transitions_
, and $C\subseteq\mathbb{N}^{d}$ is a semi-linear set. We call $d$ the
_dimension_ of $\mathcal{A}$ and refer to the entries of a vector $\mathbf{v}$
in a transition $(p,a,\mathbf{v},q)$ as _counters_. Similar to NFA, a _run_ of
$\mathcal{A}$ on a word $w=x_{1}\dots x_{n}$ is a (possibly empty) sequence of
labeled transitions $r=r_{1}\dots r_{n}$ with
$r_{i}=(p_{i-1},x_{i},\mathbf{v}_{i},p_{i})\in\Delta$ such that $p_{0}=q_{0}$.
We define the _extended Parikh image_ of a run $r$ as $\rho(r)=\sum_{i\leq
n}\mathbf{v}_{i}$ (with the convention that the empty sum equals
$\mathbf{0}$). We say $r$ is accepting if $p_{n}\in F$ and $\rho(r)\in C$,
referring to the latter condition as the _Parikh condition_. We define the
_language recognized by $\mathcal{A}$_ as
$L(\mathcal{A})=\\{w\in\Sigma^{*}\mid\text{there is an accepting run of
$\mathcal{A}$ on $w$}\\}$. If a language $L\subseteq\Sigma^{*}$ is recognized
by some PA, then we call $L$ _Parikh-recognizable_. We write
$\mathcal{L}_{\mathsf{PA}}$ to denote the class of all Parikh-recognizable
languages.

##  3 Parikh automata on infinite words

In this section we introduce our models of Parikh automata on infinite words
and make some simple observations.

###  3.1 Definitions of Parikh-Büchi Automata

We begin with the definition of Parikh automata on infinite words.

######  Definition 3.1.

A _Parikh-Büchi Automaton_ (PBA) is a PA
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$. A run of $\mathcal{A}$ on an
infinite word $\alpha_{1}\alpha_{2}\alpha_{3}\dots$ is an infinite sequence of
labeled transitions $r=r_{1}r_{2}r_{3}\dots$ with
$r_{i}=(p_{i-1},\alpha_{i},\mathbf{v}_{i},p_{i})\in\Delta$ such that
$p_{0}=q_{0}$. We consider three acceptance conditions.

  1. 1.

_PBA with prefix-acceptance condition_ (PPBA): We say that $r$ _satisfies the
prefix-acceptance condition_ (_is accepting_ for short) if there are
infinitely many $i\geq 1$ such that $p_{i}\in F$ and $\rho(r_{1}\dots
r_{i})\in C$. For these positions $i$ we say that there is an _accepting hit
in $r_{i}$_. We define the $\omega$-language recognized by a PPBA
$\mathcal{A}$ as
$P_{\omega}(\mathcal{A})=\\{\alpha\in\Sigma^{\omega}\mid\mathcal{A}\text{
accepts }\alpha\\}$.

  2. 2.

_PBA with weak reset-acceptance condition_ (WPBA): We say that $r$ _satisfies
the weak reset-acceptance condition_ (_is accepting_ for short) if there are
infinitely many _reset positions_ $0=k_{0}<k_{1}<k_{2}\dots$ such that
$p_{k_{i}}\in F$ and $\rho(r_{k_{i-1}+1}\dots r_{k_{i}})\in C$ for all $i\geq
1$. We define the $\omega$-language recognized by a WPBA $\mathcal{A}$ as
$W_{\omega}(\mathcal{A})=\\{\alpha\in\Sigma^{\omega}\mid\mathcal{A}\text{
accepts }\alpha\\}$.

  3. 3.

_PBA with strong reset-acceptance condition_ (SPBA): Let $k_{0}=0$ and denote
by $k_{1},k_{2},\dots$ the positions of all accepting states in $r$, i. e.,
$p_{k_{i}}\in F$ for all $i\geq 1$. We say that $r$ _satisfies the strong
reset-acceptance condition_ (_is accepting_ for short) if $k_{1},k_{2},\dots$
is an infinite sequence and $\rho(r_{k_{i-1}+1}\dots r_{k_{i}})\in C$ for all
$i\geq 1$. We define the $\omega$-language recognized by an SPBA $\mathcal{A}$
as $S_{\omega}(\mathcal{A})=\\{\alpha\in\Sigma^{\omega}\mid\mathcal{A}\text{
accepts }\alpha\\}$.

Intuitively, an SPBA $\mathcal{A}$ accepts all infinite words $\alpha$ in such
a way, that whenever a run of $\mathcal{A}$ on $\alpha$ visits an accepting
state, the Parikh condition _must_ be satisfied. After that, the counters are
reset. Compared to that, a WPBA _may_ reset the counters when visiting an
accepting state but does not have to do so. Both accept if they reset their
counters infinitely often. A PPBA does not reset its counters at all. It
accepts if there exists a run that has infinitely many accepting (finite)
prefixes that satisfy the Parikh condition. Since all automata are
syntactically equal objects we write $P_{\omega}$, $W_{\omega}$ and
$S_{\omega}$ for the accepted $\omega$-languages to make the different
acceptance conditions explicit. For the same reason we will often speak about
resetting states instead of accepting states in the context of SPBA/WPBA.

######  Example 1.

$q_{0}$$q_{1}$$a,\begin{pmatrix}1\\\ 0\end{pmatrix}$$b,\begin{pmatrix}0\\\
1\end{pmatrix}$$b,\begin{pmatrix}0\\\ 1\end{pmatrix}$$a,\begin{pmatrix}1\\\
0\end{pmatrix}$ Figure 1: The PBA $\mathcal{A}$ with $C=\\{(z,z)\mid
z\in\mathbb{N}\\})$ from Example 1.

Let $\mathcal{A}$ with $C=\\{(z,z)\mid z\in\mathbb{N}\\}$ be the PBA depicted
in Figure 1. Then
$W_{\omega}(\mathcal{A})=\\{w\in\\{a,b\\}^{*}\cdot\\{b\\}\mid|w|_{a}=|w|_{b}\\}^{\omega}$.
Note that this language is not $\omega$-regular. While the first counter
tracks the number of already read $a$s, the second counter tracks the number
of already read $b$s. The semi-linear set $C$ essentially states that both
values need to be the same (eventually). Since a WPBA may or may not reset its
counters when visiting an accepting state, $\mathcal{A}$ can ”move freely”
between both of its states. Note that
$P_{\omega}(\mathcal{A})=W_{\omega}(\mathcal{A})$.

Considering the strong reset-acceptance condition, we have
$S_{\omega}(\mathcal{A})=\\{ab\\}^{\omega}$, only a single infinite word is
accepted by this automaton. Assume $\mathcal{A}$ tries to accept an infinite
word $\alpha$ that has an infix $a^{n}$ where $n>1$. That is, $\mathcal{A}$
loops $n$ times in $q_{0}$, hence the first counter has a value of $n$ and the
second counter a value of 0. The only chance to increase the second counter is
by moving into the accepting state $q_{1}$. Since both counters do not have
the same values by then, $\alpha$ will be rejected. If $\mathcal{A}$ tries to
accept an infinite word that starts with a $b$, or has an infix $b^{n}$ where
$n>1$, the input will be rejected for similar reasons.

We now introduce PBAs that allow different semi-linear sets on all accepting
states, which we call Multi-PBA.

######  Definition 3.2.

A _Multi-PBA_ is a tuple $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ where
$C:F\rightarrow\mathcal{P}(\mathbb{N}^{d})$ is a function that assigns a semi-
linear set to each $q\in F$. We define Multi-PPBA (MPBA), MWPBA and MSPBA as
SPBA, WPBA and SPBA, respectively, where the condition
$\rho(r_{i},\ldots,r_{j})\in C$ in the respective definitions is replaced by
$\rho(r_{i},\ldots,r_{j})\in C(p_{j})$.

We finally introduce definitions of PBA that allow $\varepsilon$-transitions.

######  Definition 3.3.

An $\varepsilon$-PBA is a tuple
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta,\mathcal{E},F,C)$ where
$\mathcal{E}\subseteq Q\times\\{\varepsilon\\}\times\mathbb{N}^{d}\times Q$ is
the set of _labeled $\varepsilon$-transitions_, and all other entries are
defined as for PBA. A run of $\mathcal{A}$ on an infinite word
$\alpha_{1}\alpha_{2}\alpha_{3}\dots$ is an infinite sequence of transitions
$r\in(\mathcal{E}^{*}\Delta)^{\omega}$, say $r=r_{1}r_{2}r_{3}\dots$ with
$r_{i}=(p_{i-1},\gamma_{i},\mathbf{v}_{i},p_{i})$ such that $p_{0}=q_{0}$, and
$\gamma_{i}=\varepsilon$ if $r_{i}\in\mathcal{E}$, and $\gamma_{i}=\alpha_{j}$
if $r_{i}\in\Delta$ is the $j$-th occurrence of a (non-$\varepsilon$)
transition in $r$. The definitions of prefix-acceptance condition, weak reset-
acceptance condition and strong reset-condition are the same as in Definition
3.1 and extend to Multi-PBA in the natural way. We use the terms
$\varepsilon$-PPBA, $\varepsilon$-WPBA, $\varepsilon$-SPBA,
$\varepsilon$-MPPBA, $\varepsilon$-MWPBA, and $\varepsilon$-MSPBA,
respectively. We call a transition of the form
$(p,\varepsilon,\mathbf{v},p)\in\mathcal{E}$ an _$\varepsilon$ -loop_.

Note that we can treat every PBA as an $\varepsilon$-PBA, that is, a PBA
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ is equivalent to the
$\varepsilon$-PBA
$\mathcal{A}^{\prime}=(Q,\Sigma,q_{0},\Delta,\varnothing,F,C)$ in the sense
that $P_{\omega}(\mathcal{A})=P_{\omega}(\mathcal{A}^{\prime})$,
$W_{\omega}(\mathcal{A})=W_{\omega}(\mathcal{A}^{\prime})$, and
$S_{\omega}(\mathcal{A})=S_{\omega}(\mathcal{A}^{\prime})$.

###  3.2 Simple Observations.

We begin with a few simple observations. We first show that the accepting
states $F$ and the linear sets of $C$ of an $\varepsilon$-PPBA $\mathcal{A}$
are in a sense independent, as formalized by the following lemma.

######  Lemma 3.1.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,\mathcal{E},F,C)$ be an
$\varepsilon$-PPBA, where $C=C_{1}\cup\dots\cup C_{\ell}$ for linear sets
$C_{j}$, $1\leq j\leq\ell$. Then $P_{\omega}(\mathcal{A})=\bigcup_{f\in
F}\bigcup_{1\leq
j\leq\ell}P_{\omega}(Q,\Sigma,q_{0},\Delta,\mathcal{E},\\{f\\},C_{j})$.

###### Proof.

The right-to-left direction is obvious, thus we show the left-to-right
direction. Let $\alpha\in P_{\omega}(\mathcal{A})$ with an accepting run
$r=r_{1}r_{2}r_{3}\dots$ where
$r_{i}=(p_{i-1},\gamma_{i},\mathbf{v}_{i},p_{i})$, i. e., there are infinitely
many $i\geq 1$ such that $p_{i}\in F$ and $\rho(r_{1}\dots r_{i})\in C$. By
the infinite pigeonhole principle, there is a state $f\in F$ such that
$p_{i^{\prime}}=f$ and $j$ such that $\rho(r_{1}\dots r_{i^{\prime}})\in
C_{j}$ for infinitely many $i^{\prime}\geq 1$. Thus, $\alpha\in
P_{\omega}(Q,\Sigma,q_{0},\Delta,\mathcal{E},\\{f\\},C_{j})$. ∎

Note that this lemma does in general not hold for $\varepsilon$-WPBA and
$\varepsilon$-SPBA.

The following lemma illustrates the simple and yet important combinatorial
method to use additional counters and an adapted semi-linear set to store
information about runs.

######  Lemma 3.2.

For every $\varepsilon$-MPPBA $\mathcal{A}$ there exists an $\varepsilon$-PPBA
$\mathcal{A}^{\prime}$ with a single accepting state such that
$P_{\omega}(\mathcal{A})=P_{\omega}(\mathcal{A}^{\prime})$. If $\mathcal{A}$
has no non-loop $\varepsilon$-transitions, then $\mathcal{A}^{\prime}$ has no
non-loop $\varepsilon$-transitions and if $\mathcal{A}$ is an MPPBA, then
$\mathcal{A}^{\prime}$ is a PPBA.

###### Proof.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,\mathcal{E},F,C)$ be an
$\varepsilon$-MPPBA of dimension $d$ and let $F=\\{q_{1},\dots,q_{k}\\}$.
Since $\mathcal{A}$ is an $\varepsilon$-MPPBA, $C\colon
F\rightarrow\mathcal{P}(\mathbb{N}^{d})$ is a function assigning a semi-linear
set to each $q\in F$. We construct an $\varepsilon$-PPBA
$\mathcal{A}^{\prime}$ of dimension $d+k$ with a single accepting state. We
introduce a new accepting state $q_{f}$. A naive approach would be to connect
all $q_{i}$ via $\varepsilon$-transitions to $q_{f}$ and vice versa. However,
this approach fails, as $q_{f}$ has no information from which of the accepting
states a run enters and thus does not know which outgoing transitions are
valid such that no invalid shortcuts are created. Hence, we use non-
determinism to guess one accepting state (say $q_{i}$) that is visited
infinitely often to satisfy the prefix-acceptance condition. Additionally, we
introduce one new counter per accepting state to ensure that we only use
transitions related to $q_{i}$.

Formally, let
$\mathcal{A}^{\prime}=(Q\cup\\{q_{f}\\},\Sigma,\Delta^{\prime},\mathcal{E}^{\prime},\\{q_{f}\\},C)$
where

$\displaystyle\Delta^{\prime}=$ $\displaystyle\
\\{(q,a,\mathbf{v}\cdot\mathbf{0}^{k},q^{\prime})\mid(q,a,\mathbf{v},q^{\prime})\in\Delta\\}$
$\displaystyle\cup$ $\displaystyle\
\\{(q,a,\mathbf{v}\cdot\mathbf{e}_{i}^{k},q_{f})\mid(q,a,\mathbf{v},q_{i})\in\Delta,i\leq
k\\}$ $\displaystyle\cup$ $\displaystyle\
\\{(q_{f},a,\mathbf{v}\cdot\mathbf{e}_{i}^{k},q)\mid(q_{i},a,\mathbf{v},q)\in\Delta,i\leq
k\\}$ $\displaystyle\cup$ $\displaystyle\
\\{(q_{f},a,\mathbf{v}\cdot\mathbf{e}_{i}^{k},q_{f})\mid(q_{i},a,\mathbf{v},q_{i})\in\Delta,i\leq
k\\}$

and

$\displaystyle\mathcal{E}^{\prime}=$ $\displaystyle\
\\{(q,\varepsilon,\mathbf{v}\cdot\mathbf{0}^{k},q^{\prime})\mid(q,\varepsilon,\mathbf{v},q^{\prime})\in\mathcal{E}\\}$
$\displaystyle\cup$ $\displaystyle\
\\{(q,\varepsilon,\mathbf{v}\cdot\mathbf{e}_{i}^{k},q_{f})\mid(q,\varepsilon,\mathbf{v},q_{i})\in\mathcal{E},i\leq
k,q\neq q_{i}\\}$ $\displaystyle\cup$ $\displaystyle\
\\{(q_{f},\varepsilon,\mathbf{v}\cdot\mathbf{e}_{i}^{k},q)\mid(q_{i},\varepsilon,\mathbf{v},q)\in\mathcal{E},i\leq
k,q\neq q_{i}\\}$ $\displaystyle\cup$ $\displaystyle\
\\{(q_{f},\varepsilon,\mathbf{v}\cdot\mathbf{e}_{i}^{k},q_{f})\mid(q_{i},\varepsilon,\mathbf{v},q_{i})\in\mathcal{E},i\leq
k\\}.$

Define $C_{i}=C(q_{i})\cdot\\{z\mathbf{e}_{i}^{k}\mid z\in\mathbb{N}\\}$ and
$C=\bigcup_{i\leq k}C_{i}$. We claim that
$P_{\omega}(\mathcal{A})=P_{\omega}(\mathcal{A}^{\prime})$.

To show $P_{\omega}(\mathcal{A})\subseteq P_{\omega}(\mathcal{A}^{\prime})$,
let $\alpha\in P_{\omega}(\mathcal{A})$ with accepting run
$r=r_{1}r_{2}r_{3}\dots$ of $\mathcal{A}$, where
$r_{j}=(p_{j-1},\gamma_{j},\mathbf{v}_{j},p_{j})$. By the infinite pigeonhole
principle, there exists an accepting state $q_{i}$ satisfying the prefix-
acceptance condition infinitely often, i. e., there are infinitely many $j$
such that $p_{j}=q_{i}$ and $\rho(r_{1}\dots r_{j})\in C(q_{i})$. From $r$ we
construct an accepting run
$r^{\prime}=r^{\prime}_{1}r^{\prime}_{2}r^{\prime}_{3}\dots$ of
$\mathcal{A}^{\prime}$ by replacing every transition after reading
$\alpha_{1}$ of the form $(p_{j-1},\gamma_{j},\mathbf{v}_{j},q_{i})$ with
$(p_{j-1},\gamma_{j},\mathbf{v}_{j}\cdot\mathbf{e}^{k}_{i},q_{f})$, every
$(q_{i},\gamma_{j},\mathbf{v}_{j},q_{i})$ with
$(q_{f},\gamma_{j},\mathbf{v}_{j}\cdot\mathbf{e}^{k}_{i},q_{f})$, and every
$(q_{i},\gamma_{j},\mathbf{v}_{j},p_{j})$ with
$(q_{f},\gamma_{j},\mathbf{v}_{j}\cdot\mathbf{e}^{k}_{i},p_{j})$. Finally,
every other transition $(p_{j-1},\gamma_{j},\mathbf{v}_{j},p_{j})$ is replaced
by $(p_{j-1},\gamma_{j},\mathbf{v}_{j}\cdot\mathbf{0}^{k},p_{j})$. By the
choice of $\Delta^{\prime}$ and $\mathcal{E}^{\prime}$ the run $r^{\prime}$ is
indeed a run of $\mathcal{A}^{\prime}$ on $\alpha$. Furthermore, $r^{\prime}$
is accepting, as every accepting hit in $q_{i}$ in $r$ after reading
$\alpha_{1}$ (before reading the first symbol of $\alpha$ it might be the case
that we could not shortcut into $q_{f}$) translates into an accepting hit in
$r^{\prime}$: the first $d$ counter values in both runs are equal at every
position, and by construction, there is only a single non-zero value in the
$i$-th component of the appended $k$-dimensional vector in $r^{\prime}$. Thus,
we have $\rho(r^{\prime}_{1}\dots r^{\prime}_{j})\in C_{i}\subseteq C$
whenever we have $\rho(r_{1}\dots r_{j})\in C(q_{i})$.

To show $P_{\omega}(\mathcal{A})\supseteq P_{\omega}(\mathcal{A}^{\prime})$,
let $\alpha\in P_{\omega}(\mathcal{A}^{\prime})$ with accepting run
$r^{\prime}=r^{\prime}_{1}r^{\prime}_{2}r^{\prime}_{3}\dots$ of
$\mathcal{A}^{\prime}$ where
$r^{\prime}_{j}=(p_{j-1},\gamma_{j},\mathbf{v}_{j},p_{j})$. By construction of
$C$ there is a unique $C_{i}$ such that $\rho(r^{\prime}_{1}\dots
r^{\prime}_{j})\in C_{i}$ for infinitely many $j$. Similar as above, we can
replace every occurrence of $q_{f}$ in $r^{\prime}$ by $q_{i}$ and forget the
additional counters to obtain a valid run $r$ of $\mathcal{A}$ on $\alpha$,
which is accepting as every accepting hit on $q_{f}$ in $r^{\prime}$ then
corresponds to an accepting hit on $q_{i}$ in $r$.

Finally, observe that $\mathcal{A}^{\prime}$ has only non-loop
$\varepsilon$-transitions if $\mathcal{A}$ has only non-loop
$\varepsilon$-transitions, as in this case the first and fourth line of the
definition of $\mathcal{E}^{\prime}$ introduce only $\varepsilon$-loops and
the sets defined in the second and third line are empty. If $\mathcal{A}$ was
a MPPBA, we may consider it as an $\varepsilon$-MPPBA with
$\mathcal{E}^{\prime}=\varnothing$, hence, $\mathcal{A}^{\prime}$ can be seen
as a PPBA in this case. ∎

Observe that we can use a similar trick to convert ($\varepsilon$-)MSPBA and
($\varepsilon$-)MWPBA into equivalent ($\varepsilon$-)SPBA and
($\varepsilon$-)WPBA. However, in general a single accepting state is not
sufficient anymore.

######  Lemma 3.3.

For every $\varepsilon$-MSPBA ($\varepsilon$-MWPBA) $\mathcal{A}$ there exists
an $\varepsilon$-SPBA ($\varepsilon$-WPBA) $\mathcal{A}^{\prime}$ such that
$S_{\omega}(\mathcal{A})=S_{\omega}(\mathcal{A}^{\prime})$
($W_{\omega}(\mathcal{A})=W_{\omega}(\mathcal{A}^{\prime})$). If $\mathcal{A}$
has no non-loop $\varepsilon$-transitions, then $\mathcal{A}^{\prime}$ has no
non-loop $\varepsilon$-transitions and if $\mathcal{A}$ is an MSPBA (MWPBA),
then $\mathcal{A}^{\prime}$ is an SPBA (WPBA).

###### Proof sketch..

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,\mathcal{E},F,C)$ be an
($\varepsilon$-)MSPBA of dimension $d$ and let $F=\\{q_{1},\dots,q_{k}\\}$.
Again, $C\colon F\rightarrow\mathcal{P}(\mathbb{N}^{d})$ is a function
assigning a semi-linear set to each $q\in F$. We construct an equivalent
$(\varepsilon$-)SPBA $\mathcal{A}^{\prime}$ of dimension $d+k$ with a single
semi-linear set $C^{\prime}\subseteq\mathbb{N}^{d+k}$.

The idea is to use the additional counters to mark into which resetting state
we enter, that is, every transition that does not lead to a resetting state is
simply padded with $0$, while every transition entering the resetting state
$q_{i}$ has a $1$ exactly at the $d+i$th position. The semi-linear set
$C^{\prime}$ is defined as $\bigcup_{1\leq i\leq
k}C(q_{i})\cdot\\{\mathbf{e}^{d}_{i}\\}$.

When $\mathcal{A}$ is an $(\varepsilon)$-MWPBA, then additionally, for every
transition entering a resetting state we add the transition padded with $0$.
Then, the resulting automaton can non-deterministically decide if it wants to
reset or not.

Finally, observe that the resulting automaton $\mathcal{A}^{\prime}$ has only
non-loop $\varepsilon$-transitions if $\mathcal{A}$ has only non-loop
$\varepsilon$-transitions. If $\mathcal{A}$ was a MPPBA, we may consider it as
an $\varepsilon$-MPPBA with $\mathcal{E}^{\prime}=\varnothing$, hence,
$\mathcal{A}^{\prime}$ can be seen as a PPBA in this case. ∎

###  3.3 Equivalence of $\varepsilon$-WPBA and $\varepsilon$-SPBA

We now prove that the reset models $\varepsilon$-SPBA and $\varepsilon$-WPBA
define the same class of $\omega$-languages. Furthermore, we can efficiently
convert an $\varepsilon$-SPBA into an $\varepsilon$-WPBA and vice versa.

######  Lemma 3.4.

Every $\varepsilon$-SPBA $\mathcal{A}$ is equivalent to an $\varepsilon$-WPBA
$\mathcal{A}^{\prime}$ that has the same number of states and uses one
additional counter. If $\mathcal{A}$ is an SPBA, then $\mathcal{A}^{\prime}$
is a WPBA.

###### Proof.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,\mathcal{E},F,C)$ be an
$\varepsilon$-SPBA. We construct an equivalent $\varepsilon$-WPBA
$\mathcal{A}^{\prime}$ that simulates $\mathcal{A}$, ensuring that no run
visits an accepting state without resetting. To achieve that, we add an
additional counter that tracks the number of visits of an accepting state
(without resetting). Moreover, we modify $C$ such that this new counter must
be set to 1 when visiting an accepting state, thus disallowing to pass such a
state without resetting.

We choose
$\mathcal{A}^{\prime}=(Q,\Sigma,q_{0},\Delta^{\prime},$$\mathcal{E}$’$F,C^{\prime})$
where

$\displaystyle\Delta^{\prime}=$ $\displaystyle\ \\{(q,x,\mathbf{v}\cdot
0,q^{\prime})\mid(q,x,\mathbf{v},q^{\prime})\in\Delta,q^{\prime}\notin F\\}$
$\displaystyle\cup$ $\displaystyle\ \\{(q,x,\mathbf{v}\cdot
1,q_{f})\mid(q,x,\mathbf{v},q_{f})\in\Delta,q_{f}\in F\\},$

and, similarly,

$\displaystyle\mathcal{E}^{\prime}=$ $\displaystyle\
\\{(q,\varepsilon,\mathbf{v}\cdot
0,q^{\prime})\mid(q,\varepsilon,\mathbf{v},q^{\prime})\in\mathcal{E},q^{\prime}\notin
F\\}$ $\displaystyle\cup$ $\displaystyle\ \\{(q,\varepsilon,\mathbf{v}\cdot
1,q_{f})\mid(q,\varepsilon,\mathbf{v},q_{f})\in\mathcal{E},q_{f}\in F\\}.$

Finally, let $C^{\prime}=C\cdot\\{1\\}$. We claim that $\mathcal{A}^{\prime}$
is an $\varepsilon$-WPBA equivalent to $\mathcal{A}$.

Let $\alpha\in S_{\omega}(\mathcal{A})$. Since $\mathcal{A}$ resets every time
when visiting an accepting state, $\mathcal{A}^{\prime}$ can simulate an
accepting run using the same states and reset positions. In particular, the
new counter will be 1 on every visit of an accepting state. Thus, the choice
of $C^{\prime}$ implies that $\alpha\in W_{\omega}(\mathcal{A}^{\prime})$.

Now, let $\alpha\in W_{\omega}(\mathcal{A}^{\prime})$. Due to the choice of
$C^{\prime}$, it is indispensable for $\mathcal{A}$ to reset the counters
every time an accepting state is visited. Otherwise, the new counter tracking
the number of visits of accepting states would be greater than 1, thus
violating the weak reset-acceptance condition. Hence $\alpha\in
S_{\omega}(\mathcal{A})$. ∎

######  Lemma 3.5.

Every $\varepsilon$-WPBA $\mathcal{A}$ is equivalent to an $\varepsilon$-SPBA
$\mathcal{A}^{\prime}$ with at most twice the number of states and the same
number of counters. If $\mathcal{A}$ is an SPBA, then $\mathcal{A}^{\prime}$
is a WPBA.

###### Proof.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,\mathcal{E},F,C)$ be an
$\varepsilon$-WPBA. We construct an equivalent $\varepsilon$-SPBA
$\mathcal{A}^{\prime}$ that simulates $\mathcal{A}$ by having the option to
“avoid” accepting states arbitrarily long. For this purpose, we create a non-
accepting copy of $F$. Consequently, $\mathcal{A}^{\prime}$ can decide to
continue or reset a partial run using non-determinism.

We choose $\mathcal{A}^{\prime}=(Q\cup\\{\hat{q}_{f}\mid q_{f}\in
F\\},\Sigma,q_{0},\Delta^{\prime},\mathcal{E}^{\prime},F,C)$, where

$\displaystyle\Delta^{\prime}=\Delta\ \cup$ $\displaystyle\
\\{(q,x,\mathbf{v},\hat{q}_{f})\mid(q,x,\mathbf{v},q_{f})\in\Delta,q_{f}\in
F\\}$ $\displaystyle\cup$ $\displaystyle\
\\{(\hat{q}_{f},x,\mathbf{v},q)\mid(q_{f},x,\mathbf{v},q)\in\Delta,q_{f}\in
F\\}$ $\displaystyle\cup$ $\displaystyle\
\\{(\hat{q}_{f},x,\mathbf{v},\hat{q}_{f}^{\prime})\mid(q_{f},x,\mathbf{v},q_{f}^{\prime})\in\Delta,q_{f},q_{f}^{\prime}\in
F\\},$

and similarly,

$\displaystyle\mathcal{E}^{\prime}=\mathcal{E}\ \cup$ $\displaystyle\
\\{(q,\varepsilon,\mathbf{v},\hat{q}_{f})\mid(q,\varepsilon,\mathbf{v},q_{f})\in\mathcal{E},q_{f}\in
F\\}$ $\displaystyle\cup$ $\displaystyle\
\\{(\hat{q}_{f},\varepsilon,\mathbf{v},q)\mid(q_{f},\varepsilon,\mathbf{v},q)\in\mathcal{E},q_{f}\in
F\\}$ $\displaystyle\cup$ $\displaystyle\
\\{(\hat{q}_{f},\varepsilon,\mathbf{v},\hat{q}_{f}^{\prime})\mid(q_{f},\varepsilon,\mathbf{v},q_{f}^{\prime})\in\mathcal{E},q_{f},q_{f}^{\prime}\in
F\\}.$

We claim that $\mathcal{A}^{\prime}$ is an $\varepsilon$-SPBA equivalent to
$\mathcal{A}$.

$\Rightarrow$ We first show $W_{\omega}(\mathcal{A})\subseteq
S_{\omega}(\mathcal{A}^{\prime})$. Let $\alpha\in W_{\omega}(\mathcal{A})$ and
$r=r_{1}r_{2}r_{3}\dots$ be an accepting run of $\mathcal{A}$ on $\alpha$ with
reset positions $k_{0}<k_{1}<k_{2}\dots$. Now $\mathcal{A}^{\prime}$ is able
to simulate $r$ by choosing the state $\hat{q}_{i}$ for every state $q_{i}\in
F$ where $i\neq k_{j},j\geq 1$. Hence, $\mathcal{A}^{\prime}$ visits an
accepting state if and only if $\mathcal{A}$ resets its counters at the same
position. Thus, $\alpha\in S_{\omega}(\mathcal{A}^{\prime})$.

$\Leftarrow$ To see that $S_{\omega}(\mathcal{A}^{\prime})\subseteq
W_{\omega}(\mathcal{A})$, let $\alpha\in S_{\omega}(\mathcal{A}^{\prime})$ and
$r^{\prime}=r_{1}^{\prime}r_{2}^{\prime}r_{3}^{\prime}\dots$, with
$r_{i}^{\prime}=(p_{i-1}^{\prime},\gamma_{i},\mathbf{v}_{i},p_{i}^{\prime})$,
where $p_{i}^{\prime}\in\\{p_{i},\hat{p}_{i}\\}$ for all $i\geq 0$, be a run
of $\mathcal{A}^{\prime}$ on $\alpha$ satisfying the strong reset-acceptance
condition. Then $r=r_{1}r_{2}r_{3}\dots$ with
$r_{i}=(p_{i-1},\gamma_{i},\mathbf{v}_{i},p_{i})$ is a run of $\mathcal{A}$ on
$\alpha$. Furthermore, $r$ satisfies the weak reset-acceptance condition: let
$k_{1},k_{2},\dots$ denote all positions in $r^{\prime}$ where
$p^{\prime}_{f_{i}}$ is accepting. In particular, $k_{1},k_{2},\dots$ are an
infinite number of (possible) reset positions, thus satisfying the weak reset-
acceptance condition. Therefore, $\alpha\in W_{\omega}(\mathcal{A})$. ∎

As a result, we call an $\omega$-language $L$ _Reset-recognizable_ if there is
an SPBA $\mathcal{A}$ such that $S_{\omega}(\mathcal{A})=L$. We write
$\mathcal{L}_{\mathsf{Reset}}$ to denote the class of all Reset-recognizable
languages. Similarly, we call $L$ _Prefix-recognizable_ if there is a PPBA
$\mathcal{A}$, such that $P_{\omega}(\mathcal{A})=L$ and denote the class of
Prefix-recognizable languages by $\mathcal{L}_{\mathsf{Prefix}}$.

##  4 Schnepsilon-elimination

###  4.1 $\varepsilon$-elimination for PPBA

We now show that $\varepsilon$-transitions in $\varepsilon$-PPBA can be
eliminated, that is, every $\varepsilon$-PPBA $\mathcal{A}$ is equivalent to a
PPBA $\mathcal{A}^{\prime}$. We proceed in two steps. In the first step, we
show that we can convert every $\varepsilon$-PPBA into an equivalent
$\varepsilon$-PPBA where all occurring $\varepsilon$-transitions are
$\varepsilon$-loops. In the second step we show how to remove all
$\varepsilon$-loops, thus obtaining a PPBA without $\varepsilon$-transitions.

Let $\Sigma=\\{\sigma_{1},\dots,\sigma_{k}\\}$. The _Parikh image_ of a
(finite) word $w\in\Sigma^{*}$ is the vector
$p(w)=(|w|_{\sigma_{1}},\dots,|w|_{\sigma_{k}})\in\mathbb{N}^{k}$. The
definition extends to languages $L\subseteq\Sigma^{*}$ in the natural way:
$p(L)=\\{p(w)\mid w\in L\\}$. An important ingredient of our proof is (the
first statement of) Parikh’s Theorem [10], stating the following.

######  Theorem 4.1 (Parikh).

For every regular language $L$ the set $p(L)$ is semi-linear.

Let $\Gamma\subseteq\mathbb{N}^{k}$ be finite. For a word $w=w_{1}\ldots
w_{\ell}\in\Gamma^{*}$ we write $\sum w$ for $\sum_{1\leq i\leq
k}w_{i}\in\mathbb{N}^{k}$. For a language $L\subseteq\Gamma^{*}$ we define
$\sum L=\\{\sum w\mid w\in L\\}$. Let
$\Sigma=\\{\sigma_{1},\ldots,\sigma_{k}\\}$ be an alphabet. Let
$\mathcal{X}_{\Sigma}=\\{\mathbf{e}^{k}_{i}\mid 1\leq i\leq
k\\}\subseteq\mathbb{N}^{k}$ be the set of $k$-dimensional unit vectors. Then
Parikh’s Theorem implies that for every regular language $L$ over
$\mathcal{X}_{\Sigma}$ the set $\sum L$ is semi-linear. Klaedtke and Ruess
showed that this statement is true for arbitrary finite alphabets
$\Gamma\subseteq\mathbb{N}^{k}$.

######  Lemma 4.1 (Klaedkte, Ruess, Lemma 5 of [9], rephrased).

Let $\Gamma\subseteq\mathbb{N}^{k}$ be a finite alphabet. Then for every
regular language $L$ over $\Gamma$ the set $\sum L$ is semi-linear.

For an $\varepsilon$-PPBA
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta,\mathcal{E},F,C)$ we define
$\mathcal{A}^{\varepsilon}$ to be the defined as $\mathcal{A}$ where all
non-$\varepsilon$-transitions are removed, that is,
$\mathcal{A}^{\varepsilon}=(Q,\Sigma,q_{0},\varnothing,\mathcal{E},F,C)$.
Furthermore, for $p,q\in Q$ let $\mathcal{A}_{p,q}$ be defined as
$\mathcal{A}$ with initial state $p$ and a single accepting state $q$, i. e.,
$\mathcal{A}_{p,q}=(Q,\Sigma,p,\Delta,\mathcal{E},\\{q\\},C)$. Thus
$\mathcal{A}^{\varepsilon}_{p,q}=(Q,\Sigma,p,\varnothing,\mathcal{E},\\{q\\},C)$.
Let $\mathcal{B}_{p,q}$ the NFA over the alphabet
$\Gamma\subseteq\mathbb{N}^{k}$ obtained from
$\mathcal{A}_{p,q}^{\varepsilon}$ by replacing every labeled
$\varepsilon$-transition with a transition where only the vector remains, that
is, $\mathcal{B}_{p,q}=(Q,\Gamma,\\{p\\},\Delta^{\prime},\\{q\\})$ where
$\Delta^{\prime}=\\{(q_{1},\mathbf{v},q_{2})\mid(q_{1},\varepsilon,\mathbf{v},q_{2})\in\mathcal{E}\\}$.
Then, the following is immediate from Lemma 4.1.

######  Corollary 4.1.

For every $\varepsilon$-PPBA
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta,\mathcal{E},F,C)$ and all $p,q\in Q$, the
set $\sum L(\mathcal{B}_{p,q})$ is semi-linear.

We first show that we may assume that the initial state has no non-loop
$\varepsilon$-transitions.

######  Lemma 4.2.

For every $\varepsilon$-PPBA
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta,\mathcal{E},F,C)$ there is an equivalent
$\varepsilon$-PPBA
$\mathcal{A}^{\prime}=(Q\cup\\{q_{0}^{\prime}\\},\Sigma,q_{0}^{\prime},\Delta^{\prime},\mathcal{E}^{\prime},F,C^{\prime})$
such that all outgoing $\varepsilon$-transitions of $q_{0}^{\prime}$ are
$\varepsilon$-loops.

###### Proof.

We introduce a fresh initial state $q_{0}^{\prime}$. The idea of the proof is
as follows. For every $q\in Q$ reachable from $q_{0}$ by a sequence of
$\varepsilon$-transitions followed by a single transition labeled with a
symbol $a$, we introduce a shortcut labeled with $a$. To account for the
missing $\varepsilon$-transitions we introduce $\varepsilon$-loops on
$q_{0}^{\prime}$, so that the run up to $q$ can be simulated by the
$\varepsilon$-transitions on $q_{0}^{\prime}$ followed by the $a$-shortcut to
$q$. The labels of the new $\varepsilon$-transitions on $q_{0}^{\prime}$ are
given by the automata $\mathcal{B}_{q_{0},q}$. Furthermore, we will use
additional counters to make sure that we do not mix the transitions for
different states $q,q^{\prime}$. We come to the formal details.

For every state $q\in Q$ we consider the set $\sum L(\mathcal{B}_{q_{0},q})$,
which is semi-linear by Corollary 4.1. Note that $\sum
L(\mathcal{B}_{q_{0},q})$ is empty if $q$ is not reachable from $q_{0}$ via
$\varepsilon$-transitions. Otherwise $\sum L(\mathcal{B}_{q_{0},q})$ can be
written as the finite union of linear sets, say $C^{(q)}_{1}\cup\dots\cup
C^{(q)}_{\ell_{q}}$ where
$C^{(q)}_{i}=\\{b_{i,0}^{(q)}+b_{i,1}^{(q)}z_{1}+\dots+b^{(q)}_{i,k_{i,q}}z_{k_{i,q}}\mid
z_{1},\dots,z_{k_{i,q}}\in\mathbb{N}\\}$. We denote by $k_{i,q}$ the number of
period vectors of $C^{(q)}_{i}$, by $\ell_{q}$ the number of linear sets of
the semi-linear set $\sum L(\mathcal{B}_{q_{0},q})$, and define $M=\sum_{q\in
Q}\ell_{q}$. We fix an arbitrary bijection $\pi$ between the $C^{(q)}_{i}$ and
$\\{1,\dots,M\\}$.

We now introduce the new shortcuts and $\varepsilon$-loops on
$q_{0}^{\prime}$. Informally, whenever a run of $\mathcal{A}$ starts with a
sequence of $\varepsilon$-transitions $r_{1}\dots r_{m}r_{m+1}$, where
$r_{1}\dots r_{m}\in\mathcal{E}^{*}$ and
$r_{m+1}=(p_{m},\alpha_{1},\mathbf{v}_{m},p_{m+1})\in\Delta$, the automaton
$\mathcal{A}^{\prime}$ guesses the last state $p_{m}$ of the sequence of
$\varepsilon$-transitions and take a shortcut from $q^{\prime}_{0}$ to
$p_{m+1}$. As $\rho(r_{1}\dots r_{m})\in C^{(p_{m})}_{i}$ for some
$i\leq\ell_{p_{m}}$, the automaton $\mathcal{A}^{\prime}$ also guesses the set
$C^{(p_{m})}_{i}$ and use the $\varepsilon$-loops on $q_{0}^{\prime}$ labeled
with the period vectors of the $C^{(q)}_{i}$ concatenated with a
$0$-$1$-vector of dimension $M$ with a single $1$-entry. These loops replace
all sequences of $\varepsilon$-transitions leaving $q_{0}$ and the new
counters ensure that we do not mix the period vectors of different linear
sets.

Formally, we define $\mathcal{A}^{\prime}$ as follows.

$\displaystyle\Delta^{\prime}=$ $\displaystyle\
\\{(p,a,\mathbf{v}\cdot\mathbf{0}^{M},q)\mid(p,a,\mathbf{v},q)\in\Delta\\}$
$\displaystyle\cup$ $\displaystyle\
\\{(q_{0}^{\prime},a,\mathbf{v}\cdot\mathbf{0}^{M},q)\mid(q_{0},a,\mathbf{v},q)\in\Delta\\}$
$\displaystyle\cup$ $\displaystyle\
\\{(q_{0}^{\prime},a,(\mathbf{v}+b^{(p)}_{i,0})\cdot\mathbf{e}^{M}_{\pi(C^{(p)}_{i})},q)\mid(p,a,\mathbf{v},q)\in\Delta,1\leq
i\leq\ell_{p}\\},$ $\displaystyle\mathcal{E}^{\prime}=$ $\displaystyle\
\\{(p,\varepsilon,\mathbf{v}\cdot\mathbf{0}^{M},q)\mid(p,\varepsilon,\mathbf{v},q)\in\mathcal{E},p\neq
q_{0}\\}$ $\displaystyle\cup$ $\displaystyle\
\\{(q^{\prime}_{0},\varepsilon,b^{(p)}_{i,j}\cdot\mathbf{e}^{M}_{\pi(C^{(p)}_{i})},q^{\prime}_{0})\mid
p\in Q,1\leq i\leq\ell_{p},1\leq j\leq k_{i,q}\\},$

and

$\displaystyle C^{\prime}=C\cdot\\{z\mathbf{e}_{i}^{M}\mid
z\in\mathbb{N},1\leq i\leq M\\}.$

We prove that $\mathcal{A}^{\prime}$ is equivalent to $\mathcal{A}$.

$\Rightarrow$ To show that $P_{\omega}(\mathcal{A})\subseteq
P_{\omega}(\mathcal{A}^{\prime})$, let $\alpha\in P_{\omega}(\mathcal{A})$
with accepting run $r=r_{1}r_{2}r_{3}\dots$ where
$r_{i}=(p_{i-1},\gamma_{i},\mathbf{v}_{i},p_{i})$. We distinguish two cases.

In the first case assume that
$r_{1}=(q_{0},\alpha_{1},\mathbf{v},p_{1})\in\Delta$. In this case we can
simply replace $r_{1}$ by
$r_{1}^{\prime}=(q_{0}^{\prime},\alpha_{1},\mathbf{v}\cdot\mathbf{0},p_{1})$
and continue the run as in $\mathcal{A}$, padding all vectors with zeros. That
is, for $i\geq 2$ let
$r_{i}^{\prime}=(p_{i-1},\gamma_{i},\mathbf{v}_{i}\cdot\mathbf{0}^{M},p_{i})$.
Then $r^{\prime}=r_{1}^{\prime}r_{2}^{\prime}r_{3}^{\prime}$ is a run of
$\mathcal{A}^{\prime}$ on $\alpha$. We show that $r^{\prime}$ is also
accepting. As $r$ is accepting, there are infinitely many $i$ such that
$\rho(r_{1}\dots r_{i})\in C$. As $r^{\prime}$ is basically equal to $r$ (up
to padded zeros), there are infinitely many $i$ such that
$\rho(r_{1}^{\prime}\dots r_{i}^{\prime})\in
C\cdot\\{\mathbf{0}^{M}\\}\subseteq C^{\prime}$, hence $r^{\prime}$ is
accepting.

For the second case assume that $r_{1}\in\mathcal{E}$, i. e., the first
transition of $\mathcal{A}$ is an $\varepsilon$-transition. Let $r_{m}$ be the
last occurrence of the initial $\varepsilon$-sequence, that is, $r_{1}\dots
r_{m}\in\mathcal{E}^{*}$ and
$r_{m+1}=(p_{m},\alpha_{1},\mathbf{v}_{m},p_{m+1})\in\Delta$. Observe that
$\rho(r_{1}\dots r_{m})\in C^{(p_{m})}_{i}$ for some $i\leq\ell_{p_{m}}$,
hence $\rho(r_{1}\dots
r_{m})=b_{i,0}^{(p_{m})}+b_{i,1}^{(p_{m})}z_{1}+\dots+b^{(p_{m})}_{i,k_{i,p_{m}}}z_{k_{i,p_{m}}}$
for some $z_{1},\dots z_{k_{i,p_{m}}}$. As $q_{0}^{\prime}$ is equipped with
$\varepsilon$-loops labeled with the $b_{i,j}^{(p_{m})}$ (concatenated with
$\mathbf{e}^{M}_{\pi(C^{(p_{m})}_{i})}$), $\mathcal{A}^{\prime}$ can sum up
$\rho(r_{1}\dots r_{m})-b_{i,0}^{(p_{m})}$ (with the additional counters) by
taking $z_{1}$ times the transition
$(q_{0}^{\prime},\varepsilon,b^{(p_{m})}_{i,1}\cdot\mathbf{e}^{M}_{\pi(C^{(p_{m})}_{i})},q_{0}^{\prime})$,
$z_{2}$ times the transition
$(q_{0}^{\prime},\varepsilon,b^{(p_{m})}_{i,2}\cdot\mathbf{e}^{M}_{\pi(C^{(p_{m})}_{i})},q_{0}^{\prime})$,
and so on. Finally, we take the shortcut transition
$\hat{r}_{n}=(q_{0}^{\prime},a,(\mathbf{v}+b^{(p_{m})}_{i,0})\cdot\mathbf{e}^{M}_{\pi(C^{(p_{m})}_{i})},p_{m+1})$
to add the missing base vector $b_{i,0}^{(p_{m})}$. From there we can continue
the run as in $\mathcal{A}^{\prime}$ again using the zero-padded transitions.
This yields a run
$r^{\prime}=\hat{r}_{1}\dots\hat{r}_{n-1}\hat{r}_{n}r^{\prime}_{m+1}r^{\prime}_{m+2}\dots$
of $\mathcal{A}^{\prime}$ on $\alpha$ where $\hat{r}_{1}\dots\hat{r}_{n-1}$ is
a sequence of $\varepsilon$-loops, $\hat{r}_{n}$ is the shortcut transition,
and $r^{\prime}_{i}$ for $i\geq m+1$ is defined as in the first case. It
remains to show that $r^{\prime}$ is accepting. First observe that
$\rho(\hat{r}_{1}\dots\hat{r}_{n})\in\\{\rho(r_{1}\dots
r_{m+1})\\}\cdot\\{z\mathbf{e}_{\pi(C^{(p)}_{i})}^{M}\mid z\in\mathbb{N}\\}$
and for all $j\geq m+1$ we have $\rho(r^{\prime}_{m+1}\cdot
r^{\prime}_{j})=\mathbf{v}\cdot\mathbf{0}^{M}$ for some $\mathbf{v}$. Thus,
all (infinitely many) accepting hits of $r$ that occur after $r_{m}$ translate
into accepting hits of $r^{\prime}$, hence $r^{\prime}$ is accepting.
$\lrcorner$

$\Leftarrow$ To show vice versa that
$P_{\omega}(\mathcal{A}^{\prime})\subseteq P_{\omega}(\mathcal{A})$, let
$\alpha\in P_{\omega}(\mathcal{A}^{\prime})$ with accepting run
$r^{\prime}=r^{\prime}_{1}r^{\prime}_{2}r^{\prime}_{3}\dots$ where
$r^{\prime}_{i}=(p_{i-1},\gamma_{i},\mathbf{v}_{i}\cdot\mathbf{u}_{i},p_{i})$
for $\mathbf{u}_{i}\in\\{z\mathbf{e}_{i}^{M}\mid z\in\\{0,1\\},1\leq i\leq
M\\}$. Again we distinguish two cases.

In the first case assume that $r^{\prime}_{1}$ is of the form
$(q_{0}^{\prime},a,\mathbf{v}\cdot\mathbf{0}^{M},p_{1})$. By construction we
have $p_{1}\neq q_{0}^{\prime}$. In particular, we have $p_{i}\neq
q_{0}^{\prime}$ for all $i\geq 1$. Hence, we can replace $r^{\prime}_{1}$ by
$r_{1}=(q_{0},a,\mathbf{v},p_{1})$ and all $r^{\prime}_{i}$ by
$r_{i}=(p_{i-1},a,\mathbf{v}_{i},p_{i})$ for $i\geq 2$. Then the run
$r_{1}r_{2}r_{3}\dots$ is an accepting run of $\mathcal{A}$ on $\alpha$.

In the second case assume that $r^{\prime}_{1}$ is not of the form mentioned
above. Then there is a (unique) $m\geq 1$ such that $r^{\prime}_{m}$ is of the
form $(q_{0}^{\prime},\alpha_{1},\mathbf{v}\cdot\mathbf{e}_{j}^{M},p_{m})$ for
some $j\leq M$. Let $C^{(q)}_{i}$ be the set with $\pi(C^{(q)}_{i})=j$ (which
is uniquely determined as $\pi$ is a bijection). In particular, for all $k\geq
1$ we have $\rho(r^{\prime}_{1}\dots r^{\prime}_{k})=\mathbf{u}\cdot
z\mathbf{e}_{j}^{M}$ for some $z\in\mathbb{N}$ by the choice of $C^{\prime}$.
Hence, we can replace $r^{\prime}_{1}\dots r^{\prime}_{m}$ by a sequence of
$\varepsilon$-transitions $r_{1}\dots r_{n}$ in $\mathcal{A}$ such that
$r_{1}=(q_{0},\varepsilon,\mathbf{v}_{1},p_{1})$,
$r_{n}=(p_{n-1},\varepsilon,\mathbf{v}_{n},q)$ and $\rho(r_{1}\dots r_{n})\in
C^{(q)}_{i}$. Let $r_{n+1}=(q,\alpha_{1},\mathbf{v},p_{m})$ where $\mathbf{v}$
is the vector on $r^{\prime}_{m}$. Note that $r_{n+1}\in\Delta$ by
construction. Then $r_{1}\dots r_{n}r_{n+1}r_{m+1}r_{m+2}\ldots$ where
$r_{i}=(p_{i-1},\gamma_{k},\mathbf{v}_{i},p_{i})$ for all $i\geq m+1$ is a
valid run of $\mathcal{A}$ on $\alpha$. Furthermore, if
$\rho(r_{1}^{\prime},\ldots,r_{i}^{\prime})=\mathbf{u}\cdot
z\mathbf{e}_{j}^{M}$ for some $i\geq m+1$, then
$\rho(r_{1},\ldots,r_{n+1}r_{m+1},\ldots,r_{i})=\mathbf{u}$. Since
$r^{\prime}$ is accepting we conclude that $r$ is accepting. ∎

######  Lemma 4.3.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,\mathcal{E},F,C)$ be an
$\varepsilon$-PPBA of dimension $d$. There is an equivalent $\varepsilon$-PPBA
$\mathcal{A}^{\prime}$ where all $\varepsilon$-transitions are
$\varepsilon$-loops.

###### Proof.

By Lemma 3.2 we may assume that $\mathcal{A}$ has only a single accepting
state $f$, that is, $F=\\{f\\}$, and by Lemma 4.2 we may assume that all
outgoing $\varepsilon$-transitions of the initial state are
$\varepsilon$-loops.

In the beginning,
$\mathcal{A}^{\prime}=(Q^{\prime},\Sigma,q_{0}^{\prime},\Delta^{\prime},\mathcal{E}^{\prime},F^{\prime},C^{\prime})$
is a copy of $\mathcal{A}$, which will be modified step-by-step. First, we
remove all non-loop $\varepsilon$-transitions from $\mathcal{A}^{\prime}$.

The intuition for the construction is as follows. We introduce new states such
that in every run of $\mathcal{A}$ on an infinite word we can replace every
maximal partial run $r_{i}\dots r_{j}$ of $\varepsilon$-transitions, where
$r_{i-1}=(p_{i-2},\alpha_{z-1},\mathbf{v}_{i-1},p_{i-1}),r_{i}=(p_{i-1},\varepsilon,\mathbf{v}_{i},p_{i}),r_{j}=(p_{j-1},\varepsilon,\mathbf{v}_{j},p_{j})$,
and $r_{j+1}=(p_{j},\alpha_{z},\mathbf{v}_{j+1},p_{j+1})$, by a sequence of
$\varepsilon$-loops on a new state depending on $p_{i-1},p_{j}$, and $\sum
L(\mathcal{B}_{p_{i-1},p_{j}})$. The (finite) partial run $r_{i}\dots r_{j}$
translates into an accepting run in $\mathcal{B}_{p_{i-1},p_{j}}$, thus
$\rho(r_{i}\dots r_{j})\in\sum L(\mathcal{B}_{p_{i-1},p_{j}})$. By Corollary
4.1 the set $\sum L(\mathcal{B}_{p_{i-1},p_{j}})$ is semi-linear and hence a
finite union of linear sets, each defined by a base vector and a set of period
vectors, we can encode the period vectors as $\varepsilon$-loops and shortcut
the base vector. Some care must be taken if we visit the accepting state $f$
in the partial run $r_{i}\dots r_{j}$.

Let us continue with the formal construction. We iterate through all pairs
$p,q$ of states. If $L(\mathcal{B}_{p,q})=\varnothing$, we do nothing and
continue with the next pair of states. Otherwise, the state $q$ is reachable
from $p$ in $\mathcal{B}_{p,q}$ and $\sum L(\mathcal{B}_{p,q})$ is non-empty
and can be written as the finite union of linear sets. For the sake of
readability we assume that $\sum L(\mathcal{B}_{p,q})=C_{p,q}$ is a single
linear set. For the general case we apply the following construction
independently for each of the linear sets in the union. In the following, for
any pair of states $s,t$ we denote by $b_{s,t}$ the base vector of $C_{s,t}$.

We add a new state $(p,q)$ to the new state set $Q^{\prime}$ (the new state is
the tuple of states $p$ and $q$). If
$C_{p,q}=\\{b_{p,q}+b_{1}z_{1}+\dots+b_{k}z_{k}\mid
z_{1},\dots,z_{k}\in\mathbb{N}\\}$ we add $\varepsilon$-loops labeled with the
period vectors $b_{1},\dots,b_{k}$ of $C_{p,q}$ to the state $(p,q)$. Finally,
we add _shortcuts_ to $(p,q)$, that is, for every transition of the form
$(s,a,\mathbf{v},p)\in\Delta$ we add a transition
$(s,a,\mathbf{v}+b_{p,q},(p,q))$ to $\Delta^{\prime}$ (note that we add the
base vector $b_{p,q}$ of $C_{p,q}$ to $\mathbf{v}$). Likewise, for every
transition of the form $(q,a,\mathbf{v},s)\in\Delta$ we add a transition
$((p,q),a,\mathbf{v},s)$ to $\Delta^{\prime}$. Finally, we connect the new
states by further adding transitions $((p,q),a,\mathbf{v}+b_{s,t},(s,t))$ to
$\Delta^{\prime}$ for every transition $(q,a,\mathbf{v},s)\in\Delta$ and $t\in
Q$ such that $(s,t)\in Q^{\prime}$ (again assuming that $C_{s,t}$ is linear;
otherwise, we would have multiple copies of $(s,t)$, each of which gets
connected by a transition as above.).

After the exhaustive application of this procedure $\mathcal{A}^{\prime}$ can
simulate every run of $\mathcal{A}$ in the sense that all
$\varepsilon$-transitions that appear in $\mathcal{A}$ have been reduced to a
number of new states equipped with $\varepsilon$-loops. However, if the
accepting state $f$ is reachable from $p$ in $\mathcal{B}_{p,q}$ we must take
into account that the procedure above might have shortcut the accepting state,
which leads to missing accepting hits. To prevent this, we need to add
additional new states.

We iterate over all pairs of states $p,q\in Q$ again. However, this time we
consider the automata $\mathcal{A}_{p,f}^{\varepsilon}$ and
$\mathcal{A}_{f,q}^{\varepsilon}$. As above, let $\mathcal{B}_{p,f}$ and
$\mathcal{B}_{f,q}$ be the NFA whose alphabets are subsets of $\mathbb{N}^{d}$
obtained from $\mathcal{A}_{p,f}^{\varepsilon}$, resp.
$\mathcal{A}_{f,q}^{\varepsilon}$ by keeping only the vectors of the
$\varepsilon$-transitions. By Corollary 4.1 the sets $\sum
L(\mathcal{B}_{p,f})$ and $\sum L(\mathcal{B}_{f,q})$ are semi-linear.

If both of these sets are non-empty, we can write each of them as a finite
union of linear sets. Again, for the sake of readability, we assume that $\sum
L(\mathcal{B}_{p,f})=C_{p,f}$ and $\sum L(\mathcal{B}_{f,q})=C_{f,q}$ are
linear sets. For the general case, we apply the following construction for
every combination of a linear set of $L(\mathcal{B}_{p,f})$ with a linear set
of $L(\mathcal{B}_{f,q})$ independently.

Let $C_{p,f}=\\{b_{p,f}+b_{1}z_{1}+\dots+b_{k}z_{k}\mid
z_{1},\dots,z_{k}\in\mathbb{N}\\}$ and
$C_{f,q}=\\{b_{f,q}+c_{1}z_{1}+\dots+c_{\ell}z_{\ell}\mid
z_{1},\dots,z_{\ell}\in\mathbb{N}\\}$. We add a new accepting state $(p,f,q)$
to $Q^{\prime}$ and equip it with $\varepsilon$-loops labeled with the period
vectors $b_{1},\dots,b_{k}$ of $C_{p,f}$. Furthermore, for each transition of
the form $(r,a,\mathbf{v},p)\in\Delta$ we add a shortcut
$(r,a,\mathbf{v}+b_{p,f},(p,f,q))$ to $\Delta^{\prime}$.

Let us now connect the $(p,q)$-states to the states just introduced. For every
transition $(q,a,\mathbf{v},s)\in\Delta$ we add the ingoing transitions
$((p,q),a,\mathbf{v}+b_{s,f},(s,f,t))$ for all $t\in Q$ to $\Delta^{\prime}$.

In the next step we introduce the outgoing transitions of the
$(p,f,q)$-states. Unfortunately, this situation is more complicated and we
have to introduce yet more states $(p,f,q,s)$ and $(p,f,q,s,t)$. The idea is
that these states act like a copy of $s$ resp. $(s,t)$, but are additionally
equipped with the $\varepsilon$-loops labeled with the period vectors of
$C_{f,q}$. We cannot simply add these loops to $(p,f,q)$, as this might lead
to accepting hits in $\mathcal{A}^{\prime}$ that are not possible in
$\mathcal{A}$ by using these loops (which are for vectors of
$\varepsilon$-sequences _leaving_ $f$). We cannot simply ignore them either,
as they are necessary to simulate the runs of $\mathcal{A}$ appropriately.
Hence the copies, which allow us to use the loops without generating false
accepting hits.

Formally, we insert a new state $(p,f,q,s)$ for all $p,q,s\in Q$ and a new
state $(p,f,q,s,t)$ for all $p,q\in Q$ and $(s,t)\in Q^{\prime}$. For every
transition $(q,a,\mathbf{v},s)\in\Delta$ we add the following transitions to
$\Delta^{\prime}$: $((p,f,q),a,\mathbf{v}+b_{f,q},(p,f,q,s))$, and
$((p,f,q),a,\mathbf{v}+b_{f,q}+b_{s,t},(p,f,q,s,t))$ for all $t\in Q$ such
that there exists $(s,t)\in Q^{\prime}$.

Finally, we connect the new states $(p,f,q,s)$ and $(p,f,q,s,t)$ as follows.
First, $(p,f,q,s)$ and $(p,f,q,s,t)$ are equipped with $\varepsilon$-loops
labeled with the period vectors of $C_{f,q}$. Furthermore, $(p,f,q,s)$ has all
outgoing transitions of $s$, that is, for every transition
$(s,a,\mathbf{v},t)\in\Delta^{\prime}$ we also add a transition
$((p,f,q,s),a,\mathbf{v},t)$ to $\Delta^{\prime}$. Similarly, $(p,f,q,s,t)$
gets all outgoing transitions of $(s,t)$ in $\Delta^{\prime}$. Additionally,
$(p,f,q,s,t)$ gets all $\varepsilon$-loops of $(s,t)$.

Now, all remaining $\varepsilon$-transitions of $\mathcal{A}^{\prime}$ are
loops and we have finished the construction of $\mathcal{A}^{\prime}$.
$\hfill\lrcorner$

We prove that $\mathcal{A}^{\prime}$ is equivalent to $\mathcal{A}$. In the
following, by an $\varepsilon$-sequence we mean a maximal sequence of
$\varepsilon$-transitions containing at least one non-loop
$\varepsilon$-transition.

$\Rightarrow$ To show that $P_{\omega}(\mathcal{A})\subseteq
P_{\omega}(\mathcal{A}^{\prime})$, let $\alpha\in P_{\omega}(\mathcal{A})$
with accepting run $r=r_{1}r_{2}r_{3}\dots$. If there are no
$\varepsilon$-sequences in $r$ we are done (as $r$ is also a run of
$\mathcal{A}^{\prime}$ on $\alpha$).

Otherwise, we construct an accepting run $r^{\prime}$ of
$\mathcal{A}^{\prime}$ on $\alpha$ by replacing $\varepsilon$-sequences step-
by-step. Let $i$ be minimal such that $r_{i}\dots r_{j}$ is an
$\varepsilon$-sequence. Note that because $q_{0}$ has no non-loop
$\varepsilon$-transitions we have $i>1$. Let
$r_{i-1}=(p_{i-2},\alpha_{z-1},\mathbf{v}_{i-1},p_{i-1})$,
$r_{i}=(p_{i-1},\varepsilon,\mathbf{v}_{i},p_{i}),r_{j}=(p_{j-1},\varepsilon,\mathbf{v}_{j},p_{j})$,
and $r_{j+1}=(p_{j},\alpha_{z},\mathbf{v}_{j+1},p_{j+1})$. Similarly, let
$k>j$ be minimal such that $r_{k}\dots r_{\ell}$ is an $\varepsilon$-sequence,
that is, $r_{k}\dots r_{\ell}$ is the second $\varepsilon$-sequence in $r$ (it
might be the case that such $k$ does not exist, we handle this case explicitly
below). Note that we have $\rho(r_{i}\dots r_{j})\in\sum L(B_{p_{i-1},p_{j}})$
and $\rho(r_{k}\dots r_{\ell})\in\sum L(B_{p_{k-1},p_{\ell}})$.

We distinguish the (combination of the) following cases.

  * 1.

There is $f_{1}$ with $i\leq f_{1}\leq j$ such that we have an accepting hit
in $r_{f_{1}}$ (F) or not (N). Recall that we have only one accepting state
$f$ and $f_{1}$ here denotes the position of the accepting hit.

  * 2.

We have $k=j+2$, that is, there is just a single non-$\varepsilon$-transition
between the two sequences $r_{i}\dots r_{j}$ and $r_{k}\dots r_{\ell}$ (1) or
$k>j+2$, that is, there are at least two non-$\varepsilon$-transitions between
the two sequences (2).

  * 3.

There is $f_{2}$ with $k\leq f_{2}\leq\ell$ such that we have an accepting hit
in $r_{f_{2}}$ (F) or not, or $k$ does not even exist (N).

Hence, we consider eight cases in total.

$\bullet$ Case (F1N). This means we need to take care of an accepting hit in
the first $\varepsilon$-sequence (at position $f_{1}$), but not in the second
$\varepsilon$-sequence (here we assume that the second sequence exists, the
other case is handled in (F2N)), and there is just a single
non-$\varepsilon$-transition between these sequences.

We replace $r_{i-1}$ by
$\hat{r}_{i-1}=(p_{i-2},\alpha_{z-1},\mathbf{v}_{i-1}+b_{p_{i-1},f},(p_{i-1},f,p_{j}))\in\Delta^{\prime}$.
As there is an accepting hit at position $f_{1}$, we have $\rho(r_{1}\dots
r_{f_{1}})=\rho(r_{1}\dots r_{i-1})+\rho(r_{i}\dots r_{f_{1}})\in C$. In
particular, we have $\rho(r_{i}\dots r_{f_{1}})\in C_{p_{i-1},p_{f_{i}}}$. By
construction, there are $\varepsilon$-loops on $(p_{i-1},f,p_{j})$ labeled
with the period vectors of $C_{p_{i-1},p_{f_{i}}}$. Hence, we can replace
$r_{i}\dots r_{f_{1}}$ by a sequence of $\varepsilon$-loops
$\hat{r}_{i}\dots\hat{r}_{m}$ on $(p_{i-1},f,p_{j})$ with
$\rho(\hat{r}_{i}\dots\hat{r}_{m})=\rho(r_{i}\dots r_{f_{1}})-b_{p_{i-1},f}$.
As $b_{p_{i-1},f}$ has already been added to $\hat{r}_{i-1}$, the sequence
$\hat{r}=r_{1}\dots r_{i-2}\hat{r}_{i-1}\hat{r}_{i}\dots\hat{r}_{m}$ is a
prefix of a run of $\mathcal{A}^{\prime}$ on $\alpha$ with $\rho(\hat{r})\in
C$.

We describe how to continue the run at this point. We take the transition
$\hat{r}_{m+1}=((p_{i-1},f,p_{j}),\alpha_{z},\mathbf{v}_{j+1}+b_{f,p_{j}}+b_{p_{j+1},p_{\ell}},(p_{i-1},f,p_{j},p_{j+1},p_{\ell}))\in\Delta$
(recall that $p_{j+1}=p_{k-1}$). As $(p_{i-1},f,p_{j},p_{j+1},p_{\ell})$ is
equipped with $\varepsilon$-loops labeled with the period vectors of
$C_{f,p_{j}}$ and also with the period vectors of $C_{j+1,\ell}$, we can
replace the partial run $r_{m+1}\ldots r_{j}$ with a sequence of
$\varepsilon$-loops $\hat{r}_{m+2}\dots\hat{r}_{n}$ on
$(p_{i-1},f,p_{j},p_{j+1},p_{\ell})$ with
$\rho(\hat{r}_{f_{1}+1}\dots\hat{r}_{j})=\rho(r_{f_{1}+1}\dots
r_{j})-b_{f,p_{j}}$ and the partial run $r_{j+2}\ldots r_{\ell}$ with a
sequence of $\varepsilon$-loops $\hat{r}_{n+1}\dots\hat{r}_{o}$ on
$(p_{i-1},f,p_{j},p_{j+1},p_{\ell})$ with
$\rho(\hat{r}_{j+2}\dots\hat{r}_{\ell})=\rho(r_{j+2}\dots
r_{\ell})-b_{p_{j+1},p_{\ell}}$. As $b_{p_{j+1},p_{\ell}}$ and $b_{f,p_{j}}$
have already been added to $\hat{r}_{m+1}$, the partial run
$\hat{r}_{1}\dots\hat{r}_{m}\dots\hat{r}_{n}\dots\hat{r}_{o}$ is equivalent to
$r_{i}\dots r_{\ell}$ in the sense that both runs have (at least) one
accepting hit, read $\alpha_{z-1}\alpha_{z}$, have the same extended Parikh
image, and ”fit” into the whole run $r$, as $(p_{i-1},f,p_{j},p_{j+1},p_{l})$
has the same outgoing transitions (including possible shortcuts) as $p_{l}$.

We now continue with the next $\varepsilon$-sequence in $r$.

$\bullet$ Case (F1F). We do the exact same replacement as in (F1N). We thereby
lose an accepting hit in the second sequence, however, this is not a problem,
as we still have an accepting hit in the first sequence and we have infinitely
many accepting hits to come.

$\bullet$ Case (F2N). This is similar to (F1N) but we chose
$\hat{r}_{m+1}=((p_{i-1},f,p_{j}),\alpha_{z},\mathbf{v}_{j+1}+b_{f,p_{j}},(p_{i-1},f,p_{j},p_{j+1}))$.
As we do not need to consider the set $C_{k,\ell}$ at this point, we just
replace $r_{f_{1}+1}\dots r_{j}$ by a matching sequence $r_{m+2}\dots r_{n}$
of $\varepsilon$-loops on $(p_{i-1},f,p_{j},p_{j+1})$.

At this point, we continue as if we were in $p_{j+1}$. Note that we are done
if the second sequence does not exist.

$\bullet$ Case (F2F) is the same as (F2N).

$\bullet$ Case (N1F). Here we replace $r_{i-1}$ by
$\hat{r}_{i-1}=(p_{i-2},\alpha_{z-1},\mathbf{v}_{i}+b_{p_{i-1},p_{j}},(p_{i-1},p_{j}))\in\Delta^{\prime}$.
As $\rho(r_{i}\dots r_{j})\in C_{p_{i-1},p_{j}}$, we can replace this partial
run by a sequence of $\varepsilon$-loops $\hat{r}_{i}\dots\hat{r}_{m}$ on
$(p_{i-1},p_{j})$ with $\rho(\hat{r}_{i}\dots\hat{r}_{m})=\rho(r_{i}\dots
r_{j})-b_{p_{i-1},p_{j}}$. As $b_{p_{i-1},p_{j}}$ has already been added to
$\hat{r}_{i-1}$, the sequence $\hat{r}_{i-1}\hat{r}_{i}\dots\hat{r}_{m}$ is
equivalent to $r_{i-1}r_{i}\dots r_{j}$ in the sense that both runs read
$\alpha_{z-1}$, have the same Parikh images and fit into the whole run $r$, as
we can continue the run from $(p_{i},p_{j})$ in exactly the same way as in
$p_{j}$, hence we continue with the next $\varepsilon$-sequence.

$\bullet$ The remaining cases (N1N), (N2F) and (N2N) are the same as (N1F).

All accepting hits outside of $\varepsilon$-sequences translate one-to-one.
This finishes the proof of the forward direction. $\hfill\lrcorner$

$\Leftarrow$ To show that $P_{\omega}(\mathcal{A}^{\prime})\subseteq
P_{\omega}(\mathcal{A})$, let $\alpha\in P_{\omega}(\mathcal{A}^{\prime})$
with accepting run
$r^{\prime}=r^{\prime}_{1}r^{\prime}_{2}r^{\prime}_{3}\dots$. If all states
that appear in $r$ belong to the state set $Q$ of $\mathcal{A}$, we are done
as the run is also an accepting run of $\mathcal{A}$.

Otherwise, we construct an accepting run $r$ of $\mathcal{A}$ on $\alpha$
step-by-step. Let $i$ be minimal such that
$r^{\prime}_{i}=(p^{\prime}_{i-1},\alpha_{z},\mathbf{v}^{\prime}_{i},p^{\prime}_{i})$
contains a state that is not part of $Q$. As all (accepting) runs of
$\mathcal{A}^{\prime}$ start in $q_{0}$ (which belongs to $Q$), we have that
$p^{\prime}_{i}\notin Q$. We distinguish two cases.

If $p^{\prime}_{i}=(s,t)$ for some $s,t\in Q$, we have
$\mathbf{v}_{i}^{\prime}=\mathbf{v}_{i}+b_{s,t}$ by the choice of
$\Delta^{\prime}$. Let $j\geq i$ be maximal such that for all $i\leq k\leq j$
we have that $r^{\prime}_{k}$ is an $\varepsilon$-loop on $(s,t)$, i. e., of
the form $((s,t),\varepsilon,\mathbf{v}_{k}^{\prime},(s,t))$.

By the semantics of $(s,t)$, there is an $\varepsilon$-sequence $r_{i}\dots
r_{n}$ in $\mathcal{A}$ that starts in $s$ and ends in $t$. To be precise, we
have $r_{i}=(s,\varepsilon,\mathbf{v}_{i},p_{i})$ and
$r_{n}=(p_{n-1},\varepsilon,\mathbf{v}_{n},t)$, and there is a transition
$r_{i-1}=(p_{i-2},\alpha_{z},\mathbf{v}_{i},s)\in\Delta$ such that
$\mathbf{v}_{i}=\mathbf{v}_{i}^{\prime}$ and hence $\rho(r_{i-1}r_{i}\dots
r_{n})=\rho(r^{\prime}_{i}\dots r^{\prime}_{j})$. Furthermore, observe that
$p_{i-2}=p^{\prime}_{i-1}$, hence $r_{i-1}r_{i}\dots r_{n}$ is equivalent to
$r^{\prime}_{i}\dots r^{\prime}_{j}$ in the sense that both runs read
$\alpha_{z}$, have the same extended Parikh images, and fit into the whole run
$r^{\prime}$ as we can continue the run from $t$ exactly the same way as in
$(s,t)$.

If $p^{\prime}_{i}=(s,f,t)$ for some $s,t\in Q$, we have
$\mathbf{v}_{i}^{\prime}=\mathbf{v}_{i}+b_{s,f}$ by the choice of
$\Delta^{\prime}$. Let $j\geq i$ be maximal such that for all $i\leq k\leq j$
we have that $r^{\prime}_{k}$ is an $\varepsilon$-loop on $(s,f,t)$, i. e.,
$r^{\prime}_{k}$ is a transition of the form
$((s,f,t),\varepsilon,\mathbf{v}_{k}^{\prime},(s,f,t))$ and there is an
accepting hit in $r_{j}^{\prime}$ (if there is no accepting hit, let $j$ be
the last $\varepsilon$-loop in this sequence).

By the semantics of $(s,f,t)$ there is an $\varepsilon$-sequence $r_{i}\dots
r_{m}\dots r_{n}$ in $\mathcal{A}$ that starts in $s$, visits $f$, and ends in
$t$. To be precise, we have $r_{i}=(s,\varepsilon,\mathbf{v}_{i},p_{i})$,
$r_{m}=(p_{m-1},\varepsilon,\mathbf{v}_{m},f)$,
$r_{n}=(p_{n-1},\varepsilon,\mathbf{v}_{n},t)$, and there is a transition
$r_{i-1}=(p_{i-2},\alpha_{z},\mathbf{v}_{i},s)\in\Delta$ such that
$\mathbf{v}_{i}=\mathbf{v}_{i}^{\prime}$. In particular, if there is an
accepting hit in $r^{\prime}_{j}$, we can choose $m$ such that
$\rho(r_{i-1}r_{i}\dots r_{m})=\rho(r_{i}^{\prime}\dots r^{\prime}_{j})$,
hence there is also an accepting hit in $r_{m}$. By the choice of
$\Delta^{\prime}$, $r^{\prime}_{j}$ is followed by a (possibly empty) sequence
of $\varepsilon$-loops on $(s,f,t)$, followed by a transition of the form
$\delta_{1}=((s,f,t),\alpha_{z+1},\mathbf{v}+b_{f,t},(s,f,t,p))$ or
$\delta_{2}=((s,f,t),\alpha_{z+1},\mathbf{v}+b_{f,t}+b_{p,q},(s,f,t,p,q))$ for
some $p,q\in Q$. This sequence of $\varepsilon$-loops on $(s,f,t)$ matches to
a sequence of $\varepsilon$-transitions in $\mathcal{A}$ that starts and ends
in $f$ with the same extended Parikh image, hence we replace it accordingly.

We now consider the next transition. In the first case we assume that it is of
the form $\delta_{1}$. Recall that $(s,f,t,p)$ is equipped with several
$\varepsilon$-loops labeled with the period vectors of $C_{f,t}$, as well with
possible $\varepsilon$-loops of $p$ in $\mathcal{A}$. This means that the
transition is followed by a possibly empty sequence of $\varepsilon$-loops on
$(s,f,t,p)$. Without loss of generality we assume that they are ordered in
such a way that first all $\varepsilon$-loops labeled with period vectors
appear, say $\hat{r}_{1}\dots\hat{r}_{o}$, followed by possible
$\varepsilon$-loops of $p$ (this is not a problem, as we just swap
$\varepsilon$-loops and do not need to take care of any accepting hits as
$(s,f,t,p)$ is non-accepting). By construction we have
$\rho(\hat{r}_{1}\dots\hat{r}_{o})=\rho(r_{m+1}\dots r_{n})-b_{f,t}$. As
$b_{f,t}$ has already been added to $\delta_{1}$, we replace
$\delta_{1}\hat{r_{1}}\dots\hat{r}_{o}$ by $r_{m+1}\dots r_{n}r_{n+1}$ where
$r_{n+1}=(t,\alpha_{z+1},\mathbf{v},p)$. As $p$ is equipped with all outgoing
transitions of $(s,f,t,p)$ (including possible $\varepsilon$-loops, but no
other $\varepsilon$-transitions), we can continue the run in $\mathcal{A}$ the
same way as in $\mathcal{A}^{\prime}$.

Finally, we assume that the next transition is of the form $\delta_{2}$. This
case is similar, with the only exception that $(s,f,t,p,q)$ ”behaves” like
$(p,q)$ in the sense that $(s,f,t,p,q)$ has all outgoing transitions of
$(p,q)$. Thus, we continue from here as in the first case, where we handle
states of this form.

Again, all accepting hits using states in $Q$ translate one-to-one. This
finishes the proof of the backward direction. ∎

We now proceed to eliminate the remaining $\varepsilon$-loops. We need the
following lemma for $\varepsilon$-elimination for automata on finite words.

######  Lemma 4.4.

[Theorem 22 of Klaedtke and Ruess [9], reformulated] For every PA
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ of dimension $d$ _on finite words_
(with $\varepsilon$-transitions) there exists an equivalent $\varepsilon$-free
PA $\hat{}\mathcal{A}=(Q,\Sigma,q_{0},\hat{\Delta},F,\hat{C})$ on the same
state set of dimension $d+|Q|-1$.

######  Lemma 4.5.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,\mathcal{E},F,C)$ be an
$\varepsilon$-PPBA of dimension $d$ where all occuring
$\varepsilon$-transitions are $\varepsilon$-loops. There is an equivalent PPBA
$\mathcal{A}^{\prime}$.

###### Proof.

Let us first sketch the proof idea. Intuitively, we will split the automaton
into two parts. We will guess the set $S$ of states that will be seen
infinitely often. In the first part of the automaton we will deal with the set
of states that are seen only finitely often. For this, we apply the
construction of Lemma 4.4 and make all accepting states non-accepting to
obtain the automaton $\hat{}\mathcal{A}$. We non-deterministically switch to
the second part, where we will verify that for some set $S\subseteq Q$ exactly
the states of $S$ will be seen infinitely often. We follow the idea of
Klaedtke and Ruess [9] for finite words: Since it does not matter when and in
what order vectors are added, we can simulate $\varepsilon$-loops by an
appropriate modification of the semi-linear set. Instead of
$\varepsilon$-looping on a state we can intuitively “substract” the semi-
linear set corresponding to the loop from $C$. Formally, we will construct an
automaton $\mathcal{A}_{S}$ for each possible guess of $S$ and shortcut
appropriately from $\hat{}\mathcal{A}$. We will work with one semi-linear set
for each $\mathcal{A}_{S}$, so that we formally construct an MPPBA. We
conclude by applying Lemma 3.2 to translate this automaton finally to an
equivalent PPBA. Let us come to the formal proof.

By Lemma 3.2 we may assume that $\mathcal{A}$ has only a single accepting
state, say $F=\\{f\\}$. We first interpret $\mathcal{A}$ as a PA on finite
words and denote by $\hat{}\mathcal{A}$ the $\varepsilon$-free automaton
obtained from Lemma 4.4 by padding every vector with $d$-many zeros (that is
$\hat{}\mathcal{A}$ is of dimension $2d+|Q|-1$ instead of $d+|Q|-1$). We
denote the semi-linear set of $\hat{}\mathcal{A}$ by $\hat{C}$.

Now, for every non-empty subset of states $S\subseteq Q$ containing at least
$f$, we construct an MPPBA $\mathcal{A}_{S}$ of dimension $d$, as follows. Let
the states of $S$ be ordered arbitrarily, say $S=\\{s_{1},\dots,s_{m}\\}$. $S$
is a candidate set for the set consisting exactly of those states that will be
visited infinitely often. We connect $\hat{}\mathcal{A}$ to all
$\mathcal{A}_{S}$ by shortcutting all transitions in $\hat{}\mathcal{A}$ that
lead to $f$ to the initial states of the $\mathcal{A}_{S}$. In this way we can
non-deterministically switch from $\hat{}\mathcal{A}$ to some
$\mathcal{A}_{S}$.

The automaton $\mathcal{A}_{S}$ consists of $m+1$ copies of $\mathcal{A}$ as
well as a fresh state $q_{S}$, which is the initial state of
$\mathcal{A}_{S}$, as well as the only accepting state of $\mathcal{A}_{S}$.
In the following, we call the $i$th copy of $\mathcal{A}_{S}$ the $i$th
_layer_ of $\mathcal{A}_{S}$. By allowing to switch from the $i$th layer to
the $(i+1)$st layer only after visiting state $s_{i}$, the $m$ layers ensure
that we visit all of the states $s_{1},\dots,s_{m}$ infinitely often. From the
last layer we have shortcuts into the new state $q_{S}$, allowing us to ”wait”
for the point where the next transition would bring us to $f$ and the counters
to a value in the semi-linear set. Additionally, $q_{S}$ has basically the
same outgoing transitions as the accepting state $f$, but they lead into the
layer for $s_{1}$.

Formally, let
$\mathcal{A}_{S}=((S\times\\{1,\dots,m+1\\})\cup\\{q_{S}\\},\Sigma,q_{S},\Delta_{S},\\{q_{S}\\},C_{S})$,
where

$\displaystyle\Delta_{S}=\ $
$\displaystyle\\{((s_{i},k),a,\mathbf{0}^{d+|Q|-1}\cdot\mathbf{v},(s_{j},k))\mid(s_{i},a,\mathbf{v},s_{j})\in\Delta,k\leq
m+1\\}$ $\displaystyle\cup\ $
$\displaystyle\\{((s_{i},i),a,\mathbf{0}^{d+|Q|-1}\cdot\mathbf{v},(s_{j},i+1)\mid(s_{i},a,\mathbf{v},s_{j})\in\Delta,i\leq
m\\}$ $\displaystyle\cup\ $
$\displaystyle\\{((s_{i},m+1),a,\mathbf{0}^{d+|Q|-1}\cdot\mathbf{v},q_{S})\mid(s_{i},a,\mathbf{v},f)\in\Delta\\}$
$\displaystyle\cup\ $
$\displaystyle\\{(q_{S},a,\mathbf{0}^{d+|Q|-1}\cdot\mathbf{v},(s_{i},1)\mid(f,a,\mathbf{v},s_{i})\in\Delta\\}.$

For two semi-linear sets $C_{1},C_{2}$ of dimension $d$, let
$C_{1}-C_{2}=\\{\mathbf{u}\in\mathbb{N}^{d}\mid\mathbf{u}+\mathbf{v}\in C_{1}$
$\text{for some }\mathbf{v}\in C_{2}\\}$. As shown by Klaedtke and Ruess, the
set $C_{1}-C_{2}$ remains semi-linear (observe that it is definable in
Presburger Arithmetic). For $q\in Q$, let $C_{q}=\sum L(B_{q,q})$ and choose
$C_{S}(q_{S})=\\{\mathbf{0}^{d+|Q|-1}\\}\cdot(\vec{C}-C_{s_{1}}-\dots-
C_{s_{m}})$, where $\vec{C}$ is defined as $C$ but without any base vectors.

Finally, let
$\mathcal{A}^{\prime}=(Q^{\prime},\Sigma,q_{0},\Delta^{\prime},\\{q_{S}\mid
S\subseteq Q\\},C^{\prime})$ be the (disjoint) union of $\hat{}\mathcal{A}$
and all $\mathcal{A}_{S}$ with additional transitions $(q,a,\mathbf{v},q_{S})$
for each $(q,a,\mathbf{v},f)\in\Delta$ and
$C^{\prime}(q_{S})=\hat{C}+C_{S}(q_{S})$. We claim that $\mathcal{A}^{\prime}$
is equivalent to $\mathcal{A}$.

$\Rightarrow$ We first show $P_{\omega}(\mathcal{A})\subseteq
P_{\omega}(\mathcal{A}^{\prime})$. Let $\alpha\in P_{\omega}(\mathcal{A})$
with accepting run $r=r_{1}r_{2}r_{3}\dots$ where
$r_{i}=(p_{i-1},\gamma_{i},\mathbf{v}_{i},p_{i})$. Let $S$ be the set of
states that appear infinitely often in $r$ and let $i$ be minimal such that
there is an accepting hit in $r_{i}$ and we have $p_{j}\in S$ for all $j\geq
i$. Let $u=\alpha_{1}\dots\alpha_{z}\in\Sigma^{*}$ be the prefix of $\alpha$
that has been read upon visiting $p_{i}$, and let
$\beta=\alpha_{z+1}\alpha_{z+2}\dots\in\Sigma^{\omega}$, i. e.,
$\alpha=u\beta$.

First observe that $u\in L(\mathcal{A})$ as $r_{1}\dots r_{i}$ is an accepting
run of $\mathcal{A}$ on $u$ by definition. As a consequence of Lemma 4.4, the
automaton $\hat{}\mathcal{A}$ and $\mathcal{A}$ are equivalent as PA (over
finite words), hence, there is also an accepting run of $\hat{\mathcal{A}}$ on
$u$, say $\hat{r}=\hat{r}_{1}\dots\hat{r}_{z}$. Note that
$\hat{r}_{z}=(p_{z-1},\alpha_{z},\mathbf{v}_{z},f)$, hence
$\mathcal{A}^{\prime}$ has a transition of the form
$\delta=(p_{z-1},\alpha_{z},\mathbf{v}_{z},q_{S})$, hence we can simulate this
partial run of $\mathcal{A}^{\prime}$ with
$\hat{r}_{1}\dots\hat{r}_{z-1}\delta$.

Up to this point we have only used the first $d+|Q|-1$ counters, and will now
only use the last $d$ counters. By definition of $C(q_{S})$ it remains to show
that $\beta\in P_{\omega}(\mathcal{A}_{S})$ (note that we already had an
accepting hit and have thus removed the base vectors from $C(q_{S})$). Observe
that we can safely remove any $\varepsilon$-transition in $r$ without
malforming the run, as all $\varepsilon$-transitions are loops. Let $j_{0}>i$
be minimal such that $r_{j_{0}}\in\Delta$, say
$r_{j_{0}}=(f,\alpha_{z+1},\mathbf{v}_{j_{0}},p_{j_{0}})$. By construction
there is a transition of the form
$(q_{S},\alpha_{z+1},\mathbf{0}^{d+|Q|-1}\cdot\mathbf{v}_{j_{0}},(p_{j_{0}},1))$
in $\mathcal{A}^{\prime}$, which we use to continue our run in
$\mathcal{A}^{\prime}$ (i. e., we forget the $\varepsilon$-loops on $f$).

Now let $j_{m+1}>j_{0}$ be minimal such that there are
$j_{0}<j_{1}<j_{2}<\dots<j_{m}<j_{m+1}$ with $p_{j_{k}}=s_{k}$ for all $1\leq
k\leq m$, and $r_{j_{m+1}}$ is an accepting hit. For all
$j_{k-1}<\ell<j_{k},1\leq k\leq m+1$, we consider the transition $r_{\ell}$.
If $r_{\ell}\in\mathcal{E}$, we simply forget it. Otherwise, we replace
$r_{\ell}$ by
$r^{\prime}_{\ell}=((p_{\ell-1},k),\gamma_{\ell},\mathbf{0}\cdot\mathbf{v}_{\ell},((p_{\ell},k))$.
Furthermore, for $1\leq k\leq m$ we replace $r_{j_{k}}$ by
$r_{j_{k}}^{\prime}=((p_{j_{k}-1},k),\gamma_{j_{k}},$
$\mathbf{0}\cdot\mathbf{v}_{j_{k}},(p_{j_{k}},k+1))$, and finally
$r_{j_{m+1}}$ by
$r^{\prime}_{j_{m+1}}=((p_{j-1},m+1),\mathbf{0}\cdot\mathbf{v}_{j},q_{S})$.

Observe that for the partial run $r^{\prime}=r^{\prime}_{j_{0}}\dots
r^{\prime}_{j_{m+1}}$ we have $\rho(r^{\prime})\in C(q_{S})$, as
$\rho(r_{i+1}\dots r_{j_{m+1}})$ $\in C$, since we have only removed
$\varepsilon$-transitions (on states that we have all seen by construction),
and $C(q_{S})$ is defined accordingly.

We can now iterate the construction and obtain an accepting run of
$\mathcal{A}_{S}$ on $\beta$. This concludes the forward direction.

$\Leftarrow$ We now show $P_{\omega}(\mathcal{A}^{\prime})\subseteq
P_{\omega}(\mathcal{A})$. Let $\alpha\in P_{\omega}(\mathcal{A}^{\prime})$
with accepting run
$r^{\prime}=r^{\prime}_{1}r^{\prime}_{2}r^{\prime}_{3}\dots$ with
$r^{\prime}_{i}=(p^{\prime}_{i-1},\alpha_{i},\mathbf{v}^{\prime}_{i},p^{\prime}_{i})$.
Let $j_{1}<j_{2}<\ldots$ be the positions such that $r^{\prime}_{j_{i}}$ is an
accepting hit for all $i\geq 1$. We proceed by proving a sequence of claims.

Claim 1: $\mathbf{0}\in\vec{C}\subseteq\vec{C}-C_{s_{1}}-\dots-C_{s_{m}}$.
This is immediate from the fact that $\vec{C}$ has no base vectors.

Claim 2: For all $k<j_{1}$ we have $p^{\prime}_{k}\in Q$ (recall that $Q$ is
the subset of the state set of $\mathcal{A}^{\prime}$ that belongs to
$\hat{}\mathcal{A})$. Hence $\rho(r^{\prime}_{1}\dots
r^{\prime}_{j_{1}})\in\hat{C}\cdot\\{\mathbf{0}\\}$. The claim is immediate by
the fact that $\hat{}\mathcal{A}$ as a subautomaton of $\mathcal{A}^{\prime}$
has no accepting states and the transition from $\hat{}\mathcal{A}$ to some
$\mathcal{A}_{S}$ leads to the accepting state $q_{S}$, that is
$r^{\prime}_{j_{1}}=(p^{\prime}_{j_{1}-1},\alpha_{j_{1}},\mathbf{v}^{\prime}_{j_{1}},q_{S})$
with $p^{\prime}_{j_{1}-1}\in Q$.

Claim 3: $\rho(r^{\prime}_{j_{1}+1}\dots
r^{\prime}_{j})\in\\{\mathbf{0}\\}\cdot\mathbb{N}^{d}$ for every $j\geq
j_{1}+1$. Hence $\mathbf{v}^{\prime}_{j}$ can be written as
$\mathbf{0}\cdot\mathbf{v}_{j}$ for some $\mathbf{v}_{j}\in\mathbb{N}^{d}$.
Furthermore, every $p^{\prime}_{j}$ is either $q_{S}$ or of the form
$(s_{k},\ell)$ for some $k\leq m$ and $\ell\leq m+1$. This is immediate by
construction of $\mathcal{A}^{\prime}$, since after the first accepting hit we
have switched to some $\mathcal{A}_{S}$. Define $p_{j}=f$ if
$p^{\prime}_{j}=q_{S}$, and $p_{j}=s_{k}$ if $p^{\prime}_{j}=(s_{k},\ell)$.
Similarly, let $r_{j}=(p_{j-1},\alpha_{j},\mathbf{v}_{j},p_{j})$.

Claim 4: All states of $S$ are visited between every two consecutive
$j_{\ell},j_{\ell+1}$. This follows from the fact that in order to visit
$q_{S}$ in $\mathcal{A}_{S}$ again, we have to run through all layers of
$\mathcal{A}_{S}$.

Claim 5: $\rho(r^{\prime}_{j_{\ell}+1}\dots
r^{\prime}_{j_{\ell+1}})\in\\{\mathbf{0}\\}\cdot(\vec{C}-C_{s_{1}}-\dots-
C_{s_{m}})$, say $\rho(r^{\prime}_{j_{\ell}+1}\dots
r^{\prime}_{j_{\ell+1}})=\mathbf{v}_{j_{\ell}}-\mathbf{v}_{s_{1}}-\dots-\mathbf{v}_{s_{m}}$
with $\mathbf{v}_{s_{i}}\in C_{s_{i}}$. This holds by Claim 3 and the
construction of $\mathcal{A}_{S}$, since $\varepsilon$-loops have been
removed. Let $j_{\ell}<k_{1}<k_{2}<\dots<k_{m}<j_{\ell+1}$ be the positions in
the partial run where we change the layers, i. e.,
$r^{\prime}_{k_{i}}=((s_{i},i),\alpha_{k_{i}},\mathbf{v}^{\prime}_{i},(p_{k_{i}},i+1))$.
These positions exist by Claim 4.

Claim 6: For every $\mathbf{v}_{s_{i}}\in C_{s_{i}}$ there is a sequence of
$\varepsilon$-loops $\bar{\lambda}_{i}$ on $s_{i}$ in $\mathcal{A}$ with
$\rho(\bar{\lambda}_{i})=\mathbf{v}_{s_{i}}$. This is immediate by the choice
of $C_{s_{i}}$.

Claim 7: The run
$\bar{r}_{\ell}=r_{j_{\ell}+1}\dots\bar{\lambda}_{1}r_{k_{1}}\dots\bar{\lambda}_{2}r_{k_{2}}\dots\bar{\lambda}_{m}r_{k_{m}}\dots
r_{j_{\ell+1}}$ of $\mathcal{A}$ is equivalent to
$\bar{r}^{\prime}_{\ell}=r^{\prime}_{j_{\ell}}\dots r^{\prime}_{j_{\ell+1}}$
of $\mathcal{A}^{\prime}$ in the sense that
$\rho(\bar{r}_{\ell})=\rho(\bar{r}^{\prime}_{\ell})-\mathbf{v}_{s_{1}}-\dots-\mathbf{v}_{s_{m}}\in\bar{C}-C_{s_{1}}-\dots-
C_{s_{m}}$, hence $\rho(\bar{r}_{\ell})\in\vec{C}$. This claim follows from
Claim 5 and Claim 6.

We are ready to finish the proof. By Lemma 4.4 there exists an accepting run
$\hat{r}$ of $\alpha_{1}\ldots\alpha_{j_{1}}$ in $\hat{}\mathcal{A}$ (as a PA
on finite words). By construction we have
$\rho(\hat{r})\in\hat{C}\cdot\\{\mathbf{0}\\}$. We construct the run $r$ of
$\mathcal{A}$ as follows. In $r^{\prime}$ we replace $r^{\prime}_{1}\ldots
r^{\prime}_{j_{1}}$ by $\hat{r}$. Now, for $\ell\geq 1$ we replace
$r^{\prime}_{j_{\ell}+1}\ldots r^{\prime}_{j_{\ell+1}}$ by $\bar{r}_{\ell}$ as
constructed in Claim 7. Note that this is a valid run of $\mathcal{A}$.
Furthermore, by Claim 7 we have accepting hits of $\mathcal{A}$ at positions
$(|\hat{r}|-j_{1})+j_{\ell}$ for all $\ell\geq 1$. Hence, $r$ is accepting in
$\mathcal{A}$. $\lrcorner$

We have proved that the MPPBA $\mathcal{A}^{\prime}$ is equivalent to
$\mathcal{A}$. We conclude the proof of the lemma with Lemma 3.2. ∎

By combining the previous lemmas we conclude the main theorems of this section
(see also Figure 2).

######  Theorem 4.2.

The class of $\varepsilon$-PPBA recognizable $\omega$-languages coincides with
the class of PPBA recognizable $\omega$-languages. In other words,
$\varepsilon$-PPBA admit $\varepsilon$-elimination.

######  Theorem 4.3.

Let $L$ be an $\omega$-language. Then the following statements are equivalent.

  1. 1.

$L$ is PPBA-recognizable.

  2. 2.

$L$ is MPPBA-recognizable.

  3. 3.

$L$ is $\varepsilon$-PPBA-recognizable.

  4. 4.

$L$ is $\varepsilon$-MPPBA-recognizable.

PPBA$\varepsilon$-PPBAMPPBA$\varepsilon$-MPPBALemma 3.2Theorem 4.2Lemma 3.2
Figure 2: Equivalences of the prefix models. Dashed lines represent obvious
containment.

###  4.2 $\varepsilon$-elimination for SPBA

Finally, we prove that the reset models admit $\varepsilon$-elimination. In
this section, because we deal with SPBA, where every visit of an accepting
state is resetting, we speak of resetting states instead of accepting states.

######  Lemma 4.6.

For every $\varepsilon$-SPBA $\mathcal{A}$ there is an equivalent SPBA. In
other words, SPBA admit $\varepsilon$-elimination.

###### Proof.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,\mathcal{E},F,C)$ be an
$\varepsilon$-SPBA of dimension $d$. We assume w.l.o.g. that $q_{0}$ has no
ingoing transitions (this can be achieved by introducing a fresh copy of
$q_{0}$). Furthermore, we assume that $F\neq\varnothing$ (otherwise
$S_{\omega}(\mathcal{A})=\varnothing$). Let the states of $Q$ be ordered
arbitrarily, say $Q=\\{q_{0},\dots,q_{n-1}\\}$. We construct an equivalent
SPBA
$\mathcal{A}^{\prime}=(Q^{\prime},\Sigma,q_{0},\Delta^{\prime},F^{\prime},C^{\prime})$
of dimension $d+n$. In the beginning, $\mathcal{A}^{\prime}$ is a copy of
$\mathcal{A}$ (keeping the $\varepsilon$-transitions for now), which is
modified step-by-step. The purpose of the new counters is to keep track of the
states that have been visited (since the last reset). Initially, we hence
modify the transitions as follows: for every transition
$(q_{i},\gamma,\mathbf{v},q_{j})\in\Delta\cup\mathcal{E}$ we replace
$\mathbf{v}$ by $\mathbf{v}\cdot\mathbf{e}_{j}^{n}$.

Let $p,q\in Q$. Assume there is a sequence of transitions
$\tilde{\lambda}=r_{1}\dots r_{j}\dots
r_{k}\in\mathcal{E}^{*}\Delta\mathcal{E}^{*}$; $1\leq j\leq k\leq 2n+1$, where

  * 1.

$r_{j}=(p_{j-1},a,\mathbf{v}_{j},p_{j})\in\Delta$, and

  * 2.

$r_{i}=(p_{i-1},\varepsilon,\mathbf{v}_{i},p_{i})\in\mathcal{E}$ for all
$i\neq j,i\leq k$,

  * 3.

such that $p_{0}=p,p_{k}=q$, and $p_{i}\neq p_{\ell}$ for $i,\ell\leq j$ and
$p_{i}\neq p_{\ell}$ for $i,\ell\geq j$, and

  * 4.

all internal states are non-resetting, i. e., $p_{i}\notin F$ for all $0<i<k$.

Then we introduce the _shortcut_ $(p,a,\rho(\tilde{\lambda}),q)$, where
$\rho(\tilde{\lambda})$ is computed already with respect to the new counters,
tracking that the $p_{i}$ in $\tilde{\lambda}$ have been visited, i. e., the
counters corresponding to the $p_{i}$ in this sequence have non-zero values.

Let $p,q\in Q$. We call a (possibly empty) sequence $\lambda=r_{1}\dots
r_{k}\in\mathcal{E}^{*};k\geq 0$ with
$r_{i}=(p_{i-1},\varepsilon,\mathbf{v}_{i},p_{i})$ and $p_{0}=p,p_{k}=q$ a
_no-reset $\varepsilon$-sequence_ from $p$ to $q$ if all internal states are
non-resetting, i. e., $p_{i}\notin F$ for all $0<i<k$. A _no-reset
$\varepsilon$-path_ is a no-reset sequence such that $p_{i}\neq p_{j}$ for
$i\neq j$. Observe that the set of no-reset $\varepsilon$-paths from $p$ to
$q$ is finite, as the length of each path is bounded by $n-1$. We call the
pair $(p,q)$ a _$C$ -pair_ if there is a no-reset $\varepsilon$-sequence $r$
from $p$ to $q$ with $\rho(r)\in C$, where $\rho(r)$ is computed in
$\mathcal{A}$.

Let $S=(f_{1},\ldots,f_{\ell})$ be a non-empty sequence of pairwise distinct
resetting states (note that this implies $\ell\leq n$). We call $S$ a _$C$
-sequence_ if each $(f_{i},f_{i+1})$ is a $C$-pair.

For all $p,q\in F$ and $C$-sequences $S$ such that $p=f_{1}$ if $p\in F$ and
$q=f_{\ell}$ if $q\in F$, we introduce a new state $(p,S,q)$. We add $(p,S,q)$
to $F^{\prime}$, that is, we make the new states resetting. State $(p,S,q)$
will represent a partial run of the automaton with only
$\varepsilon$-transitions starting in $p$, visiting the resetting states of
$S$ in that order, and ending in $q$.

Observe that in the following we introduce only finitely many transitions by
the observations made above, we will not repeat this statement in each step.
Let $p,q\in Q$ and $S=(f_{1},\dots,f_{\ell})$ be a $C$-sequence. For every
transition of the form $(s,a,\mathbf{v},p)\in\Delta$ we insert new transitions
$\\{(s,a,\mathbf{v}+\rho(\lambda),(p,S,q))\mid\lambda$ is a no-reset
$\varepsilon$-path from $p$ to $f_{1}\\}$ to $\Delta^{\prime}$. Similarly, for
every transition of the form $(q,a,\mathbf{v},t)\in\Delta$ we insert new
transitions $\\{((p,S,q),a,\mathbf{v}+\rho(\lambda),t)\mid\lambda\text{ is a
no-reset $\varepsilon$-path from $f_{\ell}$ to $q$}\\}$ to $\Delta^{\prime}$.
Again this set is finite. Additionally, let $p^{\prime},q^{\prime}\in Q$ and
$S^{\prime}=(f_{1}^{\prime},\dots,f^{\prime}_{k})$ a $C$-sequence. For every
sequence $\tilde{\lambda}=\lambda\delta\lambda^{\prime}$ where $\lambda$ is a
no-reset $\varepsilon$-path from $f_{\ell}$ to $q$,
$\delta=(q,a,\mathbf{v},p^{\prime})$, and $\lambda^{\prime}$ is a no-reset
$\varepsilon$-path from $p^{\prime}$ to $f^{\prime}_{1}$ we add the shortcuts
$\big{(}(p,S,q),a,\rho(\tilde{\lambda}),(p^{\prime},S^{\prime},q^{\prime})\big{)}$
to $\Delta^{\prime}$.

Lastly, we connect the initial state $q_{0}$ in a similar way (recall that we
assume that $q_{0}$ has no ingoing transitions, and in particular no loops).
For every transition $(p,a,\mathbf{v},q)\in\Delta$ and every $C$-sequence
$S=(f_{1},\dots,f_{l})$ with the property that $(q_{0},f_{1})$ is a $C$-pair
and there is a no-reset $\varepsilon$-path $\lambda$ from $f_{\ell}$ to $p$,
we introduce the transition $(q_{0},a,\rho(\lambda)+\mathbf{v},q)$ for every
such path $\lambda$. Additionally, for every $C$-sequence
$S^{\prime}=(f_{1}^{\prime},\dots f^{\prime}_{k})$ such that there is a no-
reset $\varepsilon$-path $\lambda^{\prime}$ from $q$ to $f_{1}^{\prime}$, we
introduce the transition
$\big{(}q_{0},a,\rho(\lambda)+\mathbf{v}+\rho(\lambda^{\prime}),(q,S^{\prime},t)\big{)}$
for all such paths $\lambda,\lambda^{\prime}$ and $t\in Q$. Furthermore, for
every no-reset $\varepsilon$-path $\hat{\lambda}$ from $q_{0}$ to $p$, we
introduce the transition
$(q_{0},a,\rho(\hat{\lambda})+\mathbf{v}+\rho(\lambda^{\prime}),(q,S^{\prime},t))$
for all $t\in Q$. A reader who is worried that we may introduce too many
transitions at this point shall recall that $(q,S^{\prime},t)$ has no outgoing
transition if there does not exist a no-reset $\varepsilon$-path from
$f_{k}^{\prime}$ to $t$. Finally, we delete all $\varepsilon$-transitions.

We define $C^{\prime}$ similar to the construction due to Klaedtke and Ruess
[9]. For every $q\in Q$ we define $C_{q}=\sum\hat{\mathcal{B}}_{q,q}$, where
$\hat{\mathcal{B}}_{q,q}$ is defined as $\mathcal{B}_{q,q}$ but without any
accepting states, that is, $\hat{\mathcal{B}}_{q,q}=(Q\setminus
F,\Gamma,q,\\{(p,\mathbf{v},p^{\prime})\mid(p,\varepsilon,\mathbf{v},p^{\prime})\in\mathcal{E},p,p^{\prime}\notin
F\\},\\{q\\})$ for a suitable alphabet $\Gamma\subseteq\mathbb{N}^{d}$. Then
$C^{\prime}=\\{\mathbf{v}\cdot(x_{0},\dots,x_{n-1})\mid\mathbf{v}+\mathbf{u}\in
C,\mathbf{u}\in\sum_{x_{i}\geq 1}C_{q_{i}}\\}$. By this, we substract the
$C_{q_{i}}$ if the counter for $q_{i}$ is greater or equal to one, that is,
the state has been visited. This finishes the construction.

We now prove that $\mathcal{A}^{\prime}$ is equivalent to $\mathcal{A}$. In
the one direction we compress the run by using the appropriate shortcuts, in
the other direction we unravel it accordingly.

$\Rightarrow$ To show that $S_{\omega}(\mathcal{A})\subseteq
S_{\omega}(\mathcal{A}^{\prime})$, let $\alpha\in S_{\omega}(\mathcal{A})$
with accepting run $r=r_{1}r_{2}r_{3}\dots$. If there are no
$\varepsilon$-transitions in $r$, we are done (as $r$ is also an accepting run
of $\mathcal{A}^{\prime}$ on $\alpha$).

Otherwise, we construct an accepting run $r^{\prime}$ of
$\mathcal{A}^{\prime}$ on $\alpha$ by replacing maximal
$\varepsilon$-sequences in $r$ step-by-step. Let $i$ be minimal such that
$r_{i}\dots r_{j}$ is a maximal $\varepsilon$-sequence. Let
$r_{i}=(p_{i-1},\varepsilon,\mathbf{v}_{i},p_{i}),r_{j}=(p_{j-1},\varepsilon,\mathbf{v}_{j},p_{j})$,
and $r_{j+1}=(p_{j},\alpha_{z},\mathbf{v}_{j+1},p_{j+1})$. It might be the
case that $i=1$, i. e., the run $r$ starts with an $\varepsilon$-transition
leaving $q_{0}$. Otherwise $i>1$ and we can write
$r_{i-1}=(p_{i-2},\alpha_{z-1},\mathbf{v}_{i-1},p_{i-1})$. By allowing the
empty sequence, we may assume that there is always a second (possibly empty)
maximal $\varepsilon$-sequence $r_{j+2}\dots r_{k}$ starting directly after
$r_{j+1}$. We distinguish (the combination of) the following cases.

  * 1.

At least one state in $r_{i}\dots r_{j}$ is resetting, i. e., there is a
position $i-1\leq\ell\leq j$ such that $p_{\ell}\in F$ (F) or not (N).

  * 2.

At least one state in $r_{j+2}\dots r_{k}$ is resetting, i. e., there is a
position $j+1\leq\ell^{\prime}\leq k$ such that $p_{\ell^{\prime}}\in F$ (F)
or not (N). If $r_{j+2}\dots r_{k}$ is empty, we are in the case (N).

Hence, we consider four cases in total.

$\bullet$ Case (NN). That is, there is no resetting state in $r_{i}\dots
r_{k}$. Note that the $\varepsilon$-sequence $r_{i}\dots r_{j}$ can be
decomposed into an $\varepsilon$-path and $\varepsilon$-cycles as follows. If
we have $p_{i_{1}}\neq p_{j_{1}}$ for all $i\leq i_{1}<j_{1}\leq j$ we are
done as $r_{i}\dots r_{j}$ is already an $\varepsilon$-path. Otherwise let
$i_{1}\geq i$ be minimal such that there is $j_{1}>i_{1}$ with
$p_{i_{1}}=p_{j_{1}}$, that is, $r_{i_{1}+1}\dots r_{j_{1}}$ is an
$\varepsilon$-cycle. If $r_{i}\dots r_{i_{1}}r_{j_{1}+1}\dots r_{j}$ is an
$\varepsilon$-path, we are done. Otherwise, let $i_{2}>j_{1}$ be minimal such
that there is $j_{2}>i_{2}$ with $p_{i_{2}}=p_{j_{2}}$, that is,
$r_{i_{2}+1}\dots r_{j_{2}}$ is an $\varepsilon$-cycle. Then again, if
$r_{i}\dots r_{i_{1}}r_{j_{1}+1}\dots r_{i_{2}}r_{j_{2}+1}\dots r_{j}$ is an
$\varepsilon$-path, we are done. Otherwise, we can iterate this argument and
obtain a set of $\varepsilon$-cycles $r_{i_{1}+1}\dots
r_{j_{1}},\dots,r_{i_{m}+1}\dots r_{j_{m}}$ for some $m$, and an
$\varepsilon$-path $\hat{r}_{i,j}=r_{i}\dots r_{i_{1}}r_{j_{1}+1}\dots
r_{i_{m}}r_{j_{m}+1}\dots r_{j}$ which partition $r_{i}\dots r_{j}$. Now
observe that $\rho(r_{i_{1}+1}\dots r_{j_{1}})+\dots+\rho(r_{i_{m}+1}\dots
r_{j_{m}})\in C_{p_{i_{1}}}+\dots+C_{p_{i_{m}}}$. We can do the same
decomposition for the $\varepsilon$-sequence $r_{j+2}\dots r_{k}$ into a set
of $\varepsilon$-cycles and an $\varepsilon$-path $\hat{r}_{j+2,k}$. By the
construction of $\Delta^{\prime}$, there is a shortcut
$\delta=(p_{i-1},\alpha_{z},(\rho(\hat{r}_{i,j})+\mathbf{v}_{j+1}+\rho(\hat{r}_{j+2,k}))\cdot\hat{}\mathbf{e}^{n},p_{k})$,
where $\hat{}\mathbf{e}^{n}$ is the $n$-dimensional vector counting the states
appearing in $\hat{r}_{i,j}$ and $\hat{r}_{j+2,k}$ and the state $p_{j+1}$. By
the construction of $\Delta^{\prime}$ and $C^{\prime}$, we may subtract all
$\varepsilon$-cycles that have been visited in $r_{i}\dots r_{k}$, hence, we
may replace $r_{i}\dots r_{k}$ by $\delta$ to simulate exactly the behavior of
$\mathcal{A}$.

$\bullet$ Case (NF). That is, there is no resetting state in $r_{i}\dots
r_{j}$ but at least one resetting state in $r_{i+2}\dots r_{k}$ (in
particular, this sequence is not empty). Let $\ell_{1},\dots,\ell_{m}$ denote
the positions of resetting states in $r_{i+2}\dots r_{k}$, and let
$\ell_{0}<\ell_{1}$ be maximal such that $\ell_{0}$ is resetting (this is
before $r_{i}$, and if such an $\ell_{0}$ does not exist, let $\ell_{0}=0$),
i. e., $\ell_{0}$ is the position of the last reset before the reset at
position $\ell_{1}$. As $r$ is an accepting run, the sequence
$S=(\ell_{1},\dots,\ell_{m})$ is a $C$-sequence (we may assume that all states
in $S$ are pairwise distinct, otherwise there is a reset-cycle, which can be
ignored). In the same way as in the previous case we can partition the
$\varepsilon$-sequence $r_{i}\dots r_{j}$ into an $\varepsilon$-path
$\hat{r}_{i,j}$ and a set of $\varepsilon$-cycles, which may be subtracted
from $C$. Likewise, we can partition the sequence $r_{j+2}\dots r_{\ell_{1}}$
into an $\varepsilon$-path $\hat{r}_{j+2,\ell_{1}}$ and $\varepsilon$-cycles
with the same property. By the construction of $\Delta^{\prime}$ there is a
shortcut $(p_{i-1},a,\rho(\hat{r}_{i,j})+\mathbf{v}_{j+1},p_{j+1})$ and hence
a transition
$\delta=(p_{i-1},a,\rho(\hat{r}_{i,j})+\mathbf{v}_{j+1}+\rho(\hat{r}_{j+2,\ell_{1}}),(p_{j+1},S,p_{k}))$
(note that this is also the case if $i=1$). Thus, we replace $r_{i}\dots
r_{k}$ by $\delta$. In particular, $\rho(r_{\ell_{0}+1}\dots r_{i-1}\delta)$
can be obtained from $\rho(r_{\ell_{0}+1}\dots r_{\ell_{1}})$ by subtracting
all $\varepsilon$-cycles that have been visited within this partial run.
Furthermore, observe that $\rho(r_{\ell_{1}+1}\dots r_{\ell_{2}})\in
C,\dots,\rho(r_{\ell_{m-1}+1}\dots r_{\ell_{m}})\in C$ depend only on the
automaton, and not the input word. As the counters are reset in
$r_{\ell_{m}}$, we may continue the run from $\delta$ the same way as in
$r_{k}$, using an appropriate transition from $\Delta^{\prime}$ that adds the
vector $\rho(\hat{r}_{\ell_{m}+1,k})$, thus respecting the acceptance
condition.

$\bullet$ Case (FN). Similar to (NF), but this time we replace
$r_{i-1}r_{i}\dots r_{j}$ by an appropriate transition into a state of the
form $(p_{i-2},\alpha_{z},\mathbf{v},(p_{i-1},S,p_{j}))$ for a suitable
$C$-sequence $S$ and vector $\mathbf{v}$, followed by a shortcut leading to
$p_{k}$. If $i=0$ (we enter a $C$-sequence before reading the first symbol),
we make use of the transitions introduced especially for $q_{0}$.

$\bullet$ Case (FF). Similar to (FN) and (NF), but we transition from a state
of the form $(p_{i-1},S,p_{j})$ into a state of the form
$(p_{j+1},S^{\prime},p_{k})$ for suitable $C$-sequences $S,S^{\prime}$, again
respecting the case $i=0$. $\lrcorner$

$\Leftarrow$ To show that $S_{\omega}(\mathcal{A}^{\prime})\subseteq
S_{\omega}(\mathcal{A})$ we unravel the shortcuts and $(p,S,q)$-states
introduced in the construction. Let $\alpha\in
S_{\omega}(\mathcal{A}^{\prime})$ with accepting run
$r^{\prime}=r^{\prime}_{1}r^{\prime}_{2}r^{\prime}_{3}\dots$. We replace every
transition $r^{\prime}_{i}\in\Delta^{\prime}\setminus\Delta$ (i. e.,
transitions that do not appear in $\mathcal{A}$) by an appropriate sequence of
transitions in $\mathcal{A}$. Let $i\geq 1$ be minimal such that
$r^{\prime}_{i}$ is a transition in $\Delta^{\prime}\setminus\Delta$.

We distinguish the form of $r^{\prime}_{i}$ and show that the possible forms
correspond one-to-one to the cases in the forward direction.

SPBA$\varepsilon$-SPBAMSPBA$\varepsilon$-MSPBA$\varepsilon$-WPBAWPBAMWPBA$\varepsilon$-MWPBALemma
3.3Lemma 4.6Lemma 3.3Lemma 3.4Lemma 3.5Lemma 3.4Lemma 3.5Lemma 3.3Lemma 3.3
Figure 3: Equivalences of the reset models. Dashed lines represent obvious
containment.

  * 1.

Case (NN). The case that $r^{\prime}_{i}=(p,a,\rho(\tilde{\lambda}),q)$ is a
shortcut, i. e., $\tilde{\lambda}\in\mathcal{E}^{*}\Delta\mathcal{E}^{*}$,
corresponds to the case (NN). In particular, there are no accepting states in
$r$. Let $k<i$ be the position of the last reset before $r^{\prime}_{i}$, and
$k^{\prime}$ the position of the first reset after $r^{\prime}_{i}$, where
$k^{\prime}=i$ if $r^{\prime}_{i}$ transitions into a resetting state. By the
acceptance condition we have $\rho(r^{\prime}_{k+1}\dots
r^{\prime}_{k^{\prime}})\in C-(\sum_{q\in Q^{\prime}}C_{q})$ for some set
$Q^{\prime}\subseteq Q$ based on the counter values. Hence, we can replace
$r^{\prime}_{i}$ by the partial run $\tilde{\lambda}$ filled with possible
$\varepsilon$-cycles on some states in $Q^{\prime}$.

  * 2.

Case (NF). The case that
$r^{\prime}_{i}=(s,a,\mathbf{v}+\rho(\lambda),(p,S,q))$ such that
$S=(f_{1},\dots f_{\ell})$ is a $C$-sequence, there is a transition
$\delta=(s,a,\mathbf{v},p)\in\Delta$ and $\lambda$ is a no-reset
$\varepsilon$-path from $p$ to $f_{1}$, corresponds to the case (NF). By the
definition of $C$-sequence there is a sequence $r_{f_{1},f_{\ell}}$ of
$\varepsilon$-transitions in $\mathcal{A}$ starting in $f_{1}$, ending in
$f_{\ell}$, visiting the resetting states $f_{1}$ to $f_{\ell}$ (in that
order) such that the reset-acceptance condition is satisfied on every visit of
one the accepting states. Then we can replace $r^{\prime}_{i}$ by
$\delta\lambda r_{f_{1},f_{\ell}}$, possibly again filled with some
$\varepsilon$-cycles based on the state counters of $\lambda$, similar to the
previous case. Note that at this point we do not yet unravel the path from
$f_{\ell}$ to $q$, as it depends on how the run $r^{\prime}$ continues (as
handled by the next two cases).

  * 3.

Case (FN). The case that
$r^{\prime}_{i}=((p,S,q),a,\mathbf{v}+\rho(\lambda),t)$ such that
$S=(f_{1},\dots f_{\ell})$ is a $C$-sequence, there is a transition
$\delta=(q,a,\mathbf{v},t)\in\Delta$ and $\lambda$ is a no-reset
$\varepsilon$-path from $f_{\ell}$ to $q$, corresponds to the case (FN).
Similar to the previous case, we can replace $r^{\prime}_{i}$ by
$\lambda\delta$, possibly again amended with some $\varepsilon$-cycles based
on the state counters of $\lambda$. If $i=1$, the transition might also be of
the form $r^{\prime}_{1}=(q_{0},\alpha_{1},\rho(\lambda)+\mathbf{v},t)$ such
that $S$ is a $C$-sequence with the property that $(q_{0},f_{1})$ is a
$C$-pair. Then there is a sequence of $\varepsilon$-transitions
$r_{q_{0},f_{\ell}}$ in $\mathcal{A}$ as above. Then we replace
$r^{\prime}_{1}$ by $r_{q_{0},f_{\ell}}\lambda\delta$ (with possible
$\varepsilon$-cycles) instead.

  * 4.

Case (FF). The case that
$r^{\prime}_{i}=((p,S,q),a,\rho(\tilde{\lambda}),(p^{\prime},S^{\prime},q^{\prime})$
such that $S=(f_{1},\dots f_{\ell})$ and
$S^{\prime}=(f^{\prime}_{1},\dots,f^{\prime}_{k})$ are $C$-sequences, there is
a transition $\delta=(q,a,\mathbf{v},p^{\prime})\in\Delta$ and
$\tilde{\lambda}=\lambda\delta\lambda^{\prime}$, where $\lambda$ is a no-reset
$\varepsilon$-path from $f_{\ell}$ to $q$ and $\lambda^{\prime}$ is a no-reset
$\varepsilon$-path from $p^{\prime}$ to $f_{1}^{\prime}$, corresponds to the
case (FF). This case is basically the union of the previous cases. There is a
sequence $r_{f^{\prime}_{1},f^{\prime}_{k}}$ of $\varepsilon$-transitions in
$\mathcal{A}$, as in the case (RF). Hence, we replace $r^{\prime}_{i}$ by
$\tilde{\lambda}r_{f^{\prime}_{1},f^{\prime}_{k}}$ (with possible
$\varepsilon$-cycles). If $i=1$, the transition might also be of the form
$r^{\prime}_{1}=(q_{0},\alpha_{1},\rho(\lambda)+\mathbf{v}+\rho(\lambda^{\prime}),(p^{\prime},S^{\prime},q^{\prime}))$
such that $(q_{0},f_{1})$ is a $C$-pair. Then there is a sequence of
$\varepsilon$-transitions $r_{q_{0},f_{\ell}}$ in $\mathcal{A}$ as above, and
we replace $r^{\prime}_{1}$ by
$r_{q_{0},f_{\ell}}\tilde{\lambda}r_{f^{\prime}_{1},f^{\prime}_{k}}$ (with
possible $\varepsilon$-cycles). $\lrcorner$

This finishes the proof of the lemma. ∎

Concluding this section, we have proved the equivalence of all reset models,
as stated in the following theorem. See Figure 3 for an illustration.

######  Theorem 4.4.

Let $L$ be an $\omega$-language. Then the following statements are equivalent.

  1. 1.

$L$ is SPBA-recognizable.

  2. 2.

$L$ is MSPBA-recognizable.

  3. 3.

$L$ is $\varepsilon$-SPBA-recognizable.

  4. 4.

$L$ is $\varepsilon$-MSPBA-recognizable.

  5. 5.

$L$ is WPBA-recognizable.

  6. 6.

$L$ is MWPBA-recognizable.

  7. 7.

$L$ is $\varepsilon$-WPBA-recognizable.

  8. 8.

$L$ is $\varepsilon$-MWPBA-recognizable.

Recall that $\mathcal{L}_{\mathsf{Reset}}$ denotes the class of all SPBA-
recognizable $\omega$-languages, which by the above theorem can equivalently
be defined using any reset model.

##  5 Equivalence of PPBA and blind counter machines and their closure
properties

In this section we prove that PPBA describe the same class of
$\omega$-languages as (synchronous) blind counter machines introduced by
Fernau and Stiebe [5]. A _blind $k$-counter machine_ (CM) is quintuple
$\mathcal{M}=(Q,\Sigma,q_{0},\Delta,F)$ where $Q$, $\Sigma$, $q_{0}$ and $F$
are defined as for NFA, and $\Delta\subseteq
Q\times(\Sigma\cup\\{\varepsilon\\})\times\mathbb{Z}^{d}\times Q$ is the set
of _integer labeled transitions_. In particular, the transitions of $\Delta$
are labeled with possibly negative integer vectors. Furthermore,
$\varepsilon$-transitions are allowed.

A _configuration_ for an infinite word
$\alpha=\alpha_{1}\alpha_{2}\alpha_{3}\dots$ of $\mathcal{M}$ is a tuple of
the form
$c=(p,\alpha_{1}\dots\alpha_{i},\alpha_{i+1}\alpha_{i+2}\dots,\mathbf{v})\in
Q\times\Sigma^{*}\times\Sigma^{\omega}\times\mathbb{Z}^{k}$ for some $i\geq
0$. A configuration $c$ _derives_ into a configuration $c^{\prime}$, written
$c\vdash c^{\prime}$, if either
$c^{\prime}=(q,\alpha_{1}\dots\alpha_{i+1},\alpha_{i+2}\dots,\mathbf{v}+\mathbf{u})$
and $(p,\alpha_{i+1},\mathbf{u},q)\in\Delta$, or
$c^{\prime}=(q,\alpha_{1}\dots\alpha_{i},\alpha_{i+1}\alpha_{i+2}\dots,\mathbf{v}+\mathbf{u})$
and $(p,\varepsilon,\mathbf{u},q)\in\Delta$. $\mathcal{M}$  _accepts_ an
infinite word $\alpha$ if there is an infinite sequence of configuration
derivations $c_{1}\vdash c_{2}\vdash c_{3}\vdash\dots$ with
$c_{1}=(q_{0},\varepsilon,\alpha,\mathbf{0})$ such that for infinitely many
$i$ we have
$c_{i}=(p_{i},\alpha_{1}\dots\alpha_{j},\alpha_{j+1}\alpha_{j+2}\dots,\mathbf{0})$
with $p_{i}\in F$ and for all $j\geq 1$ there is a configuration of the form
$(p,\alpha_{1}\dots\alpha_{j},\alpha_{j+1}\alpha_{j+1}\dots,q)$ for some
$p,q\in Q$ in the sequence. That is, a word is accepted if we infinitely often
visit an accepting state when the counters are $\mathbf{0}$, and every symbol
of $\alpha$ is read at some point. We define the $\omega$-language recognized
by $\mathcal{M}$ as
$L_{\omega}(\mathcal{M})=\\{\alpha\in\Sigma^{\omega}\mid\mathcal{M}\text{
accepts }\alpha\\}$.

We show that we can effectively convert every CM into an equivalent
$\varepsilon$-PPBA, which is equivalent to a PPBA by Theorem 4.2. For the
other direction we will make use of $\varepsilon$-transitions, i. e., our
results do not yield an $\varepsilon$-elimination scheme for CM. To the best
of our knowledge, it is unknown if CM without $\varepsilon$-transitions are as
powerful as CM with $\varepsilon$-transitions.

######  Lemma 5.1.

For every CM $\mathcal{M}$ there is an equivalent $\varepsilon$-PPBA
$\mathcal{A}$.

###### Proof.

Let $\mathcal{M}=(Q,\Sigma,q_{0},\Delta,F)$ be a $k$-counter machine. For a
vector $(x_{1},\dots,x_{k})\in\mathbb{Z}^{k}$ we define the vector
$\mathbf{v}^{\pm}=(x_{1}^{+},\dots x_{k}^{+},x_{1}^{-},\dots
x_{k}^{-})\in\mathbb{N}^{2k}$ as follows: if $x_{i}$ is positive, then
$x_{i}^{+}=x_{i}$ and $x_{i}^{-}=0$. Otherwise, $x_{i}^{+}=0$ and
$x_{i}^{-}=|x_{i}|$. We construct an equivalent $\varepsilon$-PPBA
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta^{\prime},\mathcal{E}^{\prime},F,C)$ of
dimension $2k$, where
$\Delta^{\prime}=\\{(p,a,\mathbf{v}^{\pm},q)\mid(p,a,\mathbf{v},q)\in\Delta\\}$
and
$\mathcal{E}^{\prime}=\\{(p,\varepsilon,\mathbf{v}^{\pm},q)\mid(p,\varepsilon,\mathbf{v},q)\in\Delta\\}$.
Finally, we choose $C=\\{(x_{1},\dots,x_{k},x_{1},\dots,x_{k})\mid
x_{i}\in\mathbb{N}\\}$. It is now easily verified that
$L_{\omega}(\mathcal{M})=P_{\omega}(\mathcal{A})$. ∎

Next, we show that we can convert every PPBA with $d$ counters into an
equivalent $d$-counter machine by introducing one new state.

######  Lemma 5.2.

For every PPBA $\mathcal{A}$ there is an equivalent CM $\mathcal{M}$.

###### Proof.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ be a PPBA of dimension $d$. We
can assume that $C$ is linear by Lemma 3.1 and since CM are closed under union
[5]. We construct a $d$-counter machine $\mathcal{M}$ that simulates
$\mathcal{A}$ as follows: $\mathcal{M}$ consists of a copy of $\mathcal{A}$
where the accepting states have additional $\varepsilon$-transitions labeled
with the negated period vectors of $C$ We only need to consider the base
vector of $C$ a single time, hence we introduce a fresh initial state
$q_{0}^{\prime}$ and a $\varepsilon$-transition from $q^{\prime}_{0}$ to
$q_{0}$ labeled with the negated base vector of $C$. Observe that a vector
$\mathbf{v}$ lies in $C=\\{b_{0}+b_{1}z_{1}+\dots+b_{\ell}z_{\ell}\mid
z_{1},\dots,z_{\ell}\\}$ if and only if $\mathbf{v}-b_{1}z_{1}-\dots-
b_{\ell}z_{\ell}-b_{0}=\mathbf{0}$ for some $z_{i}$. Intuitively,
$\mathcal{M}$ computes the vector $\mathbf{v}$ in the copies of $Q$ and
guesses the $z_{i}$ in the accepting states. We construct
$\mathcal{M}=(Q\cup\\{q_{0}^{\prime}\\},\Sigma,q_{0}^{\prime},\Delta^{\prime},F)$
where

$\Delta^{\prime}=\Delta\cup\\{(q_{0}^{\prime},\varepsilon,-b_{0},q_{0}\\}\cup\\{(q_{f},\varepsilon,-b_{i},q_{f})\mid
q_{f}\in F,i\leq\ell\\}.$

It is now easily verified that
$P_{\omega}(\mathcal{A})=L_{\omega}(\mathcal{M})$. ∎

From the previous two lemmas follows the equivalence of PPBA and CM.

######  Corollary 5.1.

The classes of PPBA-recognizable $\omega$-languages and CM-recognizable
$\omega$-languages coincide.

As shown by Fernau and Stiebe, the class of CM-recognizable $\omega$-languages
are closed under union, and closed under intersection with $\omega$-regular
languages, but not closed under intersection and complement. Hence, the class
of PPBA-recognizable $\omega$-languages has the same closure properties. At
this point we briefly mention that the class of SPBA-recognizable
$\omega$-languages is also closed under union and intersection with
$\omega$-regular languages, and not closed under intersection and complement
(which can be shown using very similar arguments).

######  Observation 5.1.

The classes of PPBA-recognizable $\omega$-languages and SPBA-recognizable
$\omega$-languages are closed under union, and closed under intersection with
$\omega$-regular languages, but not under intersection and complement.

We conclude this section by showing that the classes of PPBA-recognizable and
SPBA-recognizable $\omega$-languages are also closed under left-concatenation
with Parikh-recognizable languages. We prove the following auxiliary lemma,
which simplifies the proof of this statement, as well as some proofs in the
following sections.

######  Lemma 5.3.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ be a PA (on finite words) with
$L(\mathcal{A})=L$. Then we can construct in polynomial time a PA
$\mathcal{A}_{N}$ with the following properties.

  * 1.

$L(\mathcal{A}_{N})=L\setminus\\{\varepsilon\\}$.

  * 2.

$\mathcal{A}_{N}$ has a single accepting state $f$, and $f$ has no outgoing
transitions.

We say that $\mathcal{A}_{N}$ is _normalized_.

###### Proof.

Let $\mathcal{A}_{N}=(Q\cup\\{f\\},\Sigma,q_{0},\Delta_{N},\\{f\\},C)$, where
$\Delta_{N}=\Delta\cup\\{(p,a,\mathbf{v},f)\mid(p,a,\mathbf{v},q)\in\Delta$,
$q\in F\\}$, that is, $\mathcal{A}_{N}$ guesses the position of the last
symbol of the input word and moves to the new accepting state (which has no
outgoing transitions) if the last symbol is read. As we need to read at least
one symbol to reach $f$, we can never accept the empty word. It is obvious
that $\mathcal{A}_{N}$ as constructed above satisfies the conditions of being
normalized and can be computed in polynomial time. ∎

######  Lemma 5.4.

Let $L_{1}\subseteq\Sigma^{*}$ be Parikh-recognizable and
$L_{2}\subseteq\Sigma^{\omega}$ be SPBA-recognizable (PPBA-recognizable). Then
$L_{1}L_{2}$ is SPBA-recognizable (PPBA-recognizable).

###### Proof.

We start with the argument for SPBA. Let
$\mathcal{A}_{1}=(Q_{1},\Sigma,q_{1},\Delta_{1},F_{1},C_{1})$ be a PA of
dimension $d_{1}$ with $L(\mathcal{A}_{1})=L_{1}$ and
$\mathcal{A}_{2}=(Q_{2},\Sigma,q_{2},\Delta_{2},F_{2},C_{2})$ be an SPBA of
dimension $d_{2}$ with $S_{\omega}(\mathcal{A}_{2})=L_{2}$. W.l.o.g. we assume
that $\varepsilon\notin L$ and hence assume that $\mathcal{A}_{1}$ is
normalized, in particular that $F_{1}=\\{f\\}$ (if $\varepsilon\in L$, we use
$L_{1}L_{2}=(L_{1}\setminus\\{\varepsilon\\})L_{2}\cup L_{2}$ and the closure
under union).

We choose the SPBA $\mathcal{A}=(Q_{1}\cup Q_{2},\Sigma,q_{1},\Delta,F_{1}\cup
F_{2},C)$, with

$\displaystyle\Delta=$ $\displaystyle\
\\{(p,a,\mathbf{v}\cdot\mathbf{0}^{d_{2}},q)\mid(p,a,\mathbf{v},q)\in\Delta_{1}\\}$
$\displaystyle\cup$ $\displaystyle\
\\{(p,a,\mathbf{0}^{d_{1}}\cdot\mathbf{v},q)\mid(p,a,\mathbf{v},q)\in\Delta_{2}\\}$
$\displaystyle\cup$ $\displaystyle\
\\{(f,a,\mathbf{0}^{d_{1}}\cdot\mathbf{v},q)\mid(q_{2},a,\mathbf{v},q)\in\Delta_{2}\\}$

and $C=C_{1}\cdot\\{\mathbf{0}^{d_{2}}\\}\cup\\{\mathbf{0}^{d_{1}}\\}\cdot
C_{2}$. It is straightforward to prove that
$S_{\omega}(\mathcal{A})=L(\mathcal{A}_{1})\cdot S_{\omega}(\mathcal{A}_{2})$,
we just give a proof sketch. The SPBA $\mathcal{A}$ is constructed in such a
way that it starts in a copy of $\mathcal{A}_{1}$ and can transition from $f$
to the initial state of the copy of $\mathcal{A}_{2}$. Since $\mathcal{A}_{1}$
is normalized it has only a single accepting state $f$ with no outgoing
transition into $\mathcal{A}_{1}$. In particular, in order to accept an
infinite word, the automaton $\mathcal{A}$ must transition from the copy of
$\mathcal{A}_{1}$ to the copy of $\mathcal{A}_{2}$. Since $f$ is the only
accepting state of $\mathcal{A}_{1}$ and the only state with transitions to
the states of the copy of $\mathcal{A}_{2}$, we must have read a word from
$L(\mathcal{A}_{1})$ upon reaching $f$ by the choice of $C$. After the reset
in $f$, it now accepts only if the rest of the infinite word belongs to
$S_{\omega}(\mathcal{A}_{2})$ (note that the first $d_{1}$ counters are reset
in $f$, and only the last $d_{2}$ counters are used after the reset).

The proof for PPBA is similar. Instead of an SPBA, we start with a PPBA
$\mathcal{A}_{2}$ for $L_{2}$ and construct a PPBA $\mathcal{A}$ for
$L_{1}L_{2}$. The only difference in the construction is to set $C=C_{1}\cdot
C_{2}$, as the counters are not reset when the automaton visits $f$. ∎

##  6 Expressiveness of PPBA and SPBA

In this section, we show that the class of PPBA-recognizable
$\omega$-languages is a strict subset of the class of SPBA-recognizable
$\omega$-languages. It will be convenient to consider the class
$\mathcal{L}_{\mathsf{PA}}^{\omega}=\\{U_{1}V_{1}^{\omega}\cup\dots\cup
U_{n}V_{n}^{\omega}\mid n\geq 1,U_{i},V_{i}\in\mathcal{L}_{\mathsf{PA}}\\}$,
which is inspired by Büchi’s theorem. Observe that this class is equivalent to
the class $\mathcal{K}_{*}$ mentioned by Fernau and Stiebe who have shown that
the class of CM-recognizable $\omega$-languages is a strict subset of
$\mathcal{K}_{*}$ [5, Lemmas 3.2 and 3.3]. By Corollary 5.1 we obtain that the
class of PPBA-recognizable $\omega$-languages is a strict subset of
$\mathcal{L}_{\mathsf{PA}}^{\omega}$.

We show that $\mathcal{L}_{\mathsf{PA}}^{\omega}$ is a strict subset of the
class of SPBA-recognizable languages. We begin by showing that the
$\omega$-closure of Parikh-recognizable languages is SPBA-recognizable.

######  Lemma 6.1.

Let $L\subseteq\Sigma^{*}$ be Parikh-recognizable. Then $L^{\omega}$ is SPBA-
recognizable.

###### Proof.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ be a PA with $L(\mathcal{A})=L$.
We show that we can construct an SPBA $\mathcal{A}^{\prime}$ that simulates
accepting runs of $\mathcal{A}$ infinitely often, implying
$L_{\omega}(\mathcal{A}^{\prime})=L^{\omega}$. As we have
$L^{\omega}=(L\setminus\\{\varepsilon\\})^{\omega}$ for all languages $L$ by
definition, we assume that $\mathcal{A}$ is normalized by Lemma 5.3.

We choose $\mathcal{A}^{\prime}=(Q,\Sigma,q_{0},\Delta^{\prime},F,C)$ where
$\Delta^{\prime}=\Delta\cup\\{(f,a,\mathbf{v},q)\mid(q_{0},a,\mathbf{v},q)\in\Delta\\}$.
We show that $S_{\omega}(\mathcal{A}^{\prime})=L(\mathcal{A})^{\omega}$.

$\Rightarrow$ We first show that $S_{\omega}(\mathcal{A}^{\prime})\subseteq
L(\mathcal{A})^{\omega}$. Let $\alpha\in S_{\omega}(\mathcal{A}^{\prime})$
with accepting run $r=r_{1}r_{2}r_{3}\dots$, where
$r_{i}=(p_{i-1},\alpha_{i},\mathbf{v}_{i},p_{i})$. Let
$0=k_{0}<k_{1}<k_{2}<\ldots$ denote the reset positions in $r$. We show that
we can modify the partial run $r_{j-1,j}=r_{k_{j-1}+1}r_{k_{j-1}+2}\dots
r_{k_{j}}$ on $w_{j}=\alpha[k_{j-1}+1,k_{j}]$ for all $j\geq 1$ such that it
becomes an accepting run of $\mathcal{A}$ on $w_{j}$. Note that $r_{0,1}$ is
already an accepting run of $\mathcal{A}$ on $w_{1}$. Observe that for $j>1$
the transition $r_{k_{j-1}+1}$ is a new transition of the form
$(f,\alpha_{k_{j-1}+1},\mathbf{v}_{k_{j-1}+1},p_{k_{j-1}+1})$, as $f$ has no
outgoing transitions in $\mathcal{A}$. In particular, there is a transition of
the form
$\delta=(q_{0},\alpha_{k_{j-1}+1},\mathbf{v}_{k_{j-1}+1},p_{k_{j-1}+1})\in\Delta$.
Hence, $\delta r_{k_{j-1}+2}\dots r_{k_{j}}$ is an accepting run of
$\mathcal{A}$ on $w_{j}$ for all $j>1$. Hence we have $\alpha\in
L(\mathcal{A})^{\omega}$. $\lrcorner$

$\Leftarrow$ To show that $L(\mathcal{A})^{\omega}\subseteq
S_{\omega}(\mathcal{A}^{\prime})$, let $w_{1}w_{2}w_{3}\dots\in
L(\mathcal{A})^{\omega}$, where $w_{j}\in L(\mathcal{A})$ for all $j\geq 1$.
Let $n_{j}=|w_{1}|+\dots+|w_{j}|$ denote the length of $w_{1}\cdots w_{j}$,
and let $r_{j-1,j}=r_{n_{j-1}+1}r_{n_{j-1}+2}\dots r_{n_{j}}$, where
$r_{i}=(p_{i-1},\alpha_{i},\mathbf{v}_{i},p_{i})$ be an accepting run of
$\mathcal{A}$ on $w_{j}$. Note that $p_{n_{j}}$ is the only accepting state in
$r_{j-1,j}$. Furthermore, there is a transition
$\delta_{j}=(p_{n_{j}},\alpha_{n_{j}+1},\mathbf{v}_{n_{j}+1},p_{n_{j}+1})\in\Delta^{\prime}$.
Let $r^{\prime}_{j-1,j}=\delta_{j-1}r_{n_{j-1}+2}\dots r_{n_{j}}$ for all
$j\geq 2$. Then $r=r_{0,1}r_{1,2}^{\prime}r_{2,3}^{\prime}\dots$ is a run of
$\mathcal{A}^{\prime}$ on $w_{1}w_{2}w_{3}\dots$ and we have a reset on each
$r_{n_{j}}$. As $\rho(w_{j})\in C$ for all $j\geq 1$, the run $r$ is
accepting, and hence, $w_{1}w_{2}w_{3}\dots\in
S_{\omega}(\mathcal{A}^{\prime})$. ∎

######  Remark 6.1.

As the $\omega$-language $\\{a^{n}b^{n}\mid n\geq 1\\}^{\omega}$ is not PPBA-
recognizable (consequence of Corollary 5.1 and [5, Lemma 3.3]), this lemma is
not true for PPBA-recognizable languages.

At this point we have all ingredients to show that the class
$\mathcal{L}_{\mathsf{PA}}^{\omega}$ is a subset of the class of SPBA-
recognizable $\omega$-languages. We show that this inclusion is strict.

######  Theorem 6.1.

$\mathcal{L}_{\mathsf{PA}}^{\omega}\subsetneq\mathcal{L}_{\mathsf{Reset}}$.

###### Proof.

The inclusion follows directly from 5.1, Lemma 5.4 and Lemma 6.1.

We show that the inclusion is strict. Let $L=\\{a^{n}b^{n}\mid n\geq
1\\}^{*}\cdot\\{a\\}^{\omega}\cup\\{a^{n}b^{n}\mid n\geq 1\\}^{\omega}$. We
show $L\in\mathcal{L}_{\mathsf{Reset}}$ but
$L\notin\mathcal{L}_{\mathsf{PA}}^{\omega}$. That
$L\in\mathcal{L}_{\mathsf{Reset}}$ is witnessed by the SPBA in Figure 4 with
$C=\\{(z,z)\mid z\in\mathbb{N}\\}$.

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$a,\begin{pmatrix}1\\\
0\end{pmatrix}$$b,\begin{pmatrix}0\\\ 1\end{pmatrix}$$b,\begin{pmatrix}0\\\
1\end{pmatrix}$$b,\begin{pmatrix}0\\\ 1\end{pmatrix}$$b,\begin{pmatrix}0\\\
1\end{pmatrix}$$a,\begin{pmatrix}1\\\ 0\end{pmatrix}$$a,\begin{pmatrix}0\\\
0\end{pmatrix}$$a,\begin{pmatrix}0\\\ 0\end{pmatrix}$ Figure 4: The SPBA for
$L=\\{a^{n}b^{n}\mid n\geq 1\\}^{*}\cdot\\{a\\}^{\omega}\cup\\{a^{n}b^{n}\mid
n\geq 1\\}^{\omega}$ with $C=\\{(z,z)\mid z\in\mathbb{N}\\}$.

We focus on $L\notin\mathcal{L}_{\mathsf{PA}}^{\omega}$ and argue by
contradiction. Suppose, $L\in\mathcal{L}_{\mathsf{PA}}^{\omega}$, i. e., there
are Parikh-recognizable languages $U_{1},V_{1},\dots,U_{n},V_{n}$ such that
$L=U_{1}V_{1}^{\omega}\cup\dots\cup U_{n}V_{n}^{\omega}$. Then there is some
$i\leq n$ such that for infinitely many $j\geq 1$ the infinite word
$\alpha_{j}=aba^{2}b^{2}\dots a^{j}b^{j}\cdot a^{\omega}\in
U_{i}V_{i}^{\omega}$. Then $V_{i}$ must contain a word of the form $v=a^{k}$,
$k>0$. Additionally, there cannot be a word in $V_{i}$ with infix $b$. To see
this assume for sake of contradiction that there is a word $w\in V_{i}$ with
$\ell=|w|_{b}>0$. Let $\beta=(v^{\ell+1}w)^{\omega}$. Observe that $\beta$ has
an infix that consists of at least $\ell+1$ many $a$, followed by at most
$\ell$, but at least one $b$, hence, no word of the form $u\beta$ with $u\in
U_{i}$ is in $L$. This is a contradiction, thus $V_{i}\subseteq\\{a\\}^{+}$.

Since $U_{i}\in\mathcal{L}_{\mathsf{PA}}$, there is a PA $\mathcal{A}_{i}$
with $L(\mathcal{A}_{i})=U_{i}$. Let $m$ be the number of states in
$\mathcal{A}_{i}$ and $w^{\prime}=aba^{2}b^{2}\dots a^{m^{4}+1}b^{m^{4}+1}$.
Then $w^{\prime}$ is a prefix of a word accepted by $\mathcal{A}_{i}$. Now
consider the infixes $a^{\ell}b^{\ell}$ and the pairs of states $q_{1},q_{2}$,
where we start reading $a^{\ell}$ and end reading $a^{\ell}$, and
$q_{3},q_{4}$ where we start to read $b^{\ell}$ and end to read $b^{\ell}$,
respectively. There are $m^{2}$ choices for the first pair and $m^{2}$ choices
for the second pair, hence $m^{4}$ possibilities in total. Hence, as we have
more than $m^{4}$ such infixes, there must be two with the same associated
states $q_{1},q_{2},q_{3},q_{4}$. Then we can swap these two infixes and get a
word of the form $ab\dots a^{r}b^{s}\dots a^{s}b^{r}\dots
a^{m^{4}+1}b^{m^{4}+1}$ that is prefix of some word in
$L(\mathcal{A}_{i})=U_{i}$. But no word in $L$ has such a prefix, a
contradiction. Thus, $U_{1}V_{1}^{\omega}\cup\dots\cup U_{n}V_{n}^{\omega}\neq
L$. ∎

##  7 Decision problems

In this section, we show that the (un)decidability results of the common
decision problems for PA on finite words in [9, 6] can be transferred to PBA.
These problems include the following:

  1. 1.

_Emptiness._ Does $\mathcal{A}$ recognize the empty language?

  2. 2.

_Universality._ Does $\mathcal{A}$ accept every word?

  3. 3.

_Equivalence._ Do $\mathcal{A}_{1}$ and $\mathcal{A}_{2}$ recognize the same
language?

  4. 4.

_Inclusion._ Does $\mathcal{A}_{2}$ recognize every word that
$\mathcal{A}_{1}$ recognizes?

In the following we assume that all semi-linear sets are given as a collection
of lists of base vector $b_{0}$ and period vectors $b_{1},\ldots,b_{k}$ (one
list for each linear set in the finite union). All numbers are encoded in
binary.

######  Theorem 7.1.

Emptiness for SPBA, WPBA, and PPBA (and their equivalent models) are
$\coNP$-complete. Universality, inclusion and equivalence for SPBA, WPBA, and
PPBA (and their equivalent models) are undecidable.

Since every SPBA can be converted efficiently into an equivalent WPBA and vice
versa by Lemma 3.4 and Lemma 3.5, the decidability results for SPBA hold for
WPBA, too. Furthermore, we show how to convert any PPBA into an equivalent
WPBA (and hence SPBA) in polynomial time (note that this does not directly
follow from our results, as the intermediate step of converting a PPBA into an
equivalent CM introduces $\varepsilon$-transitions whose elimination requires
super-polynomial time).

Thus, for the $\coNP$-completeness of emptiness it is sufficent to show that
emptiness for $\varepsilon$-MSPBA is in $\coNP$ (yielding the
$\coNP$-membership for all of our models), and $\coNP$-hardness for (even
1-dimensional) PPBA (yielding hardness for all our models). Similarly, it is
sufficient to show the undecidability results for PPBA.

######  Lemma 7.1.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ be a PPBA of dimension $d$. Then
there is an equivalent WPBA that can be constructed in polynomial time.

###### Proof.

The idea is as follows. We have a copy of $\mathcal{A}$ and additionally, for
each linear set $C_{i}$ in the semi-linear set $C$ we introduce a copy
$\mathcal{A}_{i}$ of $\mathcal{A}$. All states of the copy of $\mathcal{A}$
are non-resetting and all states of $F$ are resetting in the
$\mathcal{A}_{i}$. At any point while a run is still in $\mathcal{A}$ and
would enter a state $f\in F$, we allow a non-deterministic to some
$\mathcal{A}_{i}$ and to reset the counters. For this, we first go to a
special resetting copy of $f$ and then transition to $\mathcal{A}_{i}$. We use
additional counters to mark in the semi-linear set in which $\mathcal{A}_{i}$
we are moving and modify the semi-linear set so that we do not count the base-
vector again when continuing the run in $\mathcal{A}_{i}$.

Formally, assume $C=\bigcup_{i\leq k}C_{i}$. Let
$\mathcal{A}^{\prime}=(Q^{\prime},\Sigma,(q_{0},0),\Delta^{\prime},F^{\prime},C^{\prime})$
of dimension $d+k+1$, where

$\displaystyle Q^{\prime}=$ $\displaystyle\ Q\times\\{0,1,\ldots,k\\}\cup
F\times\\{1,\ldots,k\\}\times\\{R\\},$ $\displaystyle F^{\prime}=$
$\displaystyle\ F\times\\{1,\ldots,k\\}\times\\{R\\}\cup
F\times\\{1,\ldots,k\\},$ $\displaystyle\Delta^{\prime}=$ $\displaystyle\
\\{((p,0),a,\mathbf{v}\cdot\mathbf{0}^{k+1},(q,0)),((p,i),a,\mathbf{v}\cdot\mathbf{e}_{i}^{k+1},(q,i))\mid(p,a,\mathbf{v},q)\in\Delta,1\leq
i\leq k\\}$ $\displaystyle\cup$ $\displaystyle\
\\{((q,0),a,\mathbf{v}\cdot(\mathbf{e}_{i}^{k+1}+\mathbf{e}_{k+1}^{k+1}),(f,i,R)\\}\mid(q,a,\mathbf{v},f)\in\Delta,f\in
F\\}$ $\displaystyle\cup$ $\displaystyle\
\\{((f,i,R),a,\mathbf{v}\cdot\mathbf{e}_{i}^{k+1},(q,i)\\}\mid(f,a,\mathbf{v},q)\in\Delta,f\in
F\\},\text{ and }$ $\displaystyle C^{\prime}=$ $\displaystyle\ \bigcup_{i\leq
k}C_{i}\cdot\\{(\mathbf{e}_{i}^{k+1}+\mathbf{e}_{k+1}^{k+1})\\}\cup\bigcup_{i\leq
k}\vec{C}_{i}\cdot\\{z\cdot\mathbf{e}_{i}^{k+1}\mid z\in\mathbb{N}\\},$

where $\vec{C}_{i}$ is defined as $C_{i}$ but without any base vectors. We
prove that $P_{\omega}(\mathcal{A})=W_{\omega}(\mathcal{A}^{\prime})$.

$\Rightarrow$ We first show $P_{\omega}(\mathcal{A})\subseteq
W_{\omega}(\mathcal{A}^{\prime})$. Let $\alpha\in P_{\omega}(\mathcal{A})$
with accepting run $r=r_{1}r_{2}r_{3}\dots$ where
$r_{i}=(p_{i-1},\alpha_{i},\mathbf{v}_{i},p_{i})$, and denote by
$f_{1}<f_{2}<\dots$ the positions of accepting hits of $r$. By the infinite
pigeonhole principle there is some $\ell\leq k$ such that infinitely many of
these accepting hits are in the linear set $C_{\ell}$. Denote by
$k_{1}<k_{2}<\ldots$ the subsequence of $f_{1},f_{2},\ldots$ of all accepting
hits in $C_{\ell}$.

This means $p_{k_{j}}\in F$ and $\rho(r_{1}\dots r_{k_{j}})\in C_{\ell}$ for
all $j\geq 1$. For $i<j$ let $r_{i,j}=r_{k_{i}}+1\dots r_{k_{j}}$. Now observe
that $\rho(r_{1}\dots r_{k_{\ell}})=\rho(r_{1}\dots
r_{k_{1}})+\rho(r_{1,2})+\rho(r_{2,3})+\dots+\rho(r_{\ell-1,\ell})$ for all
$\ell\geq 1$. In particular, we have $\rho(r_{1}\dots r_{k_{1}})\in C_{\ell}$
and $r_{i,i+1}\in\vec{C}_{\ell}$ for all $i<\ell$.

Let
$\hat{r}=\hat{r}_{1}\dots\hat{r}_{k_{1}-1}((p_{k_{1}-1},0),\alpha_{k_{1}},\mathbf{v}_{k_{1}}\cdot(\mathbf{e}_{\ell}^{k+1}+\mathbf{e}_{k+1}^{k+1}),(f,\ell,R))$,
where $\hat{r}_{i}=((p_{i-1},0)$,
$\alpha_{i},\mathbf{v}_{i}\cdot\mathbf{e}_{0}^{k+1},(p_{i},0))$ for all $i\leq
k_{1}-1$, and let
$r^{\prime}=((f,\ell,R),\alpha_{k_{1}+1},\mathbf{v}_{k_{1}+1}\cdot\mathbf{e}_{\ell}^{k+1},(p^{\prime}_{k_{1}+1},\ell))$
$r^{\prime}_{k_{i}+2}r^{\prime}_{k_{i}+3}\dots$ where
$r^{\prime}_{i}=((p^{\prime}_{i-1},\ell),\alpha_{i},\mathbf{v}\cdot\mathbf{e}_{\ell}^{k+1},(p^{\prime}_{i},\ell))$
for all $i\geq k_{1}+1$. Then $\hat{r}r^{\prime}$ is a run of
$\mathcal{A}^{\prime}$ on $\alpha$. Furthermore, this run is accepting, as we
can translate the positions of accepting hits of $r$ one-to-one to reset
positions of $\hat{r}r^{\prime}$, and by the choice of $\Delta^{\prime}$,
$C^{\prime}$ and the observations above. Hence $\alpha\in
W_{\omega}(\mathcal{A}^{\prime})$.

$\Leftarrow$ To see that $W_{\omega}(\mathcal{A}^{\prime})\subseteq
P_{\omega}(\mathcal{A})$, let $\alpha\in W_{\omega}(\mathcal{A}^{\prime})$
with accepting run
$r^{\prime}=r^{\prime}_{1}r^{\prime}_{2}r^{\prime}_{3}\dots$, where
$r^{\prime}_{i}=(p_{i-1}^{\prime},\alpha_{i},\mathbf{v}_{i}\cdot
u,p_{i}^{\prime})$ where ${p}_{i}^{\prime}\in Q^{\prime}$ and
$u\in\\{\mathbf{0}^{k+1},\mathbf{e}_{\ell}^{k+1},(\mathbf{e}_{\ell}^{k+1}+\mathbf{e}_{k+1}^{k+1})\mid$
$1\leq\ell\leq k\\}$, and denote by $0=k_{0}<k_{1}<k_{2}\dots$ the reset
positions of $r^{\prime}$. As no state in the first copy of $\mathcal{A}$ is
resetting and by the further construction of $\mathcal{A}^{\prime}$, we have
$p_{i}^{\prime}=(p_{i},0)$ for all $i<k_{1}$,
$p_{k_{1}}^{\prime}=(p_{k_{1}},\ell,R)$, and $p_{i}^{\prime}=(p_{i},\ell)$ for
all $i>k_{1}$ for some $\ell\leq k$. As the transition from
$p_{k_{1}-1}^{\prime}$ to $p_{k_{1}}^{\prime}$ is the only one where the
$k+1$rst of the new counters is set to $1$, and such a transition appears only