University of Bremen, Bremen, Germanygrobler@uni-
bremen.dehttps://orcid.org/0000-0001-8103-6440University of Bremen, Bremen,
Germanysabellek@uni-bremen.dehttps://orcid.org/0000-0001-8051-5749 University
of Bremen, Bremen, Germanysiebertz@uni-
bremen.dehttps://orcid.org/0000-0002-6347-1198 Mario Grobler, Leif Sabellek,
and Sebastian Siebertz <ccs2012> <concept>
<concept_id>10003752.10003766.10003770</concept_id> <concept_desc>Theory of
computation Automata over infinite objects</concept_desc>
<concept_significance>500</concept_significance> </concept> </ccs2012>
[500]Theory of computation Automata over infinite objects

###### Acknowledgements.

John Q. Open and Joan R. Access 2 42nd Conference on Very Important Topics
(CVIT 2016) 2024 December 24–27, 2016 Little Whinging, United Kingdom 42 23

# Remarks on Parikh-recognizable omega-languages000This paper subsumes the
unpublished results of [19, 20]. We thank Georg Zetzsche for his valuable
remarks.

Mario Grobler  Leif Sabellek  Sebastian Siebetz

###### Abstract

Several variants of Parikh automata on infinite words were recently introduced
by Guha et al. [FSTTCS, 2022]. We show that one of these variants coincides
with blind counter machine as introduced by Fernau and Stiebe [Fundamenta
Informaticae, 2008]. Fernau and Stiebe showed that every $\omega$-language
recognized by a blind counter machine is of the form
$\bigcup_{i}U_{i}V_{i}^{\omega}$ for Parikh recognizable languages
$U_{i},V_{i}$, but blind counter machines fall short of characterizing this
class of $\omega$-languages. They posed as an open problem to find a suitable
automata-based characterization. We introduce several additional variants of
Parikh automata on infinite words that yield automata characterizations of
classes of $\omega$-language of the form $\bigcup_{i}U_{i}V_{i}^{\omega}$ for
all combinations of languages $U_{i},V_{i}$ being regular or Parikh-
recognizable. When both $U_{i}$ and $V_{i}$ are regular, this coincides with
Büchi’s classical theorem. We study the effect of $\varepsilon$-transitions in
all variants of Parikh automata and show that almost all of them admit
$\varepsilon$-elimination. Finally we study the classical decision problems
with applications to model checking.

###### keywords:

Parikh automata, blind counter machines, infinite words, Büchi’s theorem

###### category:

##  1 Introduction

Finite automata find numerous applications in formal language theory, logic,
verification, and many more, in particular due to their good closure
properties and algorithmic properties. To enrich this spectrum of applications
even more, it has been a fruitful direction to add features to finite automata
to capture also situations beyond the regular realm.

One such possible extension of finite automata with counting mechanisms has
been introduced by Greibach in her study of blind and partially blind (one-
way) multicounter machines [18]. Blind multicounter machines are generalized
by weighted automata as introduced in [27]. Parikh automata (PA) were
introduced by Klaedtke and Rueß in [25]. A PA is a non-deterministic finite
automaton that is additionally equipped with a semi-linear set $C$, and every
transition is equipped with a $d$-tuple of non-negative integers. Whenever an
input word is read, $d$ counters are initialized with the values $0$ and every
time a transition is used, the counters are incremented by the values in the
tuple of the transition accordingly. An input word is accepted if the PA ends
in an accepting state and additionally, the resulting $d$-tuple of counter
values lies in $C$. Klaedtke and Rueß showed that PA are equivalent to
weighted automata over the group $(\mathbb{Z}^{k},+,\mathbf{0})$, and hence
equivalent to Greibach’s blind multicounter machines, as well as to reversal
bounded multicounter machines [2, 23]. Recently it was shown that these models
can be translated into each other using only logarithmic space [3]. In this
work we call the class of languages recognized by any of these models _Parikh
recognizable_. Klaedtke and Rueß [25] showed that the class of Parikh
recognizable languages is precisely the class of languages definable in weak
existential monadic second-order logic of one successor extended with linear
cardinality constraints. The class of Parikh-recognizable languages 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 not
Parikh-recognizable On finite words, blind counter automata, Parikh automata
and related models have been investigated extensively, extending [18, 25] for
example by affine PA and PA on letters [5, 6], bounded PA [7], two-way PA
[16], PA with a pushdown stack [24] as well as a combination of both [10],
history-deterministic PA [12], automata and grammars with valences [13, 22],
and several algorithmic applications, e.g. in the context of path logics for
querying graphs [15].

In the well-studied realm of verification of reactive systems, automata-
related approaches provide a powerful framework to tackle important problems
such as the model checking problem [1, 8, 9]. However, computations of systems
are generally represented as infinite objects, as we often expect them to not
terminate (but rather interact with the environment). Hence, automata
processing infinite words are suited for these tasks. One common approach is
the following: assume we are given a system, e.g. represented as a Kripke
structure $K$, and a specification represented as an automaton $\mathcal{A}$
(or any formalism that can be translated into one) accepting all
counterexamples. Then we can verify that the system has no bad computations by
solving intersection-emptiness of $K$ and $\mathcal{A}$. Yet again, the most
basic model of Büchi automata (which recognize $\omega$-regular languages) are
quite limited in their expressiveness, although they have nice closure
properties.

Let us consider two examples. In a three-user setting in an operating system
we would like to ensure that none of the users gets a lot more resources than
the other two. A corresponding specification of bad computations can be
modeled via the $\omega$-language $\\{\alpha\in\\{a,b,c\\}^{\omega}\mid\text{
there are infinitely many prefixes $w$ of $\alpha$ with
$|w|_{a}>|w|_{b}+|w|_{c}$}\\}$, stating that one user gets more resources than
the other two users combined infinitely often. As another example consider a
classical producer-consumer setting, where a producer continuously produces a
good, and a consumer consumes these goods continuously. We can model this
setting as an infinite word and ask that at no time the consumer has consumed
more than the producer has produced at this time. Bad computations can be
modeled via the $\omega$-language
$\\{\alpha\in\\{p,c\\}^{\omega}\mid\text{there is a prefix $w$ of $\alpha$
with $|w|_{c}>|w|_{p}$}\\}$. Such specifications are not $\omega$-regular, as
these require to “count arbitrarily”. This motivates the study of blind-
counter and Parikh automata on infinite words, which was initiated by Fernau
and Stiebe [14]. Independently, Klaedte and Rueß proposed possible extensions
of Parikh automata on infinite words. This line of research was recently
picked up by Guha et al. [21].

Guha et al. [21] introduced _safety, reachability, Büchi- and co-Büchi Parikh
automata_. These models provide natural generalization of studied automata
models with Parikh conditions on infinite words. One shortcoming of safety,
reachability and co-Büchi Parikh automata is that they do not generalize Büchi
automata, that is, they cannot recognize all $\omega$-regular languages. The
non-emptiness problem, which is highly relevant for model checking
applications, is undecidable for safety and co-Büchi Parikh automata.
Furthermore, none of these models has $\omega$-closure, meaning that for every
model there is a Parikh-recognizable language (on finite words) $L$ such that
$L^{\omega}$ is not recognizable by any of these models. They raised the
question whether (appropriate variants of) Parikh automata on infinite words
have the same expressive power as blind counter automata on infinite words.

Büchi’s famous theorem states that $\omega$-regular languages are
characterized as languages of the form $\bigcup_{i}U_{i}V_{i}^{\omega}$, where
the $U_{i}$ and $V_{i}$ are regular languages [4]. As a consequence of the
theorem, many properties of $\omega$-regular languages are inherited from
regular languages. For example, the non-emptiness problem for Büchi automata
can basically be solved by testing non-emptiness for nondeterministic finite
automata. In their systematic study of blind counter automata, Fernau and
Stiebe [14] considered the class $\mathcal{K}_{*}$, the class of
$\omega$-languages of the form $\bigcup_{i}U_{i}V_{i}^{\omega}$ for Parikh-
recognizable languages $U_{i}$ and $V_{i}$. They proved that the class of
$\omega$-languages recognizable by blind counter machines is a proper subset
of the class $\mathcal{K}_{*}$. They posed as an open problem to provide
automata models that capture classes of $\omega$-languages of the form
$\bigcup_{i}U_{i}V_{i}^{\omega}$ where $U_{i}$ and $V_{i}$ are described by a
certain mechanism.

In this work we propose _reachability-regular Parikh automata_ , _limit Parikh
automata_ , and _reset Parikh automata_ as new automata models.

We pick up the question of Fernau and Stiebe [14] to consider classes of
$\omega$-languages of the form $\bigcup_{i}U_{i}V_{i}^{\omega}$ where $U_{i}$
and $V_{i}$ are described by a certain mechanism. We define the four classes
$\mathcal{L}_{\mathsf{Reg,Reg}}^{\omega}$,
$\mathcal{L}_{\mathsf{PA,Reg}}^{\omega}$,
$\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$ and
$\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$ of $\omega$-languages of the form
$\bigcup_{i}U_{i}V_{i}^{\omega}$, where the $U_{i},V_{i}$ are regular or
Parikh-recognizable languages of finite words, respectively. By Büchi’s
theorem the class $\mathcal{L}_{\mathsf{Reg,Reg}}^{\omega}$ is the class of
$\omega$-regular languages.

We show that the newly introduced reachability-regular Parikh automata, which
are a small modification of reachability Parikh automata (as introduced by
Guha et al. [21]) capture exactly the class
$\mathcal{L}_{\mathsf{PA,Reg}}^{\omega}$. This model turns out to be
equivalent to limit Parikh automata. This model was hinted at in the
concluding remarks of [25].

Fully resolving the classification of the above mentioned classes we introduce
reset Parikh automata. In contrast to all other Parikh models, these are
closed under the $\omega$-operation, while maintaining all algorithmic
properties of PA (in particular, non-emptiness is $\NP$-complete and hence
decidable). We show that the class of Reset-recognizable $\omega$-languages is
a strict superclass of $\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$. We show that
appropriate graph-theoretic restrictions of reset Parikh automata exactly
capture the classes $\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$ and
$\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$, yielding the first automata
characterizations for these classes.

The automata models introduced by Guha et al. [21] do not have
$\varepsilon$-transitions, while blind counter machines have such transitions.
Towards answering the question of Guha et al. we study the effect of
$\varepsilon$-transitions in all Parikh automata models. We show that all
models except safety and co-Büchi Parikh automata admit
$\varepsilon$-elimination. This in particular answers the question of Guha et
al. [21] whether blind counter automata and Büchi Parikh automata have the
same expressive power over infinite words affirmative. We show that safety and
co-Büchi automata with $\varepsilon$-transitions are strictly more powerful
than their variants without $\varepsilon$-transitions, and in particular, they
give the models enough power to recognize all $\omega$-regular languages.

##  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$.

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}\ldots w_{n}\in\Sigma^{*}$ is a (possibly empty) sequence of
transitions $r=r_{1}\ldots 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_ 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$
with $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 Büchi automaton $\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 [4]).

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}$.

If every state of a Büchi automaton $\mathcal{A}$ is accepting, we call
$\mathcal{A}$ a _safety automaton_.

###  2.3 Semi-linear sets

For some $d\geq 1$, a _linear set_ of dimension $d$ 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 a 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 $C\subseteq\mathbb{N}^{c}$ and
$D\subseteq\mathbb{N}^{d}$. Then $C\cdot
D=\\{\mathbf{u}\cdot\mathbf{v}\mid\mathbf{u}\in C,\mathbf{v}\in
D\\}\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. We also consider
semi-linear sets over $(\mathbb{N}\cup\\{\infty\\})^{d}$, that is semi-linear
sets with an additional symbol $\infty$ for infinity. As usual, addition of
vectors and multiplication of a vector with a number is defined component-
wise, where $z+\infty=\infty+z=\infty+\infty=\infty$ for all $z\in\mathbb{N}$,
$z\cdot\infty=\infty\cdot z=\infty$ for all $z>0\in\mathbb{N}$, and
$0\cdot\infty=\infty\cdot 0=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 a finite 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_.

###  2.5 Graphs

A _(directed) graph_ $G$ consists of its vertex set $V(G)$ and edge set
$E(G)\subseteq V(G)\times V(G)$. In particular, a graph $G$ may have loops,
that is, edges of the form $(u,u)$. A _path_ from a vertex $u$ to a vertex $v$
in $G$ is a sequence of pairwise distinct vertices $v_{1}\dots v_{k}$ such
that $v_{1}=u$, $v_{k}=v$, and $(v_{i},v_{i+1})\in E(G)$ for all $1\leq i<k$.
Similarly, a _cycle_ in $G$ is a sequence of pairwise distinct vertices
$v_{1}\dots v_{k}$ such that $(v_{i},v_{i+1})\in E(G)$ for all $1\leq i<k$,
and $(v_{k},v_{1})\in E(G)$. If $G$ has no cylces, we call $G$ a directed
acyclic graph (DAG). For a subset $U\subseteq V(G)$, we denote by $G[U]$ the
graph $G$ _induced by_ $U$, i. e., the graph with vertex set $U$ and edge set
$\\{(u,v)\in E(G)\mid u,v\in U\\}$. A _strongly connected component_ (SCC) in
$G$ is a maximal subset $U\in V(G)$ such that for all $u,v\in U$ there is a
path from $u$ to $v$, i. e., all vertices in $U$ are reachable from each
other. We write $SCC(G)$ for the set of all strongly connected components of
$G$ (observe that $SCC(G)$ partitions $V(G)$). The _condensation_ of $G$,
written $C(G)$, is the DAG obtained from $G$ by contracting each SCC of $G$
into a single vertex, that is $V(C(G))=SCC(G)$ and $(U,V)\in E(C(G))$ if and
only if there is $u\in U$ and $v\in V$ with $(u,v)\in E(G)$. We call the SCCs
with no outgoing edges in $C(G)$ leaves. Note that an automaton can be seen as
a labeled graph. Hence, all definitions translate to automata by considering
the underlying graph (to be precise, an automaton can be seen as a labeled
multigraph; however, we simply drop parallel edges).

##  3 Parikh automata on infinite words

