# Büchi-like characterizations for
Parikh-recognizable omega-languages

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

###### Abstract

Büchi’s theorem states that $\omega$-regular languages are characterized as
languages of the form $\bigcup_{i}U_{i}V_{i}^{\omega}$, where $U_{i}$ and
$V_{i}$ are regular languages. Parikh automata are automata on finite words
whose transitions are equipped with vectors of positive integers, whose sum
can be tested for membership in a given semi-linear set. We give an intuitive
automata theoretic characterization of languages of the form
$U_{i}V_{i}^{\omega}$, where $U_{i}$ and $V_{i}$ are Parikh-recognizable.
Furthermore, we show that the class of such languages, where $U_{i}$ is
Parikh-recognizable and $V_{i}$ is regular is exactly captured by a model
proposed by Klaedtke and Ruess [Automata, Languages and Programming, 2003],
which again is equivalent to (a small modification of) reachability Parikh
automata introduced by Guha et al. [FSTTCS, 2022]. We finish this study by
introducing a model that captures exactly such languages for regular $U_{i}$
and Parikh-recognizable $V_{i}$.

###### keywords:

Automata theory, Parikh automata, infinite words, Büchi’s theorem

††journal: arXiv

##  1 Introduction

In his groundbreaking work [4] from 1960 Büchi initiated the study of
$\omega$-regular languages and introduced Büchi automata. By his famous
theorem $\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. One shortcoming of Büchi automata, and also of many more powerful
models, is that they cannot count. For example, the language
$\\{a^{n}b^{n}c^{n}\mid n\in\mathbb{N}\\}^{\omega}$ is not $\omega$-regular,
and not even $\omega$-context-free. This shortcoming led to the study of
automata on infinite words with counters, see e.g. [1, 3, 9].

Parikh automata (PA) are another model of automata (on finite words) with
counters [8]. A PA with $d$ counters is a non-deterministic finite automaton
that is additionally equipped with a semi-linear set $C$. Furthermore, every
transition is equipped with a $d$-tuple of non-negative integers and every
time a transition is used, the counters are incremented by the values in the
tuple accordingly. A finite input word is accepted if the PA ends in a final
state and additionally, the resulting $d$-tuple in the counters lies in $C$.
The class of languages recognized by PA contains all regular languages, and
even some, but not all, context-sensitive languages, e.g. the language
$\\{a^{n}b^{n}c^{n}\mid n\in\mathbb{N}\\}$.

Recently, several possible extensions of Parikh automata on infinite words
were proposed and studied by Grobler et al. [6] and Guha et al. [7]. In fact,
it turns out that one of the models proposed in [6] is equivalent to
synchronous blind counter machines, which were introduced by Fernau and Stiebe
[5]. Fernau and Stiebe also considered the class of all $\omega$-languages of
the form $\bigcup_{i}U_{i}V_{i}^{\omega}$, where the $U_{i},V_{i}$ are Parikh-
recognizable languages of finite words. They called this class
$\mathcal{K}_{*}$ and proved that the class of $\omega$-languages recognized
by blind counter machines is a proper subset of $\mathcal{K}_{*}$.

In the light of Büchi’s famous theorem it is a natural question to find an
automata theoretic characterization of the class $\mathcal{K}_{*}$. In fact,
more generally, 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. In this work we provide automata theoretic
characterizations of the other three classes.

We first introduce the new model of _limit Parikh Büchi automata_ (LPBA),
which was suggested in the concluding remarks of Klaedtke and Ruess [8]. An
LPBA accepts an infinite word if an accepting state is visited infinitely
often (satisfies the Büchi condition) and the infinite sum of the counters
belongs to the semi-linear set, which for this purpose is extended with the
symbol $\infty$ if the sum of some counter diverges (satisfies the newly
introduced _limit Parikh condition_).

We also introduce a new model, which is obtained by a small modification of
reachability Parikh automata as introduced by Guha et al. [7], that we call
_reachability Parikh Büchi automata_ (RPBA). An RPBA accepts an infinite word
if an accepting state is visited infinitely often (satisfies the Büchi
condition) and satisfies the Parikh condition _once_.

Quite surprisingly, both models turn out to capture exactly the class
$\mathcal{L}_{\mathsf{PA,Reg}}^{\omega}$, and hence are equivalent.

We then study _strong reset Parikh automata_ (SPBA), which were introduced by
Grobler et al. [6]. We consider the automata as directed graphs and provide
two graph theoretic definitions of subclasses of SPBA that exactly capture the
classes $\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$ and
$\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$. These definitions are based on an
analysis of the strongly connected components of the underlying graph, where
the accepting states can be found and how they are connected to the rest of
the graph.

We believe that our results provide interesting insights into the theory of
Parikh-recognizable $\omega$-languages. It remains an interesting open
question to characterize the new classes of $\omega$-languages by logics.

##  2 Preliminaries

###  2.1 Finite and infinite words

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

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

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

###  2.3 Semi-linear sets