In this section, we recall the acceptance conditions of Parikh automata
operating on infinite words that were studied before in the literature and
introduce our new models. We make some easy observations and compare the
existing with the new automata models. We define only the non-deterministic
variants of these automata.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ be a PA. A run of $\mathcal{A}$
on an infinite word $\alpha=\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}$. The automata defined below differ only in their acceptance
conditions. In the following, whenever we say that an automaton $\mathcal{A}$
accepts an infinite word $\alpha$, we mean that there is an accepting run of
$\mathcal{A}$ on $\alpha$.

  1. 1.

The run $r$ satisfies the _safety condition_ if for every $i\geq 0$ we have
$p_{i}\in F$ and $\rho(r_{1}\dots r_{i})\in C$. We call a PA accepting with
the safety condition a _safety PA_ [21]. We define the $\omega$-language
recognized by a safety PA $\mathcal{A}$ as
$S_{\omega}(\mathcal{A})=\\{\alpha\in\Sigma^{\omega}\mid\mathcal{A}$ accepts
$\alpha\\}$.

  2. 2.

The run $r$ satisfies the _reachability condition_ if there is an $i\geq 1$
such that $p_{i}\in F$ and $\rho(r_{1}\dots r_{i})\in C$. We say there is an
_accepting hit_ in $r_{i}$. We call a PA accepting with the reachability
condition a _reachability PA_ [21]. We define the $\omega$-language recognized
by a reachability PA $\mathcal{A}$ as
$R_{\omega}(\mathcal{A})=\\{\alpha\in\Sigma^{\omega}\mid\mathcal{A}$ accepts
$\alpha\\}$.

  3. 3.

The run $r$ satisfies the _Büchi condition_ if there are infinitely many
$i\geq 1$ such that $p_{i}\in F$ and $\rho(r_{1}\dots r_{i})\in C$. We call a
PA accepting with the Büchi condition a _Büchi PA_ [21]. We define the
$\omega$-language recognized by a Büchi PA $\mathcal{A}$ as
$B_{\omega}(\mathcal{A})=\\{\alpha\in\Sigma^{\omega}\mid\mathcal{A}$ accepts
$\alpha\\}$.

Hence, a Büchi PA can be seen as a stronger variant of a reachability PA where
we require infinitely many accepting hits instead of a single one.

  4. 4.

The run $r$ satisfies the _co-Büchi condition_ if there is $i_{0}$ such that
for every $i\geq i_{0}$ we have $p_{i}\in F$ and $\rho(r_{1}\dots r_{i})\in
C$. We call a PA accepting with the co-Büchi condition a _co-Büchi PA_ [21].
We define the $\omega$-language recognized by a co-Büchi PA $\mathcal{A}$ as
$CB_{\omega}(\mathcal{A})=\\{\alpha\in\Sigma^{\omega}\mid\mathcal{A}$ accepts
$\alpha\\}$.

Hence, a co-Büchi PA can be seen as a weaker variant of safety PA where the
safety condition needs not necessarily be fulfilled from the beginning, but
from some point onwards.

Guha et al. [21] assume that reachability PA are complete, i.e., for every
$(p,a)\in Q\times\Sigma$ there are $\mathbf{v}\in\mathbb{N}^{d}$ and $q\in Q$
such that $(p,a,\mathbf{v},q)\in\Delta$, as incompleteness allows to express
additional safety conditions. We also make this assumption in order to study
“pure” reachability PA. In fact, we can assume that all models are complete,
as the other models can be completed by adding a non-accepting sink. We remark
that Guha et al. also considered _asynchronous_ reachability and Büchi PA,
where the Parikh condition does not necessarily need to be satisfied in
accepting states. However, for non-deterministic automata this does not change
the expressiveness of the considered models [21].

We now define the models newly introduced in this work. As already observed in
[21] among the above considered models only Büchi PA can recognize all
$\omega$-regular languages. For example,
$\\{\alpha\in\\{a,b\\}^{\omega}\mid|\alpha|_{a}=\infty\\}$ cannot be
recognized by safety PA, reachability PA or co-Büchi PA.

We first extend reachability PA with the classical Büchi condition to obtain
_reachability-regular PA_. In Theorem 4.13 we show that these automata
characterize $\omega$-languages of the form
$\mathcal{L}_{\mathsf{PA,Reg}}^{\omega}$, hence, providing a robust and
natural model.

  1. 5.

The run satisfies the _reachability and regularity condition_ if there is an
$i\geq 1$ such that $p_{i}\in F$ and $\rho(r_{1}\dots r_{i})\in C$, and there
are infinitely many $j\geq 1$ such that $p_{j}\in F$. We call a PA accepting
with the reachability and regularity condition a _reachability-regular_ PA. We
define the $\omega$-language recognized by a reachability-regular PA
$\mathcal{A}$ as
$RR_{\omega}(\mathcal{A})=\\{\alpha\in\Sigma^{\omega}\mid\mathcal{A}$ accepts
$\alpha\\}$ and call it reachability-regular.

Note that (in contrast to reachability PA) we may assume that reachability-
regular PA are complete without changing their expressiveness. Observe that
every $\omega$-regular language is reachability-regular, as we can turn an
arbitrary Büchi automaton into an equivalent reachability-regular PA by
labeling every transition with $0$ and setting $C=\\{0\\}$.

We next introduce _limit PA_ , which were proposed in the concluding remarks
of [25]. As we will prove in Theorem 4.13, this seemingly quite different
model is equivalent to reachability-regular PA.

  1. 6.

The run satisfies the _limit condition_ if there are infinitely many $i\geq 1$
such that $p_{i}\in F$, and if additionally $\rho(r)\in C$, where the $j$th
component of $\rho(r)$ is computed as follows. If there are infinitely many
$i\geq 1$ such that the $j$th component of $\mathbf{v}_{i}$ has a non-zero
value, then the $j$th component of $\rho(C)$ is $\infty$. In other words, if
the sum of values in a component diverges, then its value is set to $\infty$.
Otherwise, the infinite sum yields a positive integer. We call a PA accepting
with the limit condition a _limit PA_. We define the $\omega$-language
recognized by a limit PA $\mathcal{A}$ as
$L_{\omega}(\mathcal{A})=\\{\alpha\in\Sigma^{\omega}\mid\mathcal{A}$ accepts
$\alpha\\}$.

Still, none of the yet introduced models have $\omega$-closure. This
shortcoming is addressed with the following two models, which will turn out to
be equivalent and form the basis of the automata characterization of
$\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$ and
$\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$.

  1. 7.

The run satisfies the _strong reset condition_ if the following holds. Let
$k_{0}=0$ and denote by $k_{1}<k_{2}<\dots$ the positions of all accepting
states in $r$. Then $r$ is accepting 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
call a PA accepting with the strong reset condition a _strong reset PA_. We
define the $\omega$-language recognized by a strong reset PA $\mathcal{A}$ as
$SR_{\omega}(\mathcal{A})=\\{\alpha\in\Sigma^{\omega}\mid\mathcal{A}$ accepts
$\alpha\\}$.

  2. 8.

The run satisfies the _weak reset condition_ 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 call a PA
accepting with the weak reset condition a _weak reset PA_. We define the
$\omega$-language recognized by a weak reset PA $\mathcal{A}$ as
$W\\!R_{\omega}(\mathcal{A})=\\{\alpha\in\Sigma^{\omega}\mid\mathcal{A}$
accepts $\alpha\\}$.

Intuitively worded, whenever a strong reset PA enters an accepting state, the
Parikh condition _must_ be satisfied. Then the counters are reset. Similarly,
a weak reset PA may reset the counters whenever there is an accepting hit, and
they must reset infinitely often, too. In the following we will often just
speak of reset PA without explicitly stating whether they are weak or strong.
In this case, we mean the strong variant. We will show the equivalence of the
two models in 5.11 and 5.13.

$q_{0}$$q_{1}$$b,\begin{pmatrix}0\\\ 1\end{pmatrix}$$a,\begin{pmatrix}1\\\
0\end{pmatrix}$$a,\begin{pmatrix}1\\\ 0\end{pmatrix}$$b,\begin{pmatrix}0\\\
1\end{pmatrix}$ Figure 1: The automaton $\mathcal{A}$ with
$C=\\{(z,z^{\prime}),(z,\infty)\mid z^{\prime}\geq z\\}$ from 3.1.

######  Example 3.1.

Let $\mathcal{A}$ be the automaton in Figure 1 with
$C=\\{(z,z^{\prime}),(z,\infty)\mid z^{\prime}\geq z\\}$.

  * •

If we interpret $\mathcal{A}$ as a PA (over finite words), then we have
$L(\mathcal{A})=\\{w\in\\{a,b\\}^{*}\cdot\\{b\\}\mid|w|_{a}\leq|w|_{b}\\}\cup\\{\varepsilon\\}$.
The automaton is in the accepting state at the very beginning and every time
after reading a $b$. The first counter counts the occurrences of letter $a$,
the second one counts occurrences of $b$. By definition of $C$ the automaton
only accepts when the second counter value is greater or equal to the first
counter value (note that vectors containing an $\infty$-entry have no
additional effect).

  * •

If we interpret $\mathcal{A}$ as a safety PA, then we have
$S_{\omega}(\mathcal{A})=\\{b\\}^{\omega}$. As $q_{1}$ is not accepting, only
the $b$-loop on $q_{0}$ may be used.

  * •

If we interpret $\mathcal{A}$ as a reachability PA, then we have
$R_{\omega}(\mathcal{A})=\\{\alpha\in\\{a,b\\}^{\omega}\mid\alpha$ has a
prefix in $L(\mathcal{A})\\}$. The automaton has satisfied the reachability
condition after reading a prefix in $L(\mathcal{A})$ and accepts any
continuation after that.

  * •

If we interpret $\mathcal{A}$ as a Büchi PA, then we have
$B_{\omega}(\mathcal{A})=L(\mathcal{A})^{\omega}$. The automaton accepts an
infinite word if infinitely often the Parikh condition is satisfied in the
accepting state. Observe that $C$ has no base vector and the initial state as
well as the accepting state have the same outgoing transitions.

  * •

If we interpret $\mathcal{A}$ as a co-Büchi PA, then we have
$CB_{\omega}(\mathcal{A})=L(\mathcal{A})\cdot\\{b\\}^{\omega}$. This is
similar to the safety PA, but the accepted words may have a finite “non-safe”
prefix from $L(\mathcal{A})$.

  * •

If we interpret $\mathcal{A}$ as a reachability-regular PA, then we have
$RR_{\omega}(\mathcal{A})=\\{\alpha\in\\{a,b\\}^{\omega}\mid\alpha\text{ has a
prefix}$ in $L(\mathcal{A})\text{ and }|\alpha|_{b}=\infty\\}$. After having
met the reachability condition the automaton still needs to satisfy the Büchi
condition, which enforces infinitely many visits of the accepting state.

  * •

If we interpret $\mathcal{A}$ as a limit PA, then we have
$L_{\omega}(\mathcal{A})=\\{\alpha\in\\{a,b\\}^{\omega}\mid|\alpha|_{a}<\infty\\}$.
The automaton must visit the accepting state infinitely often. At the same
time the extended Parikh image must belong to $C$, which implies that the
infinite word contains only some finite number $z$ of letter $a$ (note that
only the vectors of the form $(z,\infty)$ have an effect here, as at least one
symbol must be seen infinitely often by the infinite pigeonhole principle).

  * •

If we interpret $\mathcal{A}$ as a weak reset PA, then we have
$W\\!R_{\omega}(\mathcal{A})=L(\mathcal{A})^{\omega}$. As a weak reset PA may
(but is not forced to) reset the counters upon visiting the accepting state,
the automaton may reset every time a (finite) infix in $L(\mathcal{A})$ has
been read.

  * •

If we interpret $\mathcal{A}$ as a strong reset PA, then we have
$SR_{\omega}(\mathcal{A})=\\{b^{*}a\\}^{\omega}\cup\\{b^{*}a\\}^{*}\cdot\\{b\\}^{\omega}$.
Whenever the automaton reaches an accepting state also the Parikh condition
must be satisfied. This implies that the $a$-loop on $q_{1}$ may never be
used, as this would increase the first counter value to at least 2, while the
second counter value is 1 upon reaching the accepting state $q_{0}$ (which
resets the counters).

The automaton $\mathcal{A}$ in the last example is deterministic. We note that
$L_{\omega}(\mathcal{A})$ is not deterministic $\omega$-regular but
deterministic limit PA-recognizable.

##  4 Büchi-like characterizations

It was observed in [21] that Büchi PA recognize a strict subset of
$\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$. In this section we first show that
the class of reset PA-recognizable $\omega$-languages is a strict superset of
$\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$. Then we provide an automata-based
characterization of
$\mathcal{L}_{\mathsf{PA,Reg}}^{\omega},\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$,
and $\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$. Towards this goal we first
establish some closure properties.

Guha et al. [21] have shown that safety, reachability, Büchi, and co-Büchi PA
are closed under union using a modification of the standard construction for
PA, i. e., taking the disjoint union of the automata (introducing a fresh
initial state), and the disjoint union of the semi-linear sets, where
disjointness is achieved by “marking” every vector in the first set by an
additional $1$ (increasing the dimension by 1), and all vectors in the second
set by an additional $2$. We observe that the same construction also works for
reachability-regular and limit PA, and a small modification is sufficient to
make the construction also work for reset PA. We leave the details to the
reader.

######  Lemma 4.1.

The classes of reachability-regular, limit PA-recognizable, and reset PA-
recognizable $\omega$-languages are closed under union.

Furthermore, we show that these classes, as well as the class of Büchi PA-
recognizable $\omega$-languages, are closed under left-concatenation with PA-
recognizable languages. We provide some details in the next lemma, as we will
need to modify the standard construction in such a way that we do not need to
keep accepting states of the PA on finite words. This will help to
characterize $\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$ via (restricted) reset
PA.

######  Lemma 4.2.

The classes of reachability-regular, limit PA-recognizable, reset PA-
recognizable, and Büchi PA-recognizable $\omega$-languages are closed under
left-concatenation with PA-recognizable languages.

######  Proof 4.3.

We begin with reset PA. Let
$\mathcal{A}_{1}=(Q_{1},\Sigma,q_{1},\Delta_{1},F_{1},C_{1})$ be a PA of
dimension $d_{1}$ and let
$\mathcal{A}_{2}=(Q_{2},\Sigma,q_{2},\Delta_{2},F_{2},C_{2})$ be a reset PA of
dimension $d_{2}$. We sketch the construction of a reset PA $\mathcal{A}$ if
dimension $d_{1}+d_{2}$ that recognizes $L(\mathcal{A}_{1})\cdot
SR_{\omega}(\mathcal{A})$. We assume wlog that $q_{2}$ is accepting (this can
be achieved by introducing a fresh initial state). Furthermore, for now we
assume that $\varepsilon\notin L(\mathcal{A}_{1})$, that is, every accepting
run of $\mathcal{A}_{1}$ is not empty. Again, $\mathcal{A}$ consists of
disjoint copies of $\mathcal{A}_{1}$ and $\mathcal{A}_{2}$ but only the
accepting states of $\mathcal{A}_{2}$ remain accepting, and the initial state
of $\mathcal{A}$ is $q_{1}$. All transitions of the copy of $\mathcal{A}_{1}$
use the first $d_{1}$ counters (that is, the remaining $d_{2}$ counters are
always 0), and, likewise, the transitions of $\mathcal{A}_{2}$ only use the
last $d_{2}$ counters (that is, the first $d_{1}$ counters are always 0),
Finally, we copy every transition of $\mathcal{A}_{1}$ that leads to an
accepting state of $\mathcal{A}_{1}$ such that it also leads to $q_{2}$, that
is, we add the transitions $\\{(p,a,\mathbf{v}\cdot
0^{d_{2}},q_{2})\mid(p,a,\mathbf{v},q)\in\Delta_{1},q\in F_{1}\\}$. The semi-
linear set $C$ of $\mathcal{A}$ is
$C_{1}\cdot\\{0^{d_{2}}\\}\cup\\{0^{d_{1}}\\}\cdot C_{2}$. As every accepting
run of $\mathcal{A}_{1}$ is non-empty by assumption, $\mathcal{A}$ may guess
the last transition of every accepting run of $\mathcal{A}_{1}$ and replace it
with one of the new transitions that leads to $\mathcal{A}_{2}$ instead. As
$q_{2}$ is accepting, the counters are reset, which justifies the choice of
$C$. Now, if $\varepsilon\in L(\mathcal{A}_{1})$, observe that
$L(\mathcal{A}_{1})\cdot
SR_{\omega}(\mathcal{A}_{2})=(L(\mathcal{A}_{1})\setminus\\{\varepsilon\\}\cdot
SR_{\omega}(\mathcal{A}_{2}))\cup SR_{\omega}(\mathcal{A}_{2})$. Hence, we may
remove $\varepsilon$ from $L(\mathcal{A}_{1})$ by replacing $q_{1}$ by a fresh
non-accepting copy and use the closure under union. Hence, in any case only
the copies of accepting states of $\mathcal{A}_{2}$ remain accepting; in
particular no state of $\mathcal{A}_{1}$ is accepting in the corresponding
copy of $\mathcal{A}$.

The construction for reachability-regular PA, limit PA and Büchi PA is very
similar. The only difference is that we choose $C=C_{1}\cdot C_{2}$ for the
semi-linear set of $\mathcal{A}$, as counters are never reset here.

Before we continue, we show that we can normalize PA (on finite words) such
that the initial state is the only accepting state. This observation
simplifies several proofs in this section.

######  Lemma 4.4.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ be a PA of dimension $d$. Then
there exists an equivalent PA $\mathcal{A}^{\prime}$ of dimension $d+1$ with
the following properties.

  * •

The initial state of $\mathcal{A}^{\prime}$ is the only accepting state.

  * •

$SCC(\mathcal{A}^{\prime})=\\{Q\\}$.

We say that $\mathcal{A}^{\prime}$ is _normalized_.

######  Proof 4.5.

The normalized PA $\mathcal{A}^{\prime}$ is obtained from $\mathcal{A}$ by
adding a fresh state $q_{0}^{\prime}$, which is the initial state and only
accepting state, and which inherits all outgoing transitions from $q_{0}$ and
all incoming transitions from the accepting states. Furthermore, all
transitions get a new counter, which is set to 0 except for the new incoming
transitions of $q_{0}^{\prime}$ where the counter is set to $1$, and all
vectors in $C$ are concatenated with $1$ (and we add the all zero-vector if we
want to accept $\varepsilon$). Finally, we remove all states that cannot reach
$q^{\prime}_{0}$ (such states can appear when shortcutting the incoming
transitions of $F$, and are useless in the sense that their removal does not
change the accepted language; however, this removal is necessary for the
second property). We observe that $L(\mathcal{A})=L(\mathcal{A}^{\prime})$.

Observe that we have
$SR_{\omega}(\mathcal{A}^{\prime})=L(\mathcal{A})^{\omega}$, that is, every
normalized PA interpreted as a reset PA recognizes the $\omega$-closure of the
language recognized by the PA. As an immediate consequence we obtain the
following corollary.

######  Corollary 4.6.

The class of reset PA-recognizable $\omega$-languages is closed under the
$\omega$-operation.

Combining these results we obtain that every $\omega$-language in
$\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$, i.e., every $\omega$-language of the
form $\bigcup_{i}U_{i}V_{i}^{\omega}$ is reset PA-recognizable. We show that
the other direction does not hold, i.e., the inclusion is strict.

######  Lemma 4.7.

The class $\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$ is a strict subclass of the
class of reset PA-recognizable $\omega$-languages.

######  Proof 4.8.

The inclusion is a direct consequence of 4.1, 4.2, and 4.6. Hence we show that
the inclusion is strict.

Consider the $\omega$-language $L=\\{a^{n}b^{n}\mid n\geq
1\\}^{\omega}\cup\\{a^{n}b^{n}\mid n\geq 1\\}^{*}\cdot\\{a\\}^{\omega}$. This
$\omega$-language is reset PA-recognizable, as witnessed by the strong reset
PA in Figure 2 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 2: The strong
reset PA for $L=\\{a^{n}b^{n}\mid n\geq 1\\}^{\omega}\cup\\{a^{n}b^{n}\mid
n\geq 1\\}^{*}\cdot\\{a\\}^{\omega}$ with $C=\\{(z,z)\mid z\in\mathbb{N}\\}$.

We claim that $L\notin\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$. Assume towards a
contraction that $L\in\mathcal{L}_{\mathsf{PA,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$.

###  4.1 Characterization of Büchi Parikh automata

As mentioned in the last section, the class of $\omega$-languages recognized
by Büchi PA is a strict subset of $\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$, i.
e., languages of the form $\bigcup_{i}U_{i}V_{i}^{\omega}$ for Parikh-
recognizable $U_{i}$ and $V_{i}$. In this subsection we show that a
restriction of the PA recognizing the $V_{i}$ is sufficient to exactly capture
the expressiveness of Büchi PA. To be precise, we show the following.

######  Lemma 4.9.

The following are equivalent for all $\omega$-languages
$L\subseteq\Sigma^{\omega}$:

  1. 1.

$L$ is Büchi PA-recognizable.

  2. 2.

$L$ is of the form $\bigcup_{i}U_{i}V_{i}^{\omega}$, where
$U_{i}\in\Sigma^{*}$ is Parikh-recognizable and $V_{i}\in\Sigma^{*}$ is
recognized by a normalized PA where $C$ is a linear set without base vector.

We note that we can translate every PA (with a linear set $C$) into an
equivalent normalized PA by 4.4. However, this construction adds a base
vector, as we concatenate $\\{1\\}$ to $C$. In fact, this can generally not be
avoided without losing expressiveness. However, this loss of expressiveness is
exactly what we need to characterize the class of $\omega$-languages
recognized by Büchi PA as stated in the previous lemma. The main reason for
this is pointed out in the following lemma.

######  Lemma 4.10.

Let $L$ be a language recognized by a (normalized) PA
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta,\\{q_{0}\\},C)$ where $C$ is linear and
has no base vector. Then we have
$B_{\omega}(\mathcal{A})=L(\mathcal{A})^{\omega}$.

######  Proof 4.11.

In this proof we assume that $C=\\{b_{1}z_{1}+\dots+b_{\ell}z_{\ell}\mid
z_{1},\dots z_{\ell}\in\mathbb{N}\\}$ for some $\ell\geq 1$.

$\Rightarrow$ To show $B_{\omega}(\mathcal{A})\subseteq
L(\mathcal{A})^{\omega}$, let $\alpha\in B_{\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})$. As $r$ satisfies the Büchi
condition and $\mathcal{A}$ is normalized there are infinitely many accepting
hits, that is, infinitely many $i$ such that $p_{i}=q_{0}$ and
$\rho(r_{1}\dots r_{i})\in C$. By Dickson’s Lemma [11], there is an infinite
monotone (sub)sequence of accepting hits $s_{1}<s_{2}<\dots$, i. e., for all
$j>i$ we have $\rho(r_{1}\dots r_{s_{i}})=b_{1}z_{1}+\dots+b_{\ell}z_{\ell}$
for some $z_{i}\in\mathbb{N}$ and $\rho(r_{1}\dots
r_{s_{j}})=b_{1}z^{\prime}_{1}+\dots+b_{\ell}z^{\prime}_{\ell}$ for some
$z^{\prime}_{i}\in\mathbb{N}$, and $z^{\prime}_{k}\geq z_{k}$ for all
$k\leq\ell$. Hence, every infix $\alpha[s_{i}+1,s_{i+1}]$ for $i\geq 0$
(assuming $s_{0}=0$) is accepted by $\mathcal{A}$.

$\Leftarrow$ To show $L(\mathcal{A})^{\omega}\subseteq
B_{\omega}(\mathcal{A})$, let $w_{1}w_{2}\dots\in L(\mathcal{A})^{\omega}$
such that $w_{i}\in L(\mathcal{A})$ for all $i\geq 1$. Let $r^{(i)}$ be an
accepting run of $\mathcal{A}$ on $w_{i}$. Observe that for every $i\geq 1$ we
have that $r^{(1)}\dots r^{(i)}$ is an accepting run of $\mathcal{A}$ on
$w_{1}\dots w_{i}$, as $C$ has no base vector, and hence we have
$\rho(r^{(1)}\dots r^{(i)})=\rho(r^{(1)})+\dots+\rho(r^{(i)})\in C$. Hence,
the infinite sequence $r^{(1)}r^{(2)}\dots$ is a run of $\mathcal{A}$ on
$w_{1}w_{2}\dots$ with infinitely many accepting hits. Hence
$w_{1}w_{2}\dots\in B_{\omega}(\mathcal{A})$.

This is the main ingredient to prove 4.9.

######  Proof 4.12 (Proof of 4.9).

We note that the proof in [21] showing that every $\omega$-language $L$
recognized by a Büchi-PA is of the form $\bigcup_{i}U_{i}V_{i}$ for PA-
recognizable $U_{i}$ and $V_{i}$ already constructs PA for the $V_{i}$ of the
desired form. This shows the implication $(1)\Rightarrow(2)$.

To show the implication $(2)\Rightarrow(1)$, we use that the $\omega$-closure
of languages recognized by PA of the stated form is Büchi PA-recognizable by
4.10. As Büchi PA are closed under left-concatenation with PA-recognizable
languages (4.2) and union [21], the claim follows.

###  4.2 Characterization of $\mathcal{L}_{\mathsf{PA,Reg}}^{\omega}$

In this subsection we characterize $\mathcal{L}_{\mathsf{PA,Reg}}^{\omega}$ by
showing the following equivalences.

######  Theorem 4.13.

The following are equivalent for all $\omega$-languages
$L\subseteq\Sigma^{\omega}$.

  1. 1.

$L$ is of the form $\bigcup_{i}U_{i}V_{i}^{\omega}$, where
$U_{i}\in\Sigma^{*}$ is Parikh-recognizable, and $V_{i}\subseteq\Sigma^{*}$ is
regular.

  2. 2.

$L$ is limit PA-recognizable.

  3. 3.

$L$ is reachability-regular.

Observe that in the first item we may assume that $L$ is of the form
$\bigcup_{i}U_{i}V_{i}$, where $U_{i}\in\Sigma^{*}$ is Parikh-recognizable,
and $V_{i}\subseteq\Sigma^{\omega}$ is $\omega$-regular. Then, by simple
combinatorics and Büchi’s theorem we have
$\bigcup_{i}U_{i}V_{i}=\bigcup_{i}U_{i}(\bigcup_{j_{i}}X_{j_{i}}Y_{j_{i}}^{\omega})=\bigcup_{i,j_{i}}U_{i}(X_{j_{i}}Y_{j_{i}}^{\omega})=\bigcup_{i,j_{i}}(U_{i}X_{j_{i}})Y_{j_{i}}^{\omega}$,
for regular languages $X_{j_{i}},Y_{j_{i}}$, where $U_{i}X_{j_{i}}$ is Parikh-
recognizable, as Parikh-recognizable languages are closed under concatenation.
111To the best of our knowledge there is no explicit construction for
concatenation in the literature for PA on finite words, however, a standard
construction very similar to the one of 4.2 works.

To simplify the proof, it is convenient to consider the following
generalizations of Büchi automata. A _transition-based generalized Büchi
automaton_ (TGBA) is a tuple $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,\mathcal{T})$
where $\mathcal{T}\subseteq 2^{\Delta}$ is a collection of sets of
transitions. Then a run $r_{1}r_{2}r_{3}\dots$ of $\mathcal{A}$ is accepting
if for all $T\in\mathcal{T}$ there are infinitely many $i$ such that $r_{i}\in
T$. It is well-known that TGBA have the same expressiveness as Büchi automata
[17].

Theorem 4.13 will be a direct consequence from the following lemmas. The first
lemma shows the implication $(1)\Rightarrow(2)$.

######  Lemma 4.14.

If $L\in\mathcal{L}_{\mathsf{PA,Reg}}^{\omega}$, then $L$ is limit PA-
recognizable.

######  Proof 4.15.