A _linear set_ of dimension $d$ for $d\geq 1$ is a set of the form
$\\{b_{0}+b_{1}z_{1}+\dots+b_{\ell}z_{\ell}\mid
z_{1},\dots,z_{\ell}\in\mathbb{N}\\}\subseteq\mathbb{N}^{d}$ for
$b_{0},\ldots,b_{\ell}\in\mathbb{N}^{d}$. A _semi-linear set_ is the finite
union of linear sets. For vectors
$\mathbf{u}=(u_{1},\dots,u_{c})\in\mathbb{N}^{c},\mathbf{v}=(v_{1},\dots,v_{d})\in\mathbb{N}^{d}$,
we denote by
$\mathbf{u}\cdot\mathbf{v}=(u_{1},\dots,u_{c},v_{1},\dots,v_{d})\in\mathbb{N}^{c+d}$
the _concatenation of $\mathbf{u}$ and $\mathbf{v}$_. We extend this
definition to sets of vectors. Let $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 the set of _labeled transitions_
, and $C\subseteq\mathbb{N}^{d}$ is a semi-linear set. We call $d$ the
_dimension_ of $\mathcal{A}$ and refer to the entries of a vector $\mathbf{v}$
in a transition $(p,a,\mathbf{v},q)$ as _counters_. Similar to NFA, a _run_ of
$\mathcal{A}$ on a word $w=x_{1}\dots x_{n}$ is a (possibly empty) sequence of
labeled transitions $r=r_{1}\dots r_{n}$ with
$r_{i}=(p_{i-1},x_{i},\mathbf{v}_{i},p_{i})\in\Delta$ such that $p_{0}=q_{0}$.
We define the _extended Parikh image_ of a run $r$ as $\rho(r)=\sum_{i\leq
n}\mathbf{v}_{i}$ (with the convention that the empty sum equals
$\mathbf{0}$). We say $r$ is accepting if $p_{n}\in F$ and $\rho(r)\in C$,
referring to the latter condition as the _Parikh condition_. We define the
_language recognized by $\mathcal{A}$_ as
$L(\mathcal{A})=\\{w\in\Sigma^{*}\mid\text{there is an accepting run of
$\mathcal{A}$ on $w$}\\}$. If a language $L\subseteq\Sigma^{*}$ is recognized
by some PA, then we call $L$ _Parikh-recognizable_.

###  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 relevant definitions of Parikh automata
operating on infinite words introduced by Grobler et al. [6] and Guha et al.
[7]. We then propose further definitions and compare the resulting automata.

A _Parikh-Büchi automaton_ (PBA) is a PA
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$. A run of $\mathcal{A}$ on an
infinite word $\alpha=\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$.

Let us first recall the definition of _(strong) reset PBA_ (SPBA) introduced
by Grobler et al. [6]: 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$. The $\omega$-language recognized by an
SPBA $\mathcal{A}$ is $S_{\omega}(\mathcal{A})=\\{\alpha\mid\mathcal{A}\text{
accepts }\alpha\\}$. Intuitively worded, whenever an SPBA enters an accepting
state, the Parikh condition _must_ be satisfied. Then the counters are reset.

Let us now recall the definition of _(synchronous) reachability Parikh
automata_ (RPA) introduced by Guhe et al. [7]. The run $r$ is accepting 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}$. The $\omega$-language
recognized by an RPA $\mathcal{A}$ is
$R_{\omega}(\mathcal{A})=\\{\alpha\mid\mathcal{A}\text{ accepts }\alpha\\}$.

Let us finally recall the definition of _prefix PBA_ (PPBA) introduced by
Grobler et al. [6], which are obviously equivalent to _(synchronous) Büchi
Parikh automata_ introduced by Guhe et al. [7]. The run $r$ is accepting if
there are infinitely many $i\geq 1$ such that $p_{i}\in F$ and
$\rho(r_{1}\dots r_{i})\in C$. The $\omega$-language recognized by a PPBA
$\mathcal{A}$ is $P_{\omega}(\mathcal{A})=\\{\alpha\mid\mathcal{A}\text{
accepts }\alpha\\}$. Hence, a PPBA can be seen as a stronger variant of RPA
where we require infinitely many accepting hits instead of a single one.

We remark that we stick to the notation of the original papers, that is, we
abbreviate (strong) reset Parikh-Büchi automata by SPBA and (synchronous)
reachability Parikh automata by RPA. The attentive reader may have noticed
that we do not use the term RPBA. The reason for this (in addition to sticking
to the original notation) is that, unlike Büchi automata, RPA do _not_ need to
see an accepting state infinitely often. We show that this property implies
that there are $\omega$-regular languages that are not RPA-recogniazble. This
motivates the study of RPA that additionally need to satisfy the Büchi-
condition (which we hence will call RPBA).

We begin with a simple lemma. A similar result was proved in Theorem 3 of [7],
however, RPA in [7] are assumed to be _complete_ , i.e., for every state and
every symbol there is at least one transition. The proof presented in [7] does
not go through for the more general setting of non-complete RPA.

######  Lemma 3.1.

There is an $\omega$-regular language that is not recognized by any RPA.

###### Proof.

We show that $L=\\{\alpha\in\\{a,b\\}^{\omega}\mid|\alpha|_{a}=\infty\\}$ is
not RPA-recognizable. Assume that there is an RPA $\mathcal{A}$ with
$R_{\omega}(\mathcal{A})=L$ and let $n$ be the number of states of
$\mathcal{A}$. As $\alpha=(a^{n}b^{n})^{\omega}\in L$, there is an accepting
run $r=r_{1}r_{2}r_{3}\dots$ of $\mathcal{A}$ on $\alpha$. Let $i$ be the
first position of an accepting hit in $r$. Now consider
$\beta=(a^{n}b^{n})^{i}\cdot b^{\omega}\notin L$. As $\alpha$ and $\beta$
share the same prefix of length $i$, the run $r_{1}\dots r_{i}$ is also a
partial run on $\beta[1,i]$, hence, generating an accepting hit. Now observe
that in every infix of the form $b^{n}$ a state is visited at least twice by
the pigeonhole principle. Hence, we can “infinitely pump” a $b$-block after
the accepting hit in $r_{i}$ and obtain an accepting run on $\beta$,
contradicting $R_{\omega}(\mathcal{A})=L$. ∎

######  Remark 3.1.

In fact, complete RPA are strictly weaker than general RPA, as there is no
complete RPA recognizing $\\{a\\}^{\omega}$ over $\Sigma=\\{a,b\\}$; an
$\omega$-language that is obviously RPA-recognizable.

As mentioned above, this weakness motivates the study of _reachability Parikh-
Büchi automata_ (RPBA). The run $r$ is accepting if there is an $i\geq 1$ such
that $\rho(r_{1}\dots r_{i})\in C$ and $p_{i}\in F$, and if there are
infinitely many $j$ such that $p_{j}\in F$. We define the $\omega$-language
recognized by an RPBA $\mathcal{A}$ as
$B_{\omega}(\mathcal{A})=\\{\alpha\mid\mathcal{A}\text{ accepts }\alpha\\}$.

Every $\omega$-regular language is RPBA-recognizable, as we can turn an
arbitrary Büchi automaton into an equivalent RPBA by labeling every transition
with $0$ and setting $C=\\{0\\}$.

Finally, we define a variant of PBA motivated by a proposal of Klaedke and
Ruess [8]. Here we consider semi-linear sets over
$(\mathbb{N}\cup\\{\infty\\})^{d}$ and compute the extended Parikh image of an
infinite run using transfinite induction. A _limit Parikh-Büchi automaton_
(LPBA) is a PA $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ where $C$ may use the
symbol $\infty$. The run $r$ is accepting 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 define the
$\omega$-language recognized by an LPBA $\mathcal{A}$ as
$L_{\omega}(\mathcal{A})=\\{\alpha\mid\mathcal{A}\text{ accepts }\alpha\\}$.

######  Schnexample 1.

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

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

  * 1.

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}=|w|_{b}\\}$. The
automaton is in the accepting state after reading a $b$. The first counter
counts the number of read $a$s, the second one reads the number of read $b$s.
By definition of $C$ the automaton only accepts when both counters are equal
(note that vectors containing an $\infty$-entry have no additional effect).

  * 2.

If we interpret $\mathcal{A}$ as an SPBA, then we have
$S_{\omega}(\mathcal{A})=\\{ab\\}^{\omega}$. Whenever the automaton reaches an
accepting state also the Parikh condition must be satisfied. In the example
this is only possible after reading exactly one $a$ and one $b$. After that
the counters are reset.

  * 3.

If we interpret $\mathcal{A}$ as a PPBA, then we have
$P_{\omega}(\mathcal{A})=L(\mathcal{A})^{\omega}$. The automaton accepts a
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 edges.

  * 4.

If we interpret $\mathcal{A}$ as an LPBA, 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 word
contains only some finite number $z$ of $a$s (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).

  * 5.

If we interpret $\mathcal{A}$ as an RPA, then we have
$R_{\omega}(\mathcal{A})=\\{\alpha\in\\{a,b\\}^{\omega}\mid\alpha\text{ has a
prefix in }$ $L(\mathcal{A})\\}$. The automaton has satisfied the reachability
condition after reading a prefix in $L(\mathcal{A})$. Since the automaton is
complete it cannot get stuck and accepts any continuation after that.

  * 6.