As the class of limit PA-recognizable $\omega$-languages is closed under union
by 4.1, it is sufficient to show how to construct a limit PA for an
$\omega$-language of the form $L=UV^{\omega}$, where $U$ is Parikh-
recognizable and $V$ is regular.

Let $\mathcal{A}_{1}=(Q_{1},\Sigma,q_{1},\Delta_{1},F_{1},C)$ be a PA with
$L(\mathcal{A}_{1})=U$ and
$\mathcal{A}_{2}=(Q_{2},\Sigma,q_{2},\Delta_{2},F_{2})$ be a Büchi automaton
with $L_{\omega}(\mathcal{A}_{2})=V^{\omega}$. We use the following standard
construction for concatenation. Let $\mathcal{A}=(Q_{1}\cup
Q_{2},\Sigma,q_{1},\Delta,F_{2},C)$ be a limit PA where

$\Delta=\Delta_{1}\cup\\{(p,a,\mathbf{0},q)\mid(p,a,q)\in\Delta_{2}\\}\cup\\{(f,a,\mathbf{0},q)\mid(q_{2},a,q)\in\Delta_{2},f\in
F_{1}\\}.$

We claim that $L_{\omega}(\mathcal{A})=L$.

$\Rightarrow$ To show $L_{\omega}(\mathcal{A})\subseteq L$, let $\alpha\in
L_{\omega}(\mathcal{A})$ with accepting run $r_{1}r_{2}r_{3}\dots$ where
$r_{i}=(p_{i-1},\alpha_{i},\mathbf{v}_{i},p_{i})$. As only the states in
$F_{2}$ are accepting, there is a position $j$ such that $p_{j-1}\in F_{1}$
and $p_{j}\in Q_{2}$. In particular, all transitions of the copy of
$\mathcal{A}_{2}$ are labeled with $\mathbf{0}$, i. e.,
$\mathbf{v}_{i}=\mathbf{0}$ for all $i\geq j$. Hence $\rho(r)=\rho(r_{1}\dots
r_{j-1})\in C$ (in particular, there is no $\infty$ value in $\rho(r)$). We
observe that $r_{1}\dots r_{j-1}$ is an accepting run of $\mathcal{A}_{1}$ on
$\alpha[1,j-1]$, as $p_{j-1}\in F_{1}$ and $\rho(r_{1}\dots r_{j-1})\in C$.
For all $i\geq j$ let $r^{\prime}_{i}=(p_{i-1},\alpha_{i},p_{i})$. Observe
that $(q_{2},\alpha_{j},p_{j})r^{\prime}_{j+1}r^{\prime}_{j+2}\dots$ is an
accepting run of $\mathcal{A}_{2}$ on
$\alpha_{j}\alpha_{j+1}\alpha_{j+2}\dots$, hence $\alpha\in
L(\mathcal{A}_{1})\cdot L_{\omega}(\mathcal{A}_{2})=L$.

$\Leftarrow$ To show $L=UV^{\omega}\subseteq L_{\omega}(\mathcal{A})$, let
$w\in L(\mathcal{A}_{1})=U$ with accepting run $s$, and $\alpha\in
L_{\omega}(\mathcal{A}_{2})=V^{\omega}$ with accepting run
$r=r_{1}r_{2}r_{3}\dots$, where $r_{i}=(p_{i-1},\alpha_{1},p_{i})$. Observe
that $s$ is also a partial run of $\mathcal{A}$ on $w$, ending in an accepting
state $f$. By definition of $\Delta$, we can continue the run $s$ in
$\mathcal{A}$ basically as in $r$. To be precise, let
$r^{\prime}_{1}=(f,\alpha_{1},\mathbf{0},p_{1})$, and, for all $i>1$ let
$r^{\prime}_{i}=(p_{i-1},\alpha_{i},\mathbf{0},p_{i})$. Then
$sr^{\prime}_{1}r^{\prime}_{2}r^{\prime}_{3}\dots$ is an accepting run of
$\mathcal{A}$ on $w\alpha$, hence $w\alpha\in L_{\omega}(\mathcal{A})$.

Observe that the construction in the proof of the lemma works the same way
when we interpret $\mathcal{A}$ as a reachability-regular PA (every visit of
an accepting state has the same good counter value; this argument is even true
if we interpret $\mathcal{A}$ as a Büchi PA), showing the implication
$(1)\Rightarrow(3)$.

######  Corollary 4.16.

If $L\in\mathcal{L}_{\mathsf{PA,Reg}}^{\omega}$, then $L$ is reachability-
regular.

For the backwards direction we need an auxiliary lemma, essentially stating
that semi-linear sets over $C\subseteq(\mathbb{N}\cup\\{\infty\\})^{d}$ can be
modified such that $\infty$-entries in vectors in $C$ are replaced by
arbitrary integers, and remain semi-linear.

######  Lemma 4.17.

Let $C\subseteq(\mathbb{N}\cup\\{\infty\\})^{d}$ be semi-linear and
$D\subseteq\\{1,\dots,d\\}$. Let $C_{D}\subseteq\mathbb{N}^{d}$ be the set
obtained from $C$ by the following procedure.

  1. 1.

Remove every vector $\mathbf{v}=(v_{1},\dots,v_{d})$ where $v_{i}=\infty$ for
an $i\notin D$.

  2. 2.

As long as $C_{D}$ contains a vector $\mathbf{v}=(v_{1},\dots,v_{d})$ with
$v_{i}=\infty$ for an $i\leq d$: replace $\mathbf{v}$ by all vectors of the
form $(v_{1},\dots v_{i-1},z,v_{i+1},\dots,v_{d})$ for $z\in\mathbb{N}$.

Then $C_{D}$ is semi-linear.

######  Proof 4.18.

For a vector
$\mathbf{v}=(v_{1},\dots,v_{d})\in(\mathbb{N}\cup\\{\infty\\})^{d}$, let
$\mathsf{Inf}(\mathbf{v})=\\{i\mid v_{i}=\infty\\}$ denote the positions of
$\infty$-entries in $\mathbf{v}$. Furthermore, let
$\bar{}\mathbf{v}=(\bar{v}_{1},\dots,\bar{v}_{d})$ denote the vector obtained
from $\mathbf{v}$ by replacing every $\infty$-entry by 0, i. e.,
$\bar{v}_{i}=0$ if $v_{i}=\infty$, and $\bar{v}_{i}=v_{i}$ otherwise.

We carry out the following procedure for every linear set of the semi-linear
set independently, hence we assume that
$C=\\{b_{0}+b_{1}z_{1}+\dots+b_{\ell}z_{\ell}\mid
z_{1},\dots,z_{\ell}\in\mathbb{N}\\}$ is linear. We also assume that there is
no $b_{j}$ with $\mathsf{Inf}(b_{j})\not\subseteq D$, otherwise, we simply
remove it.

Now, if $\mathsf{Inf}(b_{0})\not\subseteq D$, then $C_{D}=\varnothing$, as
this implies that every vector in $C$ has an $\infty$-entry at an unwanted
position (the first item of the lemma). Otherwise,
$C_{D}=\\{b_{0}+\sum_{j\leq\ell}\bar{b}_{j}z_{j}+\sum_{i\in\mathsf{Inf}(b_{j})}\mathbf{e}_{i}z_{ij}\mid
z_{j},z_{ij}\in\mathbb{N}\\}$, which is linear by definition.

We are now ready to prove the following lemma, showing the implication
$(2)\Rightarrow(1)$.

######  Lemma 4.19.

If $L$ is limit PA-recognizable, then
$L\in\mathcal{L}_{\mathsf{PA,Reg}}^{\omega}$.

######  Proof 4.20.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ be an limit PA of dimension $d$.
The idea is as follows. We guess a subset $D\subseteq\\{1,\dots,d\\}$ of
counters whose values we expect to be $\infty$. Observe that every counter not
in $D$ has a finite value, hence for every such counter there is a point where
all transitions do not increment the counter further. For every subset
$D\subseteq\\{1,\dots,d\\}$ we decompose $\mathcal{A}$ into a PA and a TGBA.
In the first step we construct a PA where every counter not in $D$ reaches its
final value and is verified. In the second step we construct a TGBA ensuring
that for every counter in $D$ at least one transition adding a non-zero value
to that counter is used infinitely often. This can be encoded directly into
the TGBA. Furthermore we delete all transitions that modify counters not in
$D$.

Fix $D\subseteq\\{1,\dots,d\\}$ and $f\in F$, and define the PA
$\mathcal{A}^{D}_{f}=(Q,\Sigma,q_{0},\Delta,\\{f\\},C_{D})$ where $C_{D}$ is
defined as in 4.17. Furthermore, we define the TGBA
$\mathcal{B}^{D}_{f}=(Q,\Sigma,f,\Delta^{D},\mathcal{T}^{D})$ where
$\Delta^{D}$ contains the subset of transitions of $\Delta$ where the counters
not in $D$ have zero-values (just the transitions without vectors for the
counters, as we construct a TGBA). On the other hand, for every counter $i$ in
$D$ there is one acceptance component in $\mathcal{T}^{D}$ that contains
exactly those transitions (again without vectors) where the $i$th counter has
a non-zero value. Finally, we encode the condition that at least one accepting
state in $F$ needs to by seen infinitely often in $\mathcal{T}^{D}$ by further
adding the component $\\{(p,a,q)\in\Delta\mid q\in F\\}$ (i. e. now we need to
see an incoming transition of a state in $F$ infinitely often).

We claim that $L_{\omega}(\mathcal{A})=\bigcup_{D\subseteq\\{1,\dots,d\\},f\in
F}L(\mathcal{A}^{D}_{f})\cdot L_{\omega}(\mathcal{B}^{D}_{f})$, which by the
comment below Theorem 4.13 and the equivalence of TGBA and Büchi automata
implies the statement of the lemma.

$\Rightarrow$ To show
$L_{\omega}(\mathcal{A})\subseteq\bigcup_{D\subseteq\\{1,\dots,d\\},f\in
F}L(\mathcal{A}^{D}_{f})\cdot L_{\omega}(\mathcal{B}^{D}_{f})$, let $\alpha\in
L_{\omega}(\mathcal{A})$ with accepting run $r_{1}r_{2}r_{3}\dots$ where
$r_{i}=(p_{i-1},\alpha_{i},\mathbf{v}_{i},p_{i})$. Let $D$ be the positions of
$\infty$-entries in $\rho(r)=(v_{1},\dots,v_{d})$. As the $v_{i}$ with
$i\notin D$ have integer values, there is a position $j$ such that in all
$\mathbf{v}_{k}$ for $k\geq j$ the $i$-th entry of $\mathbf{v}_{k}$ is 0. Let
$\ell\geq j$ be minimal such that $p_{\ell}$ in $F$. We split $\alpha=w\beta$,
where $w=\alpha[1,\ell]$, and $\beta=\alpha_{\ell+1}\alpha_{\ell+2}\dots$.

First we argue that $w\in L_{\omega}(\mathcal{A}^{D}_{p_{\ell}})$. Observe
that $\mathcal{A}^{D}_{p_{\ell}}$ inherits all transitions from $\mathcal{A}$,
hence $r_{1}\dots r_{\ell}$ is a run of $\mathcal{A}^{D}_{p_{\ell}}$ on $w$.
As $p_{\ell}$ is accepting by definition, it remains to show that
$\rho(r_{1}\dots r_{\ell})\in C_{D}$. By the choice of $\ell$, all counters
not in $D$ have reached their final values. As $C_{D}$ contains all vectors of
$C$ where all $\infty$-entries are replaced by arbitrary values, the claim
follows, hence $w\in L(\mathcal{A}^{D}_{p_{\ell}})$.

Now we argue that $\beta\in L_{\omega}(\mathcal{B}^{D}_{p_{\ell}})$. For every
$k>\ell$ define $r^{\prime}_{k}=(p_{k-1},\alpha_{k},p_{k})$. Observe that
$r^{\prime}=r^{\prime}_{k+1}r^{\prime}_{k+2}\dots$ is a run of
$\mathcal{B}^{D}_{p_{\ell}}$ on $\beta$ (all $r^{\prime}_{k+1}$ exist in
$\mathcal{B}^{D}_{p_{\ell}}$, as the counters not in $D$ of all transitions
$r_{k}$ have zero-values by the definition of $\ell$). It remains to show that
$r^{\prime}$ is accepting, i. e., that for every counter in $D$ at least one
transition with a non-zero value is used infinitely often, and an accepting
state is visited infinitely often. This is the case, as these counter values
are $\infty$ in $\rho(r)$ and by the acceptance condition of limit PA, hence
$\beta\in L_{\omega}(\mathcal{B}^{D}_{p_{\ell}})$.

We conclude $\alpha\in\bigcup_{D\subseteq\\{1,\dots,d\\},f\in
F}L(\mathcal{A}^{D}_{f})\cdot L_{\omega}(\mathcal{B}^{D}_{f})$. $\lrcorner$

$\Leftarrow$ To show $\bigcup_{D\subseteq\\{1,\dots,d\\},f\in
F}L(\mathcal{A}^{D}_{f})\cdot L_{\omega}(\mathcal{B}^{D}_{f})\subseteq
L_{\omega}(\mathcal{A})$, let $w\in L(\mathcal{A}^{D}_{f})$ and $\beta\in
L_{\omega}(\mathcal{B}^{D}_{f})$ for some $D\subseteq\\{1,\dots,d\\}$ and
$f\in F$. We show that $w\beta\in L_{\omega}(\mathcal{A})$.