If we interpret $\mathcal{A}$ as an RPBA, then we have
$B_{\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.

######  Remark 3.2.

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

We denote the class of $\omega$-languages recognized by an SPBA (PPBA, RPA,
RPBA, LPBA) by $\mathcal{L}_{\mathsf{SPBA}}$ ($\mathcal{L}_{\mathsf{PPBA}}$,
$\mathcal{L}_{\mathsf{RPA}}$, $\mathcal{L}_{\mathsf{RPBA}}$,
$\mathcal{L}_{\mathsf{LPBA}}$). Furthermore, denote by
$\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$ the class of $\omega$-languages of the
form $\bigcup_{i}U_{i}V_{i}^{\omega}$, where the $U_{i}$ and $V_{i}$ are
Parikh-recognizable, by $\mathcal{L}_{\mathsf{PA,Reg}}^{\omega}$ such
languages where the $U_{i}$ are Parikh-recognizable and the $V_{i}$ are
regular, and by $\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$ such languages where
the $U_{i}$ are regular and the $V_{i}$ are Parikh-recognizable. As shown by
Guhe et al. we have
$\mathcal{L}_{\mathsf{RPA}}\subsetneq\mathcal{L}_{\mathsf{PPBA}}$ [7].
Likewise, Grobler et al. [6] have shown
$\mathcal{L}_{\mathsf{PPBA}}\subsetneq\mathcal{L}_{\mathsf{PA,PA}}^{\omega}\subsetneq\mathcal{L}_{\mathsf{SPBA}}$.
We conclude this section by showing
$\mathcal{L}_{\mathsf{RPA}}\subsetneq\mathcal{L}_{\mathsf{RPBA}}\subsetneq\mathcal{L}_{\mathsf{PPBA}}$.
In the next section we show that
$\mathcal{L}_{\mathsf{RPBA}}=\mathcal{L}_{\mathsf{LPBA}}=\mathcal{L}_{\mathsf{PA,Reg}}^{\omega}$.

######  Lemma 3.2.

$\mathcal{L}_{\mathsf{RPA}}\subsetneq\mathcal{L}_{\mathsf{RPBA}}$.

###### Proof.

We show $\mathcal{L}_{\mathsf{RPA}}\subseteq\mathcal{L}_{\mathsf{RPBA}}$.
Strictness follows from Lemma 3.1. The proof is very similar to the proof that
$\mathcal{L}_{\mathsf{RPA}}\subsetneq\mathcal{L}_{\mathsf{PPBA}}$ [7, Theorem
3]. Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ be an RPA. The idea is to
create two copies of $\mathcal{A}$, where the second copy is modified such
that all counters are zero and all states are accepting. Then we use non-
determinism to guess the accepting hit and transition into the second copy
where the counters are frozen and all states are accepting. Let
$\mathcal{A}^{\prime}=(Q^{\prime},\Sigma,q_{0},\Delta^{\prime},F^{\prime},C)$
where $Q^{\prime}=\\{q,q^{\prime}\mid q\in Q\\}$,
$F^{\prime}=\\{q^{\prime}\mid q\in Q\\}$ and
$\Delta^{\prime}=\Delta\cup\\{(p^{\prime},a,\mathbf{0},q^{\prime})\mid(p,a,\mathbf{v},q)\in\Delta\\}\cup\\{(p,a,\mathbf{v},q^{\prime})\mid(p,a,\mathbf{v},q)\in\Delta,q\in
F\\}$ be a RPBA. We claim that
$R_{\omega}(\mathcal{A})=B_{\omega}(\mathcal{A}^{\prime})$.

$\Rightarrow$ To show $R_{\omega}(\mathcal{A})\subseteq
B_{\omega}(\mathcal{A}^{\prime})$, let $\alpha\in R_{\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 $i\geq 1$ be an
arbitrary position such that there is an accepting hit in $r_{i}$ (which
exists by definition). Let
$r^{\prime}_{i}=(p_{i-1},\alpha_{i},\mathbf{0},p_{i}^{\prime})$ and define
$r^{\prime}_{j}=(p^{\prime}_{j-1},\alpha_{j},\mathbf{0},p^{\prime}_{j})$ for
all $j>i$. Then $r^{\prime}=r_{1}r_{2}\dots
r_{i-1}r^{\prime}_{i}r^{\prime}_{i+1}r^{\prime}_{i+2}\dots$ is a run of
$\mathcal{A}^{\prime}$ on $\alpha$. Furthermore, $r^{\prime}$ is accepting:
the accepting hit in $r_{i}$ translates one-to-one to an accepting hit in
$r^{\prime}_{i}$. Furthermore, all $p_{j}$ for $j\geq i$ are accepting by the
definition of $F^{\prime}$. Hence, $r^{\prime}$ is accepting, thus $\alpha\in
B_{\omega}(\mathcal{A}^{\prime})$.

$\Leftarrow$ To show $B_{\omega}(\mathcal{A}^{\prime})\subseteq
R_{\omega}(\mathcal{A})$, let $\alpha\in B_{\omega}(\mathcal{A}^{\prime})$
with accepting run
$r^{\prime}=r^{\prime}_{1}r^{\prime}_{2}r^{\prime}_{3}\dots$ where
$r^{\prime}_{i}=(\hat{p}_{i-1},\alpha_{i},\mathbf{v}_{i},\hat{p}_{i})$ with
$\hat{p}_{i}\in\\{p_{i},p^{\prime}_{i}\\}$. Again, let $i\geq 1$ be an
arbitrary position such that there is an accepting hit in $r^{\prime}_{i}$. As
there are no accepting states in the first copy of $\mathcal{A}$ in
$\mathcal{A}^{\prime}$, there is a point where $r$ transitions from the first
copy to the second copy, i. e., there is a $j\leq i$ such that
$r^{\prime}_{j}=(p_{j-1},\alpha_{j},\mathbf{v}_{j},p_{j}^{\prime})$. Observe
that the counters are frozen after transitioning to the second copy, hence, we
have $\rho(r^{\prime}_{1}\dots r^{\prime}_{i})=\rho(r^{\prime}_{1}\dots
r^{\prime}_{j})\in C$. Furthermore, we have $p_{j}\in F$ by the choice of
$\Delta^{\prime}$. Finally, observe that $\hat{p}_{\ell}=p_{\ell}$ for all
$\ell<j$, and $\hat{p}_{\ell}=p^{\prime}_{\ell}$ for all $\ell\geq j$. Hence,
we can replace $r^{\prime}_{j}$ by
$r_{j}=(p_{j-1},\alpha_{j},\mathbf{v}_{j},p_{j})$, and for all $\ell>j$ we
replace $r^{\prime}_{\ell}$ by
$r_{\ell}=(p_{\ell-1},\alpha_{\ell},\mathbf{v}_{\ell},p_{\ell})$, where
$\mathbf{v}_{\ell}$ is arbitrary such that $r_{\ell}\in\Delta$ (observe that
at least one such $\mathbf{v}$ exists by definition of $\Delta^{\prime}$).
Then $r=r^{\prime}_{1}r^{\prime}_{2}\dots
r^{\prime}_{j-1}r_{j}r_{j+1}r_{j+2}\dots$ is a run of $\mathcal{A}$ on
$\alpha$ that is furthermore accepting as witnessed by the accepting hit in
$r_{j}$. Hence $\alpha\in R_{\omega}(\mathcal{A})$. ∎

Observe that a very similar construction can be used to turn an arbitrary RPBA
into an equivalent PPBA. The only difference is that we choose
$F^{\prime}=\\{q^{\prime}\mid q\in F\\}$. Hence we obtain the following
corollary.

######  Corollary 3.1.

$\mathcal{L}_{\mathsf{RPBA}}\subseteq\mathcal{L}_{\mathsf{PPBA}}$.

Finally, we show that this inclusion is also strict.

######  Lemma 3.3.

There is an $\omega$-language that is PPBA-recognizable but not RPBA-
recognizable.

###### Proof.

Consider
$L=\\{\alpha\in\\{a,b\\}^{\omega}\mid|\alpha[1,i]|_{a}=|\alpha[1,i]|_{b}\text{
for infinitely many $i$}\\}$, which is obviously PPBA-recognazable.

Assume that $L$ is recognized by an RPBA $\mathcal{A}$ and let $n$ be the
number of states of $\mathcal{A}$. Consider an accepting run
$r=r_{1}r_{2}r_{3}\ldots$ of $\mathcal{A}$ on $\alpha=(a^{n}b^{n})^{\omega}$
where $r_{i}=(p_{i-1},\alpha_{i},\mathbf{v}_{i},p_{i})$, and let $k$ be the
position of the accepting hit, i. e. $p_{k}\in F$ and $\rho(r_{1}\dots
r_{k})\in C$. By definition there are infinitely many $j\geq 1$ (and hence
infinitely many $j\geq k$) such that $p_{j}\in F$. By the pigeonhole
principle, there is a state $q$ that is visited twice while reading an
arbitrary $a^{n}$-infix, say at positions $k\leq c<d$, i. e., $p_{c}=p_{d}=q$
and $d-c<n$. Hence, we can pump an infix of the form $a^{d-c}$ and obtain an
accepting run on an infinite word of the form
$(a^{n}b^{n})^{*}(a^{n+d-c}b^{n})(a^{n}b^{n})^{\omega}$, which is not in $L$,
a contradiction. ∎

##  4 Characterization of $\mathcal{L}_{\mathsf{PA,Reg}}^{\omega}$ by limit
PBA and reachability PBA

The main goal of this section is to prove the following theorem.

######  Theorem 4.1.

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 LPBA-recognizable.

  3. 3.

$L$ is RPBA-recognizable.

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
regular, as regular languages are closed under concatenation.

To simplify the proof, it is convenient to consider the following
generalizations of Büchi automata. A _generalized Büchi automaton_ (GBA) is a
tuple $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,\mathcal{F})$ where $Q,\Sigma,q_{0}$
and $\Delta$ are defined as for BA, and $\mathcal{F}\subseteq 2^{Q}$ is a
collection of sets of accepting states. Then a run $r_{1}r_{2}r_{3}\dots$ with
$r_{i}=(p_{i-1},\alpha_{i},p_{i})$ is accepting if for all $F\in\mathcal{F}$
there are infinitely many $i$ such that $p_{i}\in F$. It is well-known that
GBA are not more expressive than BA, see e. g. [2, Theorem 4.56].

Furthermore, we consider a variant of GBA where acceptance is not defined via
states that are seen infinitely often, but rather via transitions that are
used infinitely often. A _Generalized Transition Büchi Automaton_ (GTBA) 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$ is accepting if for all $T\in\mathcal{T}$ there
are infinitely many $i$ such that $r_{i}\in T$.

######  Lemma 4.1.

GTBA and BA have the same expressiveness.

###### Proof.

Obviously, every BA can be turned into an equivalent GTBA by choosing
$\mathcal{T}=\\{\\{(p,a,q)\mid q\in F\\}\\}$, hence we focus on the other
direction.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,\mathcal{T})$ be a GTBA. As GBA are as
expressive as BA, it is sufficient to convert $\mathcal{A}$ into an equivalent
GBA. The idea is basically to consider the line graph of $\mathcal{A}$, that
is, to use $\Delta$ as the new state set, keeping the initial state. Then
there is a $b$-transition from the _state_ $(p,a,q)$ to every state of the
form $(q,b,t)$. Hence, the acceptance component translates directly. To be
precise, we construct the GBA
$\mathcal{A}^{\prime}=(\Delta\cup\\{q_{0}\\},\Sigma,q_{0},\Delta^{\prime},\mathcal{T})$
where
$\Delta^{\prime}=\\{((p,a,q),b,(q,b,t)\mid(p,a,q),(q,b,t)\in\Delta\\}\cup\\{(q_{0},a,(q_{0},a,q)\mid(q_{0},a,q)\in\Delta\\}$.
It is now easily verified that
$L_{\omega}(\mathcal{A})=L_{\omega}(\mathcal{A}^{\prime})$. ∎

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

######  Lemma 4.2.

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

###### Proof.

First observe that $\mathcal{L}_{\mathsf{LPBA}}$ is closed under union (this
can be shown using a standard construction). Hence, it is sufficient to show
how to construct an LPBA 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 an LPBA 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})$. Now 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 an RPBA (every visit of an accepting state
has the same good counter value; this argument is even true if we interpret
$\mathcal{A}$ as a PPBA), showing the implication $(1)\Rightarrow(3)$.

######  Corollary 4.1.

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

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.3.

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_{n})$ 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.

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

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

###### Proof.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ be an LPBA 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 GTBA.
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 GTBA 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 GTBA. 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 Lemma 4.3. Furthermore, we define the GTBA
$\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 GTBA). 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 in $\mathcal{T}^{D}$ by further adding the
component $\\{(p,a,q)\in\Delta\mid q\in F\\}$.

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.1 and Lemma 4.1 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 on $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 values 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 LPBA, 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})$. ∎

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

######  Lemma 4.5.

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

###### Proof.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ be an RPBA. The intuition is as
follows. An RPBA 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 $B_{\omega}(\mathcal{A})=\bigcup_{f\in F}L(\mathcal{A}_{f})\cdot
L_{\omega}(\mathcal{B}_{f})$.

$\Rightarrow$ To show $B_{\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 B_{\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})$. ∎

##  5 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}$. Grobler et al. [6] have shown that
$\mathcal{L}_{\mathsf{PA,PA}}^{\omega}\subsetneq\mathcal{L}_{\mathsf{SPBA}}$,
i. e., SPBA are too strong to capture this class. However, restrictions of
SPBA 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 section. Further restricting the vectors yields a model capturing
$\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$, as specified in the second theorem
of this section. Recall that the condensation of $\mathcal{A}$ is the DAG of
strong components of the underlying graph of $\mathcal{A}$.