Let $s$ be an accepting run of $\mathcal{A}^{D}_{f}$ on $w$, which ends in the
accepting state $f$ by definition. Let $\rho(s)=(v_{1},\dots,v_{d})$. By
definition of $C_{D}$, there is a vector $\mathbf{u}=(u_{1},\dots,u_{d})$ in
$C$ where $u_{i}=\infty$ if $i\in D$, and $u_{i}=v_{i}$ if $i\notin D$.
Furthermore, let $r=r_{1}r_{2}r_{3}\dots$, where
$r_{i}=(p_{i-1},\alpha_{i},p_{i})$, be an accepting run of
$\mathcal{B}^{D}_{f}$ on $\beta$, which starts in the accepting state $f$ by
definition. By definition of $\mathcal{T}^{d}$, for every counter $i\in D$ at
least one transition where the $i$-th counter of the corresponding transition
in $\Delta$ is non-zero is used infinitely often. Hence, let
$r^{\prime}=r^{\prime}_{1}r^{\prime}_{2}r^{\prime}_{3}\dots$ where
$r^{\prime}_{i}=(p_{i-1},\alpha_{i},\mathbf{v}_{i},p_{i})$ for a suitable
vector $\mathbf{v}_{i}$. Furthermore, the labels of transitions of counters
not in $D$ have a value of zero, hence $\rho(r^{\prime})=(x_{1},\dots,x_{d})$,
where $x_{i}=\infty$ if $i\in D$, and $x_{i}=0$ if $i\notin D$. A technical
remark: it might be the case that there are more than one transitions in
$\Delta$ that collapse to the same transition in $\Delta^{D}$, say
$\delta_{1}=(p,a,\mathbf{u},q)$ and $\delta_{2}=(p,a,\mathbf{v},q)$ appear in
$\Delta$ and collapse to $(p,a,q)$ in $\Delta^{D}$. If both transitions,
$\delta_{1}$ and $\delta_{2}$, are seen infinitely often, we need to take care
that we also see both infinitely often when translating the run $r$ back. This
is possible using a round-robin procedure.

Now observe that $sr^{\prime}$ is a run of $\mathcal{A}$ on $w\beta$ (recall
that $s$ ends in $f$, and $r^{\prime}$ starts in $f$). Furthermore, we have
$\rho(sr^{\prime})=\rho(s)+\rho(r^{\prime})=(v_{1}+x_{1},\dots,v_{d}+x_{d})$,
where $v_{i}+x_{i}=\infty$ if $i\in D$, and $v_{i}+x_{i}=v_{i}$ if $i\notin D$
by the observations above. Hence $\rho(sr^{\prime})\in C$. Finally,
$\mathcal{T}^{D}$ enforces that at least one accepting state in
$\mathcal{B}^{D}_{f}$ is seen infinitely often, hence $w\beta\in
L_{\omega}(\mathcal{A})$.

Observe that the construction in 4.14 yields a limit PA whose semi-linear set
$C$ contains no vector with an $\infty$-entry. Hence, by this observation and
the construction in the previous lemma we obtain the following corollary.

######  Corollary 4.21.

For every limit PA there is an equivalent limit PA whose semi-linear set does
not contain any $\infty$-entries.

Finally we show the implication $(3)\Rightarrow(1)$.

######  Lemma 4.22.

If $L$ is reachability-regular, then
$L\in\mathcal{L}_{\mathsf{PA,Reg}}^{\omega}$.

######  Proof 4.23.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ be a reachability-regular PA.
The intuition is as follows. a reachability-regular PA just needs to verify
the counters a single time. Hence, we can recognize the prefixes of infinite
words $\alpha\in B_{\omega}(\mathcal{A})$ that generate the accepting hit with
a PA. Further checking that an accepting state is seen infinitely often can be
done with a Büchi automaton.

Fix $f\in F$ and let $\mathcal{A}_{f}=(Q,\Sigma,q_{0},\Delta,\\{f\\},C)$ be
the PA that is, syntactically equal to $\mathcal{A}$ with the only difference
that $f$ is the only accepting state. Similarly, let
$\mathcal{B}_{f}=(Q,\Sigma,f,\\{(p,a,q)\mid(p,a,\mathbf{v},q)\in\Delta\\},F)$
be the Büchi automaton obtained from $\mathcal{A}$ by setting $f$ as the
initial state and the forgetting the vector labels.

We claim that $RR_{\omega}(\mathcal{A})=\bigcup_{f\in
F}L(\mathcal{A}_{f})\cdot L_{\omega}(\mathcal{B}_{f})$.

$\Rightarrow$ To show $RR_{\omega}(\mathcal{A})\subseteq\bigcup_{f\in
F}L(\mathcal{A}_{f})\cdot L_{\omega}(\mathcal{B}_{f})$, let $\alpha\in
B_{\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})$. Let $k$ be arbitrary such
that there is an accepting hit in $r_{k}$ (such a $k$ exists by definition)
and consider the prefix $\alpha[1,k]$. Obviously $r_{1}\dots r_{k}$ is an
accepting run of $\mathcal{A}_{p_{k}}$ on $\alpha[1,k]$. Furthermore, there
are infinitely many $j$ such that $p_{j}\in F$ by definition. In particular,
there are also infinitely many $j\geq k$ with this property. Let
$r^{\prime}_{i}=(p_{i-1},\alpha_{i},p_{i})$ for all $i>k$. Then
$r^{\prime}_{k+1}r^{\prime}_{k+2}\dots$ is an accepting run of
$\mathcal{B}_{p_{k}}$ on $\alpha_{k+1}\alpha_{k+2}\dots$ (recall that $p_{k}$
is the initial state of $\mathcal{B}_{p_{k}}$). Hence we have $\alpha[1,k]\in
L(\mathcal{A}_{p_{k}})$ and $\alpha_{k+1}\alpha_{k+2}\dots\in
L_{\omega}(\mathcal{B}_{p_{k}})$.

$\Leftarrow$ To show $\bigcup_{f\in F}L(\mathcal{A}_{f})\cdot
L_{\omega}(\mathcal{B}_{f})\subseteq RR_{\omega}(\mathcal{A})$, let $w\in
L(\mathcal{A}_{f})$ and $\beta\in L_{\omega}(\mathcal{B}_{f})$ for some $f\in
F$. We show $w\beta\in B_{\omega}(\mathcal{A})$. Let $s=s_{1}\dots s_{n}$ be
an accepting run of $\mathcal{A}_{f}$ on $w$, which ends in the accepting
state $f$ with $\rho(s)\in C$ by definition. Furthermore, let
$r=r_{1}r_{2}r_{3}\dots$ be an accepting run of $\mathcal{B}^{D}_{f}$ on
$\beta$ which starts in the accepting state $f$ by definition. It is now
easily verified that $sr^{\prime}$ with
$r^{\prime}=r^{\prime}_{1}r^{\prime}_{2}r^{\prime}_{3}\dots$ where
$r^{\prime}_{i}=(p_{i-1},\alpha_{i},\mathbf{v}_{i},p_{i})$ (for an arbitrary
$\mathbf{v}_{i}$ such that $r^{\prime}_{i}\in\Delta)$ is an accepting run of
$\mathcal{A}$ on $w\beta$, as there is an accepting hit in $s_{n}$, and the
(infinitely many) visits of an accepting state in $r$ translate one-to-one,
hence $w\beta\in B_{\omega}(\mathcal{A})$.

As shown in 4.9, the class of Büchi PA-recognizable $\omega$-languages is
equivalent to the class of $\omega$-languages of the form
$\bigcup_{i}U_{i}V_{i}^{\omega}$ where $U_{i}$ and $V_{i}$ are Parikh-
recognizable, but the PA for $V_{i}$ is restricted in such a way that the
initial state is the only accepting state and the set is linear without base
vector. Observe that for every regular language $L$ there is a Büchi automaton
$\mathcal{A}$ where the initial state is the only accepting state with
$L_{\omega}(\mathcal{A})=L^{\omega}$ (see e.g. [29, Lemma 1.2]). Hence,
$\mathcal{L}_{\mathsf{PA,Reg}}^{\omega}$ is a subset of the class of Büchi PA-
recognizable $\omega$-languages. This inclusion is also strict, as witnessed
by the Büchi PA in 3.1 which has the mentioned property.

######  Corollary 4.24.

The class $\mathcal{L}_{\mathsf{PA,Reg}}^{\omega}$ is a strict subclass of the
class of Büchi PA-recognizable $\omega$-languages.

We finish this subsection by observing that (complete) reachability PA capture
a subclass of $\mathcal{L}_{\mathsf{PA,Reg}}^{\omega}$ where, due to
completeness, all $V_{i}=\Sigma$. The following are equivalent for all
$\omega$-languages $L\subseteq\Sigma^{\omega}$.

  1. 1.

$L$ is of the form $\bigcup_{i}U_{i}\Sigma^{\omega}$ where
$U_{i}\subseteq\Sigma^{*}$ is Parikh-recognizable.

  2. 2.

$L$ is reachability PA-recognizable.

###  4.3 Characterization of $\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$ and
$\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$

In this section we give a characterization of
$\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$ and a characterization of
$\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$. As mentioned in the beginning of
this section, reset PA are too strong to capture this class. However,
restrictions of strong reset PA are a good candidate to capture
$\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$ as well as
$\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$. In fact we show that it is
sufficient to restrict the appearances of accepting states to capture
$\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$, as specified by the first theorem of
this subsection. Further restricting the vectors yields a model capturing
$\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$, as specified in the second theorem
of this subsection. Recall that the condensation of $\mathcal{A}$ is the DAG
of strong components of the underlying graph of $\mathcal{A}$.

######  Theorem 4.25.

The following are equivalent for all $\omega$-languages
$L\subseteq\Sigma^{\omega}$.

  1. 1.

$L$ is of the form $\bigcup_{i}U_{i}V_{i}^{\omega}$, where
$U_{i},V_{i}\subseteq\Sigma^{*}$ are Parikh-recognizable.

  2. 2.

$L$ is recognized by a strong reset PA $\mathcal{A}$ with the property that
accepting states appear only in the leaves of the condensation of
$\mathcal{A}$, and there is at most one accepting state per leaf.

######  Proof 4.26.

$(1)\Rightarrow(2)$. Let
$\mathcal{A}_{i}=(Q_{i},\Sigma,q_{i},\Delta_{i},F_{i})$ for $i\in\\{1,2\\}$ be
PA and let $L=L(\mathcal{A}_{1})\cdot L(\mathcal{A}_{2})^{\omega}$. By 4.4 we
may assume that $\mathcal{A}_{2}$ is normalized (recall that by 4.6 this
implies $SR_{\omega}(\mathcal{A}_{2})=L(\mathcal{A}_{2})^{\omega}$) and hence
write $L=L(\mathcal{A}_{1})\cdot SR_{\omega}(\mathcal{A}_{2})$. As pointed out
in the proof of 4.2, we can construct a reset PA $\mathcal{A}$ that recognizes
$L$ such that only the accepting states of $\mathcal{A}_{2}$ remain accepting
in $\mathcal{A}$. As $\mathcal{A}_{2}$ is normalized, this means that only
$q_{2}$ is accepting in $\mathcal{A}$. Hence $\mathcal{A}$ satisfies the
property of the theorem. Finally observe that the construction in 4.1
maintains this property, implying that the construction presented in 4.7
always yields a reset PA of the desired form $\lrcorner$

$(2)\Rightarrow(1)$. Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ be a strong
reset PA of dimension $d$ with the property of the theorem. Let $f\in F$ and
let $\mathcal{A}_{f}=(Q,\Sigma,q_{0},\Delta_{f},\\{f\\},C\cdot\\{1\\})$ with
$\Delta_{f}=\\{p,a,\mathbf{v}\cdot 0,q)\mid(p,a,\mathbf{v},q)\in\Delta,q\neq
f\\}\cup\\{(p,a,\mathbf{v}\cdot 1,f)\mid(p,a,\mathbf{v},f)\in\Delta\\}$ be the
PA of dimension $d+1$ obtained from $\mathcal{A}$ by setting $f$ as the only
accepting state with an additional counter that is, 0 at every transition
except the incoming transitions of $f$, where the counter is set to 1.
Additionally all vectors in $C$ are concatenated with $1$. Similarly, let
$\mathcal{A}_{f,f}=(Q,\Sigma,f,\Delta_{f},\\{f\\},C\cdot\\{1\\})$ be the PA of
dimension $d+1$ obtained from $\mathcal{A}$ by setting $f$ as the initial
state and only accepting state, where $\Delta_{f}$ is defined as for
$\mathcal{A}_{f}$. We claim $SR_{\omega}(\mathcal{A})=\bigcup_{f\in
F}L(\mathcal{A}_{f})\cdot L(\mathcal{A}_{f,f})^{\omega}$.

$\Rightarrow$ To show $SR_{\omega}(\mathcal{A})\subseteq\bigcup_{f\in
F}L(\mathcal{A}_{f})\cdot L(\mathcal{A}_{f,f})^{\omega}$, let $\alpha\in
S_{\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})$. Let $k_{1}<k_{2}<\dots$ be
the positions of accepting states in $r$, i. e., $p_{k_{i}}\in F$ for all
$i\geq 1$. First observe that the property in the theorem implies
$p_{k_{i}}=p_{k_{j}}$ for all $i,j\geq 1$, i. e., no two distinct accepting
states appear in $r$, since accepting states appear only in different leaves
of the condensation of $\mathcal{A}$.

For $j\geq 1$ define $r^{\prime}_{j}=(p_{j-1},\alpha_{j},\mathbf{v}_{j}\cdot
0,p_{j})$ if $j\neq k_{i}$ for all $i\geq 1$, and
$r^{\prime}_{j}=(p_{j-1},\alpha_{j},\mathbf{v}_{j}\cdot 1,p_{j})$ if $j=k_{i}$
for some $i\geq 1$, i. e., we replace every transition $r_{j}$ by the
corresponding transition in $\Delta_{f}$.

Now consider the partial run $r_{1}\dots r_{k_{1}}$ and observe that
$p_{i}\neq p_{k_{1}}$ for all $i<k_{1}$, and $\rho(r_{1}\dots r_{k_{1}})\in C$
by the definition of strong reset PA. Hence $r^{\prime}=r^{\prime}_{1}\dots
r^{\prime}_{k_{1}}$ is an accepting run of $\mathcal{A}_{p_{k_{1}}}$ on
$\alpha[1,k_{1}]$, as only a single accepting state appears in $r^{\prime}$,
the newly introduced counter has a value of $1$ when entering $p_{k_{1}}$, i.
e., $\rho(r^{\prime})\in C\cdot\\{1\\}$, hence $\alpha[1,k_{1}]\in
L(\mathcal{A}_{p_{k_{1}}})$.