######  Theorem 5.1.

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 an SPBA $\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.

In fact, the proof of Grobler et al. [6] showing
$\mathcal{L}_{\mathsf{PA,PA}}^{\omega}\subseteq\mathcal{L}_{\mathsf{SPBA}}$ is
constructive and _almost_ yields an SPBA with the desired property. A key
notion are _normalized_ PA (on finite words), where a PA
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F)$ is normalized if $F=\\{f\\}$ and $f$
has no outgoing transitions. It was shown that one can, given a PA
$\mathcal{A}$, construct a normalized PA $\mathcal{A}_{N}$ with
$L(\mathcal{A}_{N})=L(\mathcal{A})\setminus\\{\varepsilon\\}$. For our proofs
it is convenient to introduce a similar, yet stronger notion.

######  Lemma 5.1.

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

  * 1.

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

  * 2.

$L(\mathcal{A})\setminus\\{\varepsilon\\}=L(\mathcal{A}^{IO})\setminus\\{\varepsilon\\}$.

  * 3.

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

We say that $\mathcal{A}^{IO}$ is _IO-normalized_.

###### Proof.

Define
$\mathcal{A}^{IO}=\\{Q\cup\\{q_{0}^{\prime}\\},\Sigma,q_{0}^{\prime},\Delta^{IO},\\{q_{0}^{\prime}\\},C\cdot\\{1\\})$,
where

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

That is, $\mathcal{A}^{IO}$ is obtained from $\mathcal{A}$ by adding a fresh
state $q_{0}^{\prime}$, which is the initial state and only accepting state,
inherits all outgoing transitions from $q_{0}$ and all in-going transitions
from the accepting states. Furthermore, all transitions get a new counter,
which is set to 0 except for the new ingoing transitions of $q_{0}^{\prime}$
where the counter is set to $1$, and all vectors in $C$ are concatenated with
$1$. Finally, we remove all states that cannot reach $q^{\prime}_{0}$ (such
states can appear when shortcutting the ingoing 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 third property). We claim that
$L(\mathcal{A})\setminus\\{\varepsilon\\}=L(\mathcal{A}^{IO})\setminus\\{\varepsilon\\}$.

$\Rightarrow$ To show $L(\mathcal{A})\setminus\\{\varepsilon\\}\subseteq
L(\mathcal{A}^{IO})\setminus\\{\varepsilon\\}$, let $w_{1}\dots w_{n}\in
L(\mathcal{A})$ for $n\geq 1$ with accepting run $r=r_{1}\dots r_{n}$ where
$r_{i}=(p_{i-1},w_{i},\mathbf{v}_{i},p_{i})$. By definition of $\Delta^{IO}$,
there is a transition
$r^{\prime}_{1}=(q_{0}^{\prime},w_{1},\mathbf{v}_{1}\cdot 0,p_{1})$ as well as
a transition $r^{\prime}_{n}=(p_{n-1},w_{n},\mathbf{v}_{n}\cdot
1,q_{0}^{\prime})$ (or in case $n=1$ the loop
$(q_{0}^{\prime},w_{1},\mathbf{v}_{1}\cdot 1,q_{0}^{\prime})$). For all
$1<i<n$ define $r^{\prime}_{i}=(p_{i-1},w_{i},\mathbf{v}_{i}\cdot 0,p_{i})$.
It is now easily verified that $r^{\prime}_{1}\dots r^{\prime}_{n}$ (or simply
$(q_{0}^{\prime},w_{1},\mathbf{v}_{1}\cdot 1,q_{0}^{\prime})$) is an accepting
run of $\mathcal{A}^{IO}$ on $w_{1}\dots w_{n}$.

$\Leftarrow$ To show $L(\mathcal{A}^{IO})\setminus\\{\varepsilon\\}\subseteq
L(\mathcal{A})\setminus\\{\varepsilon\\}$, let $w_{1}\dots w_{n}\in
L(\mathcal{A}^{IO})$ for $n\geq 1$ with accepting run
$r^{\prime}=r^{\prime}_{1}\dots r^{\prime}_{n}$ where
$r^{\prime}_{i}=(p_{i-1},w_{i},\mathbf{v}_{i}\cdot c_{i},p_{i})$ with
$c_{i}\in\\{0,1\\}$. Observe that $p_{0}=p_{n}=q_{0}^{\prime}$, and for all
$0<i<n$ we have $p_{i}\neq q_{0}^{\prime}$ as enforced by the additional
counter (that is, $c_{n}=1$ and $c_{i}=0$ for all $i<n$, as $C\cdot\\{1\\}$ is
the semi-linear set of $\mathcal{A}^{IO}$). By definition of $\Delta^{IO}$
there is a transition $r_{1}=(q_{0},w_{1},\mathbf{v}_{1},p_{1})$, and a
transition $r_{n}=(p_{n-1},w_{n},\mathbf{v}_{n},f)$ for some $f\in F$ in
$\Delta$ (or in case $n=1$ the transition $(q_{0},w_{1},\mathbf{v}_{1},f)$).
For all $1<i<n$ define $r_{i}=(p_{i-1},w_{i},\mathbf{v}_{i},p_{i})$. It is now
easily verified that $r_{1}\dots r_{n}$ (or simply
$(q_{0},w_{1},\mathbf{v}_{1},f)$) is an accepting run of $\mathcal{A}$ on
$w_{1}\dots w_{n}$. ∎

Observe that $L(\mathcal{A})^{\omega}=L(\mathcal{A}^{IO})^{\omega}$ for every
PA $\mathcal{A}$, as $L^{\omega}=(L\setminus\\{\varepsilon\\})^{\omega}$ for
every language $L$ by definition. In fact, it is easily observed that we even
have $S_{\omega}(\mathcal{A}^{IO})=L(\mathcal{A})^{\omega}$. We are now ready
to proof the main theorem.

###### Proof of Theorem 5.1.