Finally, we show that $\alpha[k_{i}+1,k_{i+1}]\in
L(\mathcal{A}_{p_{k_{1}},p_{k_{1}}})$. Observe that $r^{\prime}_{k_{i}+1}\dots
r^{\prime}_{k_{i+1}}$ is an accepting run of
$\mathcal{A}_{p_{k_{1}},p_{k_{1}}}$ on $\alpha[k_{i}+1,k_{i+1}]$: we have
$\rho(r_{k_{i}+1}\dots r_{k_{i+1}})=\mathbf{v}\in C$ by definition. Again, as
only a single accepting state appears in $r^{\prime}_{k_{i}+1}\dots
r^{\prime}_{k_{i+1}}$, we have $\rho(r^{\prime}_{k_{i}+1}\dots
r^{\prime}_{k_{i+1}})=\mathbf{v}\cdot 1\in C\cdot\\{1\\}$, and hence
$\alpha[k_{i}+1,k_{i+1}]\in L(\mathcal{A}_{p_{k_{1}},p_{k_{1}}})$. We conclude
$\alpha\in L(\mathcal{A}_{p_{k_{1}}})\cdot
L(\mathcal{A}_{p_{k_{1}},p_{k_{1}}})^{\omega}$.

$\Leftarrow$ To show $\bigcup_{f\in F}L(\mathcal{A}_{f})\cdot
L(\mathcal{A}_{f,f})^{\omega}\subseteq SR_{\omega}(\mathcal{A})$, let $u\in
L(\mathcal{A}_{f})$, and $v_{1},v_{2},\dots\in L(\mathcal{A}_{f,f})$ for some
$f\in F$. We show that $uv_{1}v_{2}\dots\in SR_{\omega}(\mathcal{A})$.

First let $u=u_{1}\dots u_{n}$ and $r^{\prime}=r^{\prime}_{1}\dots
r^{\prime}_{n}$ with $r^{\prime}_{i}=(p_{i-1},u_{i},\mathbf{v}_{i}\cdot
c_{i},p_{i})$, where $c_{i}\in\\{0,1\\}$, be an accepting run of
$\mathcal{A}_{f}$ on $u$. Observe that $\rho(r^{\prime})\in C\cdot\\{1\\}$,
hence $\sum_{i\leq n}c_{i}=1$, i. e., $p_{n}$ is the only occurrence of an
accepting state in $r^{\prime}$ (if there was another, say $p_{j}$, then
$c_{j}=1$ by the choice of $\Delta_{f}$, hence $\sum_{i\leq n}c_{i}>1$, a
contradiction). For all $1\leq i\leq n$ let
$r_{i}=(p_{i-1},u_{i},\mathbf{v}_{i},p_{i})$. Then $r_{1}\dots r_{n}$ is a
partial run of $\mathcal{A}$ on $w$ with $\rho(r_{1}\dots r_{n})\in C$ and
$p_{n}=f$.

Similarly, no run of $\mathcal{A}_{f,f}$ on any $v_{i}$ visits an accepting
state before reading the last symbol, hence we continue the run from $r_{n}$
on $v_{1},v_{2},\dots$ using the same argument. Hence $uv_{1}v_{2}\dots\in
SR_{\omega}(\mathcal{A})$, concluding the proof.

As a side product of the proof of Theorem 4.25 we get the following corollary,
which is in general not true for arbitrary reset PA.

######  Corollary 4.27.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ be a strong reset PA with the
property that accepting states appear only in the leaves of the condensation
of $\mathcal{A}$, and there is at most one accepting state per leaf. Then we
have $SR_{\omega}(\mathcal{A})=\bigcup_{f\in
F}S_{\omega}(Q,\Sigma,q_{0},\Delta,\\{f\\},C)$.

By even further restricting the power of strong reset PA, we get the following
characterization of $\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$.

######  Theorem 4.28.

The following are equivalent for all $\omega$-languages
$L\subseteq\Sigma^{\omega}$.

  1. 1.

$L$ is of the form $\bigcup_{i}U_{i}V_{i}^{\omega}$, where
$U_{i}\subseteq\Sigma^{*}$ is regular and $V_{i}\subseteq\Sigma^{*}$ is
Parikh-recognizable.

  2. 2.

$L$ is recognized by a strong reset PA $\mathcal{A}$ with the following
properties.

    1. (a)

At most one state $q$ per leaf of the condensation of $\mathcal{A}$ may have
incoming transitions from outside the leaf, this state $q$ is the only
accepting state in the leaf, and there are no accepting states in non-leaves.

    2. (b)

only transitions connecting states in a leaf may be labeled with a non-zero
vector.

Observe that property (a) is a stronger property than the one of Theorem 4.25,
hence, strong reset PA with this restriction are at most as powerful as those
that characterize $\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$. However, as a side
product of the proof we get that property (a) is equivalent to the property of
Theorem 4.25. Hence, property (b) is mandatory to sufficiently weaken strong
reset PA such that they capture $\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$. In
fact, using the notion of normalization, we can re-use most of the ideas in
the proof of Theorem 4.25.

######  Proof 4.29 (Proof of Theorem 4.28).

$(1)\Rightarrow(2)$. We can trivially convert an NFA into an equivalent PA by
labeling every transition with $0$ and choosing $C=\\{0\\}$. Let $\mathcal{A}$
be an arbitrary PA and assume that it is normalized; in particular implying
that it only a single SCC. Again, we have
$L(\mathcal{A})^{\omega}=S_{\omega}(\mathcal{A})$ and the constructions for
concatenation and union do not destroy the properties, hence we obtain a
strong reset PA of the desired form. $\lrcorner$

$(2)\Rightarrow(1)$ Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ be a strong
reset PA of dimension $d$ with properties (a) and (b). Fix $f\in F$ and let
$\mathcal{B}_{f}=(Q_{f},\Sigma,q_{0},\\{(p,a,q)\mid(p,a,\mathbf{v},q)\in\Delta,p,q\in
Q_{f}\\},\\{f\\})$ with $Q_{f}=\\{q\in Q\mid q\text{ appears in a non-leaf SCC
of }C(\mathcal{A})\\}\cup\\{f\\}$ be the NFA obtained from $\mathcal{A}$ by
removing all leaf states except $f$, and removing all labels from the
transitions. Recycling the automaton from Theorem 4.25, let
$\mathcal{A}_{f,f}=(Q,\Sigma,f,\Delta_{f},\\{f\\},C\cdot\\{1\\})$ with
$\Delta_{f}=\\{(p,a,\mathbf{v}\cdot 0,q)\mid(p,a,\mathbf{v},q)\in\Delta,q\neq
f\\}\cup\\{(p,a,\mathbf{v}\cdot 1,f)\mid(p,a,\mathbf{v},f)\in\Delta\\}$. We
claim $SR_{\omega}(\mathcal{A})=\bigcup_{f\in F}L(\mathcal{B}_{f})\cdot
L(\mathcal{A}_{f,f})^{\omega}$.

$\Rightarrow$ To show $SR_{\omega}(\mathcal{A})\subseteq\bigcup_{f\in
F}L(\mathcal{B}_{f})\cdot L(\mathcal{A}_{f,f})^{\omega}$, let $\alpha\in
SR_{\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 let $k_{1}<k_{2}<\dots$
be the positions of the accepting states in $r$, and consider the partial run
$r_{1}\dots r_{k_{1}}$ (if $k_{1}=0$, i. e., the initial state is already
accepting, then $r_{1}\dots r_{k_{1}}$ is empty).

By property (a) we have that $p_{k_{1}}$ is the first state visited in $r$
that is, located in a leaf of $C(\mathcal{A})$. Hence $r^{\prime}_{1}\dots
r^{\prime}_{k_{1}}$, where $r^{\prime}_{i}=(p_{i-1},\alpha_{i},p_{i})$, is an
accepting run of $\mathcal{B}_{p_{k_{1}}}$ on $\alpha[1,k_{1}]$ (in the case
$k_{1}=0$ we define $\alpha[1,k_{1}]=\varepsilon$).

By the same argument as in the proof of Theorem 4.25 we have
$p_{k_{i}}=p_{k_{j}}$ for all $i,j\geq 1$, hence $\alpha[k_{i}+1,k_{i+1}]\in
L(\mathcal{A}_{p_{k_{1}},p_{k_{1}}})$, and hence $\alpha\in
L(\mathcal{B}_{p_{k}})\cdot L(\mathcal{A}_{p_{k_{1}},p_{k_{1}}})^{\omega}$.

$\Leftarrow$ To show $\bigcup_{f\in F}L(\mathcal{A}_{f})\cdot
L(\mathcal{A}_{f,f})^{\omega}\subseteq SR_{\omega}(\mathcal{A})$, let $u\in
L(\mathcal{B}_{f})$, and $v_{1},v_{2},\dots\in L(\mathcal{A}_{f,f})$ for some
$f\in F$. We show that $uv_{1}v_{2}\dots\in S_{\omega}(\mathcal{A})$.

First observe that properties (a) and (b) enforce that $\mathbf{0}\in C$, as
the accepting state of a leaf of $C(\mathcal{A})$ is visited before a
transition labeled with a non-zero can be used. Let $u=u_{1}\dots u_{n}$ and
$s_{1}\dots s_{n}$ with $s_{i}=(p_{i_{1}},u_{i},p_{i})$ be an accepting run of
$\mathcal{B}_{f}$ on $u$. Define
$s^{\prime}_{i}=(p_{i_{1}},u_{i},\mathbf{0},p_{i})$ and observe that
$s^{\prime}_{1}\dots s^{\prime}_{n}$ is a partial run of $\mathcal{A}$ with
$\rho(s^{\prime}_{1}\dots s^{\prime}_{n})\in C$ and $p_{n}=f$ by the
observation above.

Again we can very similarly continue the run on $v_{1},v_{2},\dots$ using the
same argument. Hence $uv_{1}v_{2}\dots\in SR_{\omega}(\mathcal{A})$,
concluding the proof.

##  5 Blind counter machines and $\varepsilon$-elimination

As mentioned in the introduction, blind counter machines as an extension of
automata with counting mechanisms were already introduced and studied in the
70s [18]. Over finite words they are equivalent to Parikh automata [25]. Blind
counter machines over infinite words were first considered by Fernau and
Stiebe [14]. In this section we first recall the definition of blind counter
machines as introduced by Fernau and Stiebe [14]. The definition of these
automata admits $\varepsilon$-transitions. It is easily observed that Büchi PA
with $\varepsilon$-transitions are equivalent to blind counter machines.
Therefore, we extend all Parikh automata models studied in this paper with
$\varepsilon$-transitions and consider the natural question whether they admit
$\varepsilon$-elimination (over infinite words). We show that almost all
models allow $\varepsilon$-elimination, the exception being safety and co-
Büchi PA. For the latter two models we observe that $\varepsilon$-transitions
allow to encode $\omega$-regular conditions, meaning that such transitions
give the models enough power such that they can recognize all $\omega$-regular
languages.

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 a finite
set of _integer labeled transitions_. In particular, the transitions of
$\Delta$ are labeled with possibly negative integer vectors. Observe that
$\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\\}$.

Parikh automata naturally generalize to Parikh automata with
$\varepsilon$-transitions. An $\varepsilon$-PA 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
a finite set of _labeled $\varepsilon$-transitions_, and all other entries are
defined as for PA. 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 acceptance conditions of the models translate to runs
of $\varepsilon$-PA in the obvious way. We use terms like $\varepsilon$-safety
PA, $\varepsilon$-reachability PA, etc, to denote an $\varepsilon$-PA with the
respective acceptance condition.

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

###  5.1 Equivalence of blind counter machines with Büchi PA

We start with the following simple observation.

######  Lemma 5.1.

CM and $\varepsilon$-Büchi PA are equivalent.

######  Proof 5.2.

We first show that for every CM $\mathcal{M}$ there is an equivalent
$\varepsilon$-Büchi PA $\mathcal{A}$. 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$-Büchi PA
$\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, let $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})$.

For the reverse direction we show that for every Büchi PA $\mathcal{A}$ there
is an equivalent CM $\mathcal{M}$. Let
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ be a Büchi PA of dimension $d$ where
$C=C_{1}\cup\dots\cup C_{\ell}$ for linear $C_{i}$. Note that we have
$B_{\omega}(\mathcal{A})=\bigcup_{i\leq\ell}B_{\omega}(Q,\Sigma,q_{0},\Delta,F,C_{i})$
by the infinite pigeonhole principle. Hence, we can assume that $C$ is linear
as CM are closed under union [14]. We construct a blind $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
$B_{\omega}(\mathcal{A})=L_{\omega}(\mathcal{M})$.

###  5.2 $\varepsilon$-elimination for Parikh automata

We now show that almost all PA models admit $\varepsilon$-elimination. We
first consider Büchi PA, where $\varepsilon$-elimination implies the
equivalence of blind counter machines and Büchi PA by 5.1. We provided a
direct but quite complicated proof in the manuscript [19]. We thank Georg
Zetzsche for outlining a much simpler proof, which we present here.

######  Theorem 5.3.

$\varepsilon$-Büchi PA admit $\varepsilon$-elimination.

######  Proof 5.4.

Observe that the construction in 5.1 translates $\varepsilon$-free CM into
$\varepsilon$-free Büchi PA. We can hence translate a given Büchi PA into a CM
and eliminate $\varepsilon$-transitions and then translate back into a Büchi
PA. Therefore, all we need to show is that CM admit $\varepsilon$-elimination.

To show that CM admit $\varepsilon$-elimination we observe that

$\text{$L$ is recognized by a CM}\quad\Longleftrightarrow\quad
L=\bigcup_{i}U_{i}V_{i}^{\omega},$

where $U_{i}$ is a language of finite words that is recognized by a CM and
$V_{i}$ is a language of finite words that is recognized by a CM where
$F=\\{q_{0}\\}$. The proof of this observation is very similar to the proof of
4.9 and we leave the details to the reader.

As shown in [18, 26], CM on finite words admit $\varepsilon$-elimination.
Furthermore, from the proof technique established in [30] is is immediate that
the condition $F=\\{q_{0}\\}$ can be preserved. We obtain $\varepsilon$-free
CM $\mathcal{A}_{i}^{\prime}$ and $\mathcal{B}_{i}^{\prime}$ for the languages
$U_{i}$ and $V_{i}$. Using the construction of [25], we can translate
$\mathcal{A}_{i}^{\prime}$ and $\mathcal{B}_{i}^{\prime}$ into PA
$\mathcal{A}_{i}$ and $\mathcal{B}_{i}$, where the $\mathcal{B}_{i}$ satisfy
$F_{i}=\\{q_{0}\\}$ and the sets $C_{i}$ are linear and have no base vector
$b_{0}$ (Theorem 32 of [25]). Now the statement follows by 4.9.