$(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 Lemma
5.1 and the observation above we can equivalently write
$L=L(\mathcal{A}_{1})\cdot S_{\omega}(\mathcal{A}^{IO}_{2})$. As
$\mathcal{A}^{IO}_{2}$ is IO-normalized it satisfies the property of the
theorem.

We can now easily adapt the construction in [6] showing that the concatenation
of a Parikh-recognizable language and an SPBA-recognizable $\omega$-language
is SPBA-recognizable to obtain an SPBA for $L(\mathcal{A}_{1})\cdot
S_{\omega}(\mathcal{A}^{IO}_{2})$ that only keeps the accepting state of
$\mathcal{A}^{IO}_{2}$, maintaining the property of the theorem. Finally, the
closure under union is shown using a standard construction, hence combining
SPBA with the desired property still yields an SPBA with the property.
Overall, we obtain an SPBA $\mathcal{A}$ recognizing $L$ where the only
accepting states appear in the leaves of $C(\mathcal{A})$. $\lrcorner$

$(2)\Rightarrow(1)$. Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ be an SPBA
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 of the ingoing 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 $S_{\omega}(\mathcal{A})=\bigcup_{f\in
F}L(\mathcal{A}_{f})\cdot L(\mathcal{A}_{f,f})^{\omega}$.

$\Rightarrow$ To show $S_{\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 all $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 SPBA. 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_{1}+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_{k_{i+1}}$, we have $\rho(r^{\prime}_{k_{i}+1}\dots
r_{k_{i+1}})=\mathbf{v}\cdot 1\in C\cdot\\{1\\}$, and hence
$\alpha[k_{1}+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 S_{\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 S_{\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
S_{\omega}(\mathcal{A})$, concluding the proof. ∎

As a side product of the proof of Theorem 5.1 we get the following corollary,
which is in general not true for SPBA.

######  Corollary 5.1.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ be an SPBA 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
$S_{\omega}(\mathcal{A})=\bigcup_{f\in
F}S_{\omega}(Q,\Sigma,q_{0},\Delta,\\{f\\},C)$.

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

######  Theorem 5.2.

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 an SPBA $\mathcal{A}$ with the following properties.

    1. (a)

At most one state $q$ per leaf of the condensation of $\mathcal{A}$ may have
ingoing 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 5.1,
hence, SPBA 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 5.1. Hence, property (b) is mandatory to sufficiently weaken SPBA such
that they capture $\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$. In fact, using the
notion of IO-normalization, we can re-use most of the ideas in the proof of
Theorem 5.1.

###### Proof of Theorem 5.2.

$(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 observe that $\mathcal{A}^{IO}$ has only a single SCC
by definition. Again, we have
$L(\mathcal{A})^{\omega}=S_{\omega}(\mathcal{A}^{IO})$ and the constructions
for concatenation and union do not destroy the properties, hence we obtain an
SPBA of the desired form. $\lrcorner$

$(2)\Rightarrow(1)$ Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,C)$ be an SPBA
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 5.1, 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 $S_{\omega}(\mathcal{A})=\bigcup_{f\in F}L(\mathcal{B}_{f})\cdot
L(\mathcal{A}_{f})^{\omega}$.

$\Rightarrow$ To show $S_{\omega}(\mathcal{A})=\bigcup_{f\in
F}L(\mathcal{B}_{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})$, 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 5.1 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 S_{\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 S_{\omega}(\mathcal{A})$, concluding
the proof. ∎

##  6 Conclusion

We conclude with an overview of our results shown in Figure 2.

complete RPARPARPBA = LPBA = $\mathcal{L}_{\mathsf{PA,Reg}}^{\omega}$BA =
$\mathcal{L}_{\mathsf{Reg,Reg}}^{\omega}$SPBA $(**)$ =
$\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$PPBASPBA $(*)$ =
$\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$SPBARemark 3.1Lemma 3.2Corollary 3.1[5,
6], [7][6]$\neq$Lemma 3.1$\neq$$\neq$$\neq$Theorem 4.1Theorem 5.2Theorem
2.1Theorem 5.1$(*)$ At most one state $q$ per leaf of $C(\mathcal{A})$ may
have ingoing 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 2: Overview of our results. Arrows mean strict
inclusions and $\neq$ means orthogonal.

To finalize the picture, we observe the following.

######  Observation 6.1.

  1. 1.

There are RPA-recognizable $\omega$-languages not contained in
$\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$, for example $\\{a^{n}b^{n}\mid n\geq
0\\}\\{a\\}^{\omega}$.

  2. 2.

We have
$\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}\subseteq\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$
by definition, and there are $\omega$-languages contained in
$\mathcal{L}_{\mathsf{PA,PA}}^{\omega}$ that are not contained in
$\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$, for example $\\{a^{n}b^{n}\mid n\geq
1\\}\\{c^{n}d^{n}\mid n\geq 1\\}^{\omega}$.

  3. 3.

We have
$\mathcal{L}_{\mathsf{Reg,Reg}}^{\omega}\subseteq\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$
by definition, and there are $\omega$-languages contained in
$\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$ that are neither PPBA-recognizable
nor $\omega$-regular, as witnessed by many $\omega$-closures of Parikh-
recognizable languages (which are trivially contained in
$\mathcal{L}_{\mathsf{Reg,PA}}^{\omega}$), for example $\\{a^{n}b^{n}\mid
n\geq 1\\}^{\omega}$ (a formal proof can be found for blind counter machines
in [5], which are known to be equivalent to PPBA [6]).

Finally, 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\\}$ [10].
This characterization can easily be adapted to show that deterministic PPBA-
recognizable $\omega$-languages are captured by arrows of deterministic
Parikh-recognizable languages. We conjecture that PPBA-recognizable
$\omega$-languages are captured by arrows of Parikh-recognizable languages
yielding a similar characterization of $\mathcal{L}_{\mathsf{PPBA}}$.

## References

  * [1] Joël Allred and Ulrich Ultes-Nitsche.  $k$-counting automata.  RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, 46(4):461–478, 2012.
  * [2] Christel Baier and Joost-Pieter Katoen.  Principles of Model Checking.  The MIT Press, 2008.
  * [3] Mikolaj Bojanczyk.  Beyond omega-Regular Languages.  In Jean-Yves Marion and Thomas Schwentick, editors, 27th International Symposium on Theoretical Aspects of Computer Science, volume 5 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11–16, Dagstuhl, Germany, 2010. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.
  * [4] J. Richard Büchi.  Weak second-order arithmetic and finite automata.  Mathematical Logic Quarterly, 6(1‐6):66–92, 1960.
  * [5] Henning Fernau and Ralf Stiebe.  Blind counter automata on omega-words.  Fundam. Inform., 83:51–64, 2008.
  * [6] Mario Grobler, Leif Sabellek, and Sebastian Siebertz.  Parikh automata on infinite words, 2023.
  * [7] Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann.  Parikh automata over infinite words, 2022.
  * [8] Felix Klaedtke and Harald Rueß.  Monadic second-order logics with cardinalities.  In Jos C. M. Baeten, Jan Karel Lenstra, Joachim Parrow, and Gerhard J. Woeginger, editors, Automata, Languages and Programming, pages 681–696, Berlin, Heidelberg, 2003. Springer.
  * [9] Dario Della Monica, Angelo Montanari, and Pietro Sala.  Beyond $\omega$BS-regular languages: $\omega$t-regular expressions and counter-check automata.  Electronic Proceedings in Theoretical Computer Science, 256:223–237, 2017.
  * [10] Wolfgang Thomas.  Automata on Infinite Objects, page 133–191.  MIT Press, Cambridge, MA, USA, 1991.