We continue with $\varepsilon$-reachability, $\varepsilon$-reachability-
regular and $\varepsilon$-limit PA, as we show $\varepsilon$-elimination using
the same technique for these models. As shown in 4.24 and Theorem 4.13, the
class of $\omega$-languages recognized by reachability PA coincides with the
class of $\omega$-languages of the form $\bigcup_{i}U_{i}\Sigma^{\omega}$ for
Parikh-recognizable $U_{i}$, and the class of reachability-regular and limit
PA-recognizable $\omega$-languages coincides with the class of
$\omega$-languages of the form $\bigcup_{i}U_{i}V_{i}^{\omega}$ for Parikh-
recognizable $U_{i}$ and regular $V_{i}$, respectively. It is well-known that
NFA and PA on finite words are closed under homomorphisms and hence admit
$\varepsilon$-elimination [25] (as a consequence of [26, Proposition II.11],
$\varepsilon$-transitions can even be eliminated without changing the semi-
linear set). The characterizations allow us to reduce
$\varepsilon$-elimination of these infinite word PA to the finite case.

######  Lemma 5.5.

$\varepsilon$-reachability, $\varepsilon$-reachability-regular, and
$\varepsilon$-limit PA admit $\varepsilon$-elimination.

######  Proof 5.6.

We show the statement for $\varepsilon$-reachability PA. The technique can
very easily be translated to the other two models. Let $\mathcal{A}$ be an
$\varepsilon$-reachability PA with
$R_{\omega}(\mathcal{A})=L\subseteq\Sigma^{\omega}$. Let $\mathcal{A}_{e}$ be
the reachability PA obtained from $\mathcal{A}$ by replacing every
$\varepsilon$-transition with an $e$-transition, where $e$ is a fresh symbol
that does not appear in $\Sigma$. Let $h$ be the homomorphism that erases the
letter $e$, i.e., $h(e)=\varepsilon$. Observe that $\mathcal{A}_{e}$
recognizes an $\omega$-language $L_{e}\subseteq(\Sigma\cup\\{e\\})^{\omega}$
with the property that $h(L_{e})=L$ (note that by definition
$\\{\varepsilon\\}^{\omega}=\varnothing$). Now, by 4.24 we can write $L_{e}$
as $\bigcup_{i}U_{i}\cdot(\Sigma\cup\\{e\\})^{\omega}$ where
$U_{i}\subseteq(\Sigma\cup\\{e\\})^{*}$ is Parikh-recognizable. As the class
of Parikh-recognizable languages is closed under homomorphisms [25], we have

$L=h(L_{e})=h\left(\bigcup_{i}U_{i}\cdot(\Sigma\cup\\{e\\})^{\omega}\right)=\bigcup_{i}h(U_{i})\cdot\Sigma^{\omega},$

and can hence find a reachability PA for $L$. The proof for reachability-
regular and limit PA works the same way, as the regular languages are also
closed under homomorphisms.

Finally we show that safety and co-Büchi PA do not admit
$\varepsilon$-elimination.

######  Lemma 5.7.

$\varepsilon$-safety PA and $\varepsilon$-co-Büchi PA do not admit
$\varepsilon$-elimination.

######  Proof 5.8.

Consider the automaton $\mathcal{A}$ in Figure 3 with $C=\\{(z,z^{\prime})\mid
z^{\prime}\geq z\\}$.

$q_{0}$$q_{1}$$\varepsilon,\begin{pmatrix}0\\\
1\end{pmatrix}$$a,\begin{pmatrix}0\\\ 0\end{pmatrix}$$b,\begin{pmatrix}1\\\
0\end{pmatrix}$$b,\begin{pmatrix}0\\\ 0\end{pmatrix}$ Figure 3: The
$\varepsilon$-PA with $C=\\{(z,z^{\prime})\mid z^{\prime}\geq z\\}$ for the
proof of 5.7.

If we interpret $\mathcal{A}$ as an $\varepsilon$-safety or $\varepsilon$-co-
Büchi PA, we have we have
$S_{\omega}(\mathcal{A})=CB_{\omega}(\mathcal{A})=\\{ab^{+}\\}^{\omega}$. This
$\omega$-language is neither safety PA nor co-Büchi PA-recognizable (one can
easily adapt the proof in [21] showing that
$\\{\alpha\in\\{a,b\\}^{\omega}\mid|\alpha|_{a}=\infty\\}$ is neither safety
PA nor co-Büchi PA-recognizable).

Observe how $\mathcal{A}$ utilizes the $\varepsilon$-transition to enforce
that $q_{0}$ is infinitely often: whenever the $b$-loop on $q_{1}$ is used,
the first counter increments. The semi-linear set states that at no point the
first counter value may be greater than the second counter value which can
only be increased using the $\varepsilon$-loop on $q_{0}$. Hence, any infinite
word accepted by $\mathcal{A}$ may contain arbitrary infixes of the form
$b^{n}$ for $n<\infty$, as the automaton can use the $\varepsilon$-loop on
$q_{0}$ at least $n$ times before, but not $b^{\omega}$.

As a consequence of the previous proof we show that $\varepsilon$-safety PA
and $\varepsilon$-co-Büchi PA recognize all $\omega$-regular languages, as the
presented trick can be used to encode $\omega$-regular conditions, that is
$\varepsilon$-transitions can be used to enforce that at least one state of a
subset of states needs to be visited infinitely often.

######  Lemma 5.9.

Every $\omega$-regular language is $\varepsilon$-safety PA and
$\varepsilon$-co-Büchi recognizable.

######  Proof 5.10.

Let $L$ be an $\omega$-regular language and let
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F)$ be a Büchi automaton recognizing $L$.
Wlog we assume that $q_{0}\in F$ (this can be achieved by creating a fresh
accepting copy of $q_{0}$). We construct an $\varepsilon$-safety (or in this
case equivalent $\varepsilon$-co-Büchi) PA
$\mathcal{A}^{\prime}=(Q,\Sigma,q_{0},\Delta^{\prime},\mathcal{E}^{\prime},Q)$
with two counters where $\Delta^{\prime}$ is defined as follows. The set
$\Delta^{\prime}$ inherits every transition of $\Delta$ where the first
counter value is increased by one. For every $q\in F$ we create an
$\varepsilon$-loop on $q$ that increments the second counter by one. The semi-
linear set $C$ enforces that the second counter value must be greater or equal
the first counter value all the time. Formally, we have
$\Delta^{\prime}=\\{(p,a,(1,0),q)\mid(p,a,q)\in\Delta\\}$ and
$\mathcal{E}^{\prime}=\\{(q,\varepsilon,(0,1),q)\mid q\in F\\}$, and
$C=\\{(z,z^{\prime})\mid z^{\prime}\geq z\\}$. Hence, every accepting run of
$\mathcal{A}^{\prime}$ must visit at least one accepting state an infinite
amount of times, as only accepting states can increase the second counter
which is necessary to use other transitions. To be precise, if $r$ is an
accepting run of $\mathcal{A}$ with accepting positions
$0=k_{0},k_{1},k_{2},\dots$, then $\mathcal{A}^{\prime}$ can mimic the run $r$
by using the inherited transitions, and additionally, using an
$\varepsilon$-loop at position $k_{i}$ at least $k_{i+1}-k_{i}$ many times.

Finally we show that strong $\varepsilon$-reset PA and weak
$\varepsilon$-reset PA admit $\varepsilon$-elimination. We show that these two
models are equivalent. Hence to show this statement we only need to argue that
strong $\varepsilon$-reset PA admit $\varepsilon$-elimination.

######  Lemma 5.11.

Every strong $\varepsilon$-reset PA $\mathcal{A}$ is equivalent to a weak
$\varepsilon$-reset PA $\mathcal{A}^{\prime}$ that has the same set of states
and uses one additional counter. If $\mathcal{A}$ is a strong reset PA, then
$\mathcal{A}^{\prime}$ is a weak reset PA.

######  Proof 5.12.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,\mathcal{E},F,C)$ be a strong
$\varepsilon$-reset PA. We construct an equivalent weak $\varepsilon$-reset PA
$\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 define $C^{\prime}=C\cdot\\{1\\}$, such that
this new counter must be set to 1 when visiting an accepting state, thus
disallowing to pass such a state without resetting. Now it is clear that
$\mathcal{A}^{\prime}$ is a weak $\varepsilon$-reset PA equivalent to
$\mathcal{A}$. Observe that if $\mathcal{A}$ has no $\varepsilon$-transitions,
then $\mathcal{A}^{\prime}$ has no $\varepsilon$-transitions.

######  Lemma 5.13.

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

######  Proof 5.14.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,\mathcal{E},F,C)$ be a weak
$\varepsilon$-reset PA. We construct an equivalent strong $\varepsilon$-reset
PA $\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. Again, it is clear that
$\mathcal{A}^{\prime}$ is equivalent to $\mathcal{A}$. Observe that if
$\mathcal{A}$ has no $\varepsilon$-transitions, then $\mathcal{A}^{\prime}$
has no $\varepsilon$-transitions.

######  Lemma 5.15.

Strong $\varepsilon$-reset PA admit $\varepsilon$-elimination.

######  Proof 5.16.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,\mathcal{E},F,C)$ be a strong
$\varepsilon$-reset PA of dimension $d$. We assume wlog that $q_{0}$ has no
incoming transitions (this can be achieved by introducing a fresh copy of
$q_{0}$). Furthermore, we assume that $F\neq\varnothing$ (otherwise
$SR_{\omega}(\mathcal{A})=\varnothing$). Let the states of $Q$ be ordered
arbitrarily, say $Q=\\{q_{0},\dots,q_{n-1}\\}$. We construct an equivalent
strong reset PA
$\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

  * •

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

  * •

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

  * •

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

  * •

all internal states are non-accepting, 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-accepting, 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
accepting 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 accepting. State $(p,S,q)$
will represent a partial run of the automaton with only
$\varepsilon$-transitions starting in $p$, visiting the accepting 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})$ be 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 incoming 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 by Klaedtke and Ruess [25]
used to eliminate $\varepsilon$-transitions in the finite setting. For every
$q\in Q\setminus F$ we define $C_{q}=\\{\rho(r)\mid r\in\mathcal{E}^{*}$ is
partial run of $\mathcal{A}$ starting and ending in $q$ that does not visit
any accepting state$\\}$. As a consequence of Parikh’s theorem [28] and [25,
Lemma 5], the sets $C_{q}$ are semi-linear. 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 $SR_{\omega}(\mathcal{A})\subseteq
SR_{\omega}(\mathcal{A}^{\prime})$, let $\alpha\in SR_{\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.

  * •

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

  * •

At least one state in $r_{j+2}\dots r_{k}$ is accepting, 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.

  * •

Case (NN). That is, there is no accepting 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}$.

  * •

Case (NF). That is, there is no accepting state in $r_{i}\dots r_{j}$ but at
least one accepting 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
accepting 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.

  * •

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}$.

  * •

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 $SR_{\omega}(\mathcal{A}^{\prime})\subseteq
SR_{\omega}(\mathcal{A})$ we unravel the shortcuts and $(p,S,q)$-states
introduced in the construction. Let $\alpha\in
SR_{\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.

  * •

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 accepting 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}$.

  * •

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 accepting 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).

  * •

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.

  * •

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$

Observe that the size of $\mathcal{A}^{\prime}$ is in
$\mathcal{O}(|\mathcal{A}|^{2}|\mathcal{A}|!)$. This finishes the proof of the
lemma.

##  6 Decision problems

As shown by Guha et al. [21], the results for common decision problems
translate from the finite case to reachability PA and Büchi PA, that is, non-
emptiness is $\NP$-complete, and universality (and hence inclusion and
equivalence) are undecidable. We show that these results translate to reset PA
(which are more expressive), even if we allow $\varepsilon$-transitions (which
does not increase their expressiveness but our $\varepsilon$-elimination
procedure constructs an equivalent reset PA of super-polynomial size). Hence,
($\varepsilon$-)reset PA are a powerful model that can still be used for
algorithmic applications, such as the model checking problem.

The main reason for this is that the $\omega$-languages recognized by reset PA
are ultimately periodic, meaning that whenever a reset PA accepts at least one
infinite word, then it also accepts an infinite word of the form
$uv^{\omega}$.

######  Lemma 6.1.

Let $\mathcal{A}$ be an $\varepsilon$-reset PA. If
$SR_{\omega}(\mathcal{A})\neq\varnothing$, then $\mathcal{A}$ accepts an
infinite word of the form $uv^{\omega}$.

######  Proof 6.2.

Assume $SR_{\omega}(\mathcal{A})\neq\varnothing$. Then there exists an
infinite word $\alpha\in SR_{\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 $k_{1}<k_{2}<\dots$ be
the positions of all accepting states in $r$. Let $k_{i}<k_{j}$ be two such
positions such that $p_{k_{i}}=p_{k_{j}}$ and $\mathcal{A}$ has read at least
one symbol from $\alpha$ after leaving $p_{k_{i}}$ and entering $p_{k_{j}}$.
Let $u=\gamma_{1}\dots\gamma_{k_{i}}$ be the prefix of $\alpha$ read upon
visiting $p_{k_{i}}$ and $v=\gamma_{k_{i}+1}\dots\gamma_{k_{j}}$ the infix
read between $p_{k_{i}}$ and $p_{k_{j}}$. Note that $v\neq\varepsilon$ by the
choice of $k_{j}$. Then $\mathcal{A}$ also accepts $uv^{\omega}$, as
$r_{1}\dots r_{k_{i}}(r_{k_{i}+1}\dots r_{k_{j}})^{\omega}$ is an accepting
run of $\mathcal{A}$ on $uv^{\omega}$ by definition.

As a consequence, we can reduce non-emptiness for reset PA to the finite word
case, as clarified in the following lemma.

######  Lemma 6.3.

Non-emptiness for $\varepsilon$-reset PA is $\NP$-complete.

######  Proof 6.4.

The $\NP$-hardness follows from the finite word case [15], hence we focus on
the membership in $\NP$. Let $\mathcal{A}$ be a strong reset PA. By the
previous lemma, it suffices to check whether $\mathcal{A}$ accepts an infinite
word $uv^{\omega}$ with $u\in\Sigma^{*}$ and $v\in\Sigma^{+}$. If such a word
exists, we may assume that there is an accepting run $r_{u}r_{v}^{\omega}$ of
$\mathcal{A}$ on $uv$ where neither $r_{u}$ nor $r_{v}$ visit the same
accepting state twice. For any $p,q\in Q$ we define $\mathcal{A}_{p\Rightarrow
q}=(Q\cup\\{q_{0}^{\prime}\\},\Sigma,q_{0}^{\prime},\Delta^{\prime},\mathcal{E}^{\prime},\\{q\\},C)$,
where
$\Delta^{\prime}=\\{(q_{1},a,\mathbf{v},q_{2})\mid(q_{1},a,\mathbf{v},q_{2})\in\Delta,q_{1}\notin
F\\}\cup\\{(q_{0}^{\prime},a,\mathbf{v},q_{2})\mid(p,a,\mathbf{v},q_{2})\in\Delta\\}$
and, analogously,
$\mathcal{E}^{\prime}=\\{(q_{1},\varepsilon,\mathbf{v},q_{2})\mid(q_{1},\varepsilon,\mathbf{v},q_{2})\in\mathcal{E},q_{1}\notin
F\\}\cup\\{(q_{0}^{\prime},\varepsilon,\mathbf{v},q_{2})\mid(p,\varepsilon,\mathbf{v},q_{2})\in\Delta\\}$.

Now, the following $\NP$ algorithm solves non-emptiness:

  1. 1.

Guess a sequence $f_{1},\ldots,f_{k}$ of accepting states with $k\leq 2|F|$
such that $f_{i}=f_{k}$ for some $i\leq k$.

  2. 2.

Verify that $L(\mathcal{A}_{q_{0}\Rightarrow f_{1}})\neq\varnothing$ and
$L(\mathcal{A}_{f_{j}\Rightarrow f_{j+1}})\neq\varnothing$ for all $1\leq j<k$
(interpreted as PA over finite words).

  3. 3.

Verify that $L(\mathcal{A}_{f_{i}\Rightarrow f_{i+1}})\cdot\ldots\cdot
L(\mathcal{A}_{f_{k-1}\Rightarrow f_{k}})\not\subseteq\\{\varepsilon\\}$.

The second step can be done by adding a fresh symbol (say $e$) to the automata
and replacing every $\varepsilon$-transition with an $e$-transition (observe
that this does construction does not change the emptiness behavior, and is, in
contrast to the $\varepsilon$-elimination procedure in [25] computable in
polynomial time). Afterwards we use the NP-algorithm for non-emptiness for PA
[15].

The third step essentially states that not all
$L(\mathcal{A}_{f_{j}\Rightarrow f_{j+1}})$ for $j\geq i$ may only accept the
empty word, as we require $v\neq\varepsilon$. To check this property, we can
construct a PA222This is possible in polynomial time by a standard
construction very similar to the one of 4.2. recognizing
$L(\mathcal{A}_{f_{i}\Rightarrow f_{i+1}})\cdot\ldots\cdot
L(\mathcal{A}_{f_{k-1}\Rightarrow f_{k}})$, and again replace every
$\varepsilon$-transition with an $e$-transition. Finally, we build the product
automaton with the PA (NFA) that recognizes the language
$\\{w\in(\Sigma\cup\\{e\\})^{*}\mid w\text{ contains at least 1 symbol from
}\Sigma\\}$, which is possible in polynomial time [25] and test non-emptiness
for the resulting PA.

Furthermore, we study the following membership problem for automata processing
infinite words. Given an automaton $\mathcal{A}$ and finite words $u,v$, does
$\mathcal{A}$ accept $uv^{\omega}$?

Note that we can always construct a safety automaton that recognizes
$uv^{\omega}$ and no other infinite word with $|uv|$ many states. Recall that
every state of a safety automaton is accepting. We show that the intersection
of a reset PA-recognizable $\omega$-language and a safety automaton-
recognizable $\omega$-language remains reset PA-recognizable using a product
construction which is computable in polynomial time. Hence, we can reduce the
membership problem to the non-emptiness the standard way.

######  Lemma 6.5.

The class of reset PA-recognizable $\omega$-languages is closed under
intersection with safety automata-recognizable $\omega$-languages.

######  Proof 6.6.

We show a construction for strong $\varepsilon$-reset PA that is computable in
polynomial time. Let
$\mathcal{A}_{1}=(Q_{1},\Sigma,q_{1},\Delta_{1},\mathcal{E}_{1},F_{1},C_{1})$
be a strong $\varepsilon$-reset PA and
$\mathcal{A}_{2}=(Q_{2},\Sigma,q_{2},\Delta_{2},Q_{2})$ be a safety automaton.
Consider the product automaton $\mathcal{A}=(Q_{1}\times
Q_{2},\Sigma,(q_{1},q_{2}),\Delta,\mathcal{E},$ $F_{1}\times Q_{2},C_{1})$
with
$\Delta=\\{((p,q),a,\mathbf{v},(p^{\prime},q^{\prime})\mid(p,a,\mathbf{v},p^{\prime})\in\Delta_{1}\text{
and }(q,a,q^{\prime})\in\Delta_{2}\\}$ and
$\mathcal{E}=\\{((p,q),\varepsilon,\mathbf{v},(p^{\prime},q))\mid(p,\varepsilon,\mathbf{v},p^{\prime})\in\mathcal{E}_{1}\text{
and }q\in Q_{2}\\}$.

As every state of $\mathcal{A}_{2}$ is accepting, we need to take care that
$\mathcal{A}$ does not use a transition that is not enabled in
$\mathcal{A}_{2}$ while mimicking the behavior of $\mathcal{A}_{1}$. Hence, it
is easily verified that
$SR_{\omega}(\mathcal{A})=SR_{\omega}(\mathcal{A}_{1})\cap
L_{\omega}(\mathcal{A}_{2})$.

As the membership problem for PA (on finite words) is $\NP$-complete [15], and
the construction in the previous lemma can be computed efficiently, we obtain
the following result.

######  Corollary 6.7.

Membership for $\varepsilon$-reset PA is $\NP$-complete.

Finally, we observe that universality, inclusion and equivalence remain
undecidable for ($\varepsilon$-)reset PA, as these problems are already
undecidable for Büchi PA [21] and the constructions showing that the class of
Büchi PA-recognizable $\omega$-languages is a subclass of
$\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$, and that
$\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$ is a subclass of the class of reset
PA-recognizable $\omega$-languages are effective.

##  7 Conclusion

We conclude by giving an overview of all characterizations and inclusions
shown in this paper, as depicted in Figure 4.

rechability PAreachability-regular PA = limit PA =
$\mathcal{L}_{\mathsf{PA,Reg}}^{\omega}$Büchi PA$\omega$-regular =
$\mathcal{L}_{\mathsf{Reg,Reg}}^{\omega}$reset PA $(**)$ =
$\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$safety PA$\varepsilon$-safety
PA$\varepsilon$-co-Büchi PAco-Büchi PAreset PA $(*)$ =
$\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$strong reset PA = weak reset PA$(*)$ At
most one state $q$ per leaf of $C(\mathcal{A})$ may have incoming transitions
from outside the leaf, this $(*)$ state $q$ is the only accepting state in the
leaf, and there are no accepting states in non-leaves;$(**)$ and only
transitions connecting states in leaves may be labeled with non-zero vectors.
Figure 4: Overview of our results. Arrows mean strict inclusions. If not
explicitly shown otherwise, all models are equivalent to their
$\varepsilon$-counterparts.

Recall the $\omega$-languages motivated by the model checking problem from the
introduction, namely $\\{\alpha\in\\{a,b,c\\}^{\omega}\mid\text{ there are
infinitely many prefixes $w$ of $\alpha$ with $|w|_{a}>|w|_{b}+|w|_{c}$}\\}$,
representing unfair resource distributions of an operating system, and
$\\{\alpha\in\\{p,c\\}^{\omega}\mid\text{there is a prefix $w$ of $\alpha$
with $|w|_{c}>|w|_{p}$}\\}$, representing invalid computations in a producer-
consumer setting. Both of these $\omega$-languages are Reset PA-recognizable
(in fact, the first is Büchi PA-recognizable and the second is even
reachability PA-recognizable). As mentioned, in a common approach we are given
a system represented as a Kripke structure $K$, and a specification of
counter-examples given as an automaton, e.g. a reset PA $\mathcal{A}$. By
moving the labels of the states of $K$ to its transitions, we can see a Kripke
structure as a safety automaton $\mathcal{A}_{K}$ (see [9, Theorem 28] for
details). As every state of a safety automaton is accepting, we can easily
find a reset automaton recognizing all bad computations of $K$ (that is the
intersection of the $\omega$-languages recognized by $\mathcal{A}_{K}$ and
$\mathcal{A})$ by 6.5. As (non-)emptiness is decidable for reset PA, we can
solve the model-checking problem by computing the product automaton of
$\mathcal{A}_{K}$ and $\mathcal{A}$ and testing for emptiness, which is in
$\coNP$ by 6.3.

We recall that deterministic $\omega$-regular languages are characterized as
regular arrow-languages $\vec{L}$, where $\vec{L}=\\{\alpha\mid\alpha[1,i]\in
L\text{ for infinitely many }i\\}$ [29]. This characterization can easily be
adapted to show that deterministic Büchi PA-recognizable $\omega$-languages
are captured by arrows of deterministic Parikh-recognizable languages. In
future work we plan to study the expressiveness of the deterministic variants
of the introduced models and find similar characterizations. Observe that the
proof showing that every strong reset PA can be translated into an equivalent
weak reset PA relies on non-determinism. Hence we conjecture that the class of
$\omega$-languages recognized by deterministic weak reset PA is a strict
subclass of those recognized by deterministic strong reset PA (and that
nondeterministic reset PA are strictly more powerful than their deterministic
counterparts). In particular, it would be nice to understand the structure of
$\omega$-languages that are not reset PA-recognizable. Furthermore, one could
define a reset-counterpart on finite words and study the resulting automata.

Although the existence of a natural logic capturing the expressiveness of the
presented models of PA on infinite words is very unlikely due to their bad
closure properties [21], we hope that our characterizations in terms of
regular and Parikh-recognizable (finite word) languages (for which equivalent
logics are known) help us to gain more insights.

## References

  * [1] Christel Baier and Joost-Pieter Katoen.  Principles of Model Checking.  The MIT Press, 2008.
  * [2] Brenda S. Baker and Ronald V. Book.  Reversal-bounded multipushdown machines.  Journal of Computer and System Sciences, 8(3):315–332, 1974.
  * [3] Pascal Baumann, Flavio D’Alessandro, Moses Ganardi, Oscar Ibarra, Ian McQuillan, Lia Schütze, and Georg Zetzsche.  Unboundedness problems for machines with reversal-bounded counters.  In Foundations of Software Science and Computation Structures, pages 240–264, Cham, 2023. Springer Nature Switzerland.
  * [4] J. Richard Büchi.  Weak second-order arithmetic and finite automata.  Mathematical Logic Quarterly, 6(1-6):66–92, 1960.
  * [5] Michaël Cadilhac, Alain Finkel, and Pierre McKenzie.  On the expressiveness of Parikh automata and related models.  In Third Workshop on Non-Classical Models for Automata and Applications - NCMA 2011, volume 282 of<EMAIL_ADDRESS>pages 103–119. Austrian Computer Society, 2011.
  * [6] Michaël Cadilhac, Alain Finkel, and Pierre McKenzie.  Affine Parikh automata.  RAIRO Theor. Informatics Appl., 46(4):511–545, 2012.
  * [7] Michaël Cadilhac, Alain Finkel, and Pierre McKenzie.  Bounded Parikh automata.  Int. J. Found. Comput. Sci., 23(8):1691–1710, 2012.
  * [8] Edmund M Clarke, Orna Grumberg, and Doron A. Peled.  Model checking.  The MIT Press, London, Cambridge, 1999.
  * [9] Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem.  Handbook of Model Checking.  Springer Publishing Company, Incorporated, 1st edition, 2018.
  * [10] Luc Dartois, Emmanuel Filiot, and Jean-Marc Talbot.  Two-way Parikh automata with a visibly pushdown stack.  In Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, volume 11425 of Lecture Notes in Computer Science, pages 189–206. Springer, 2019.
  * [11] Leonard Eugene Dickson.  Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors.  American Journal of Mathematics, 35(4):413–422, 1913.
  * [12] Enzo Erlich, Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann.  History-deterministic Parikh automata.  arXiv preprint arXiv:2209.07745, 2022.
  * [13] Henning Fernau and Ralf Stiebe.  Sequential grammars and automata with valences.  Theoretical Computer Science, 276(1):377–405, 2002.
  * [14] Henning Fernau and Ralf Stiebe.  Blind counter automata on omega-words.  Fundam. Inform., 83:51–64, 2008.
  * [15] Diego Figueira and Leonid Libkin.  Path logics for querying graphs: Combining expressiveness and efficiency.  In Proceedings of the 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), LICS ’15, pages 329–340. IEEE, 2015.
  * [16] Emmanuel Filiot, Shibashis Guha, and Nicolas Mazzocchi.  Two-way Parikh automata.  In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2019, volume 150 of LIPIcs, pages 40:1–40:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.
  * [17] Dimitra Giannakopoulou and Flavio Lerda.  From states to transitions: Improving translation of LTL formulae to Büchi automata.  In Formal Techniques for (Networked and) Distributed Systems, 2002.
  * [18] Sheila A. Greibach.  Remarks on blind and partially blind one-way multicounter machines.  Theoretical Computer Science, 7(3):311–324, 1978.
  * [19] Mario Grobler, Leif Sabellek, and Sebastian Siebertz.  Parikh automata on infinite words.  arXiv preprint arXiv:2301.08969, 2023.