Deterministic Parikh automata on infinite words

Mario Grobler

University of Bremen

Sebastian Siebertz

University of Bremen

Various variants of Parikh automata on infinite words have recently been introduced and studied in the literature.
However, with some exceptions only their non-deterministic versions have been studied.
In this paper we study the deterministic versions of all variants of Parikh automata on infinite words that have not yet been studied in the literature.
We compare the expressiveness of the deterministic models, study their closure properties and decision problems with applications to model checking.
The model of deterministic limit Parikh automata turns out to be most interesting, as it is the only deterministic Parikh model generalizing the $\omega$-regular languages, the only deterministic Parikh model closed under the Boolean operations and the only deterministic Parikh model for which all common decision problems are decidable.

<concept_desc>Theory of computation Automata over infinite objects</concept_desc>

[500]Theory of computation Automata over infinite objects

We thank Georg Zetzsche for insightful discussions and valuable remarks.

§ INTRODUCTION

Finite automata operating on infinite words find many applications in the world of formal languages, logic, formal verification, games, and many more.
In many scenarios, non-determinism adds expressiveness or succinctness to their deterministic counterparts. However, this often comes at the price of important decision problems becoming hard to solve, or even undecidable <cit.>.

This is not only true for the most common model of finite automata operating on infinite words, namely Büchi automata (which recognize the $\omega$-regular languages), but also for various extensions leaving the $\omega$-regular realm.
These include Parikh automata (PA) on infinite words, which gained a lot of attention just recently <cit.>. Such automata are equipped with a constant number of counters (positive integers), and the counter values can be checked to satisfy some linear constraints.
Several acceptance conditions for Parikh  on infinite words have been studied in the literature, including deterministic and non-deterministic reachability PA, safety PA, Büchi PA and co-Büchi PA <cit.>, as well as non-deterministic limit PA, reachability-regular PA, and strong and weak reset PA <cit.>.
For all of these models, except safety PA and co-Büchi PA, testing emptiness is -complete and universality is undecidable <cit.>. In contrast, for safety PA and co-Büchi PA, both problems are undecidable; however, requiring determinism yields a -complete universality problem.

This motivates the study of the deterministic variants of the remaining models, namely deterministic limit PA, reachability-regular PA, strong reset PA, and weak reset PA.
In this paper we study their expressiveness, closure properties and common decision problems.
Grobler et al. <cit.> have shown that almost all non-deterministic variants of the aforementioned models (the exception being safety PA and co-Büchi PA again) form a hierarchy:
\begin{align*}
\text{reach~PA } & \subseteq \text{ reachability-regular~PA } = \text{ limit~PA}
\\
& \subseteq \text{ Büchi~PA } \subseteq
\text{ weak reset~PA } = \text{ strong reset~PA.}
\end{align*}

First, we show that this is not the case for their deterministic variants. While

\[\text{deterministic strong reset~PA $\subseteq$ deterministic weak reset~PA}\]

\begin{align*}
\text{
deterministic} & \text{ reachability~PA} \\ &\subseteq \text{ deterministic reachability-regular~PA} \\ & \subseteq \text{deterministic weak reset~PA}
\end{align*}

still holds, all other models become pairwise incomparable.
Furthermore, we show that among all studied deterministic models only deterministic limit PA generalize Büchi automata in the sense that they recognize all $\omega$-regular languages.

Deterministic limit PA also shine in the light of closure properties: among all studied PA operating on infinite words (the deterministic variants as well as the non-deterministic ones) they are the only ones closed under union, intersection and complement.
This benefit also yields decidable decision problems. In contrast to the other models that were studied in <cit.>, emptiness and universality are decidable for deterministic limit PA. We show that also strong reset PA benefit from determinism: although having bad closure properties their universality problems becomes decidable. However, as we show, for deterministic reachability-regular PA and deterministic weak reset PA the universality problem remains undecidable.

$\cup$     $\cap$     $\bar{\phantom{a}}$

deterministic limit PA

deterministic reachability-regular PA

deterministic weak reset PA

deterministic strong reset PA

Closure properties.

$L = \varnothing?$     $uv^\omega \in L?$     $L = \Sigma^\omega?$

det. limit PA     -c.     -c.     decidable

det. reach-reg.  PA     coNP-c.     -c.     undecidable

det. weak reset PA     -c.     -c.     undecidable

det. strong reset PA     -c.     -c.     decidable

Decision problems.

Finally, we study their inclusion and intersection emptiness problems, as these are important problems in order to study model checking problems. Here, we are given a system $\Kmc$ as a Kripke structure (a safety automaton) or a PA and a specification $\Amc$ as a PA. The question whether at least one computation of a Kripke structure satisfies the specification (which we call existential safety model checking) has been studied in <cit.>.
The authors show that this problem is $\coNP$-complete for (nondeterministic) reset PA and for all models that are weaker.
Similarly, the question whether all computations of a PA satisfy the specification (which we call universal PA model checking) has been studied in <cit.>. The authors show that this problem is $\coNP$-complete for deterministic safety and co-Büchi PA, and undecidable for their nondeterministic counterparts as well as for deterministic reachability and Büchi PA.
We study this problem as well as the universal safety model checking problem and the existential PA model checking problem for the remaining deterministic models.
Again, deterministic limit PA shine as all these problems are decidable for them. For the other models, some problems are decidable and some are not.

In the following table we list our results. Some of the questions have already been studied in the literature or follow immediately from the results of <cit.>.
We fill the missing gaps and remark that these results are the technically most demanding results of this paper.

4cModel Checking

2c|Kripke     2cPA

1c|$\exists$     1c|$\forall$     1c|$\exists$     1c$\forall$

det. limit PA     <cit.>

det. reach-reg. PA    <cit.>

det. weak reset PA    <cit.>

det. strong reset PA    <cit.>

det. reachability PA    <cit.>      <cit.>     <cit.>     <cit.>

det. Büchi PA    <cit.>     <cit.>        <cit.>

det. safety PA     <cit.>     <cit.>     <cit.>     <cit.>

det. co-Büchi PA     <cit.>     <cit.>     <cit.>     <cit.>

Decidability of the model checking problem.

§.§ Related work

Parikh automata on finite words were introduced by Klaedtke and Ruess in <cit.> in order to show that an extension of weak monadic second-order logic (MSO) with cardinality constraints is decidable. PA turn out to be equivalent to Ibarra's reversal bounded multi-counter machines <cit.> and Greibach's blind counter machines <cit.>, which are also known as integer vector addition systems with states ($\Zbb$-$\mathsf{VASS}$) <cit.>. Furthermore, they can be efficiently translated into each other <cit.>.
The study of Parikh automata on infinite words was initiated just recently by Guha et al. <cit.>, followed by <cit.>.
Closely related to PA on infinite words are blind counter machines on infinite words, as introduced by Fernau and Stiebe <cit.>. Indeed, these machines turn out to be equivalent to Büchi PA <cit.>. Another model of automata with counters on infinite words are Büchi $\mathsf{VASS}$.
A recent result by Baumann et al. shows that their regular separability problem (that is, the question whether an $\omega$-regular languages separates two $\omega$-languages recognized by Büchi $\mathsf{VASS}$) is decidable <cit.>.
Another recent work shows the impact of PA on infinite words.  et al. <cit.> introduce a logic subsuming counting MSO and Boolean algebra with Presburger arithmetic, and show decidability over labeled infinite binary trees by introducing Parikh-Muller tree automata (which can be seen as an extension of reachability-regular PA to trees).
Yet another recent work by Bergsträßer et al. <cit.> shows that Ramsey quantifiers in Presburger arithmetic can be eliminated efficiently.
Such a quantifier basically asks for the existence of an infinite clique in the graph induced by some formulas. The authors show that their results strengthen recent results on PA on infinite words. We use these results on Ramsey quantifiers to give an explicit application, namely that intersection emptiness of two Büchi PA is decidable, and hence their existential PA model checking problem.

§ PRELIMINARIES

§.§ Finite and infinite words

We write $\Zbb$ for the set of all integers and $\Nbb$ for the set of non-negative integers including $0$. Furthermore, let $\Nbbinfty = \Nbb \cup \{\infty\}$. Throughout the paper we use the variables $c,d,k,\ell,m,n,z$ to denote positive integers and we will tacitly assume this without explicit mention. Let $\Sigma$ be an alphabet, , 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 : \Nbb \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_1w_2\dots \mid w_i \in L \setminus \{\varepsilon\}\} \subseteq \Sigma^\omega$.
We call a non-empty $\omega$-language $L \subseteq \Sigma^\omega$ ultimately periodic if it contains an infinite word of the form $uv^\omega$ for finite words $u,v \in \Sigma^*$. We refer to such infinite words also as ultimately periodic.

§.§ Regular and omega-regular languages

A non-deterministic finite automaton (NFA) is a schnuple $\Amc = (Q, \Sigma, q_0, \Delta, F)$, where $Q$ is a 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.
We call $\Amc$ deterministic if for every pair $(p, a) \in Q \times \Sigma$ there is exactly one transition of the form $(p, a, q) \in \Delta$ for some $q \in Q$.
A run of $\Amc$ 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 $\epsilon$ is accepting if $q_0 \in F$. We define the language recognized by  as $L(\Amc) = \{w \in \Sigma^* \mid \text{there is an accepting run of $\Amc$ on $w$}\}$. If a language $L$ is recognized by some NFA $\Amc$, we call $L$ regular.

A Büchi automaton is an NFA $\Amc = (Q, \Sigma, q_0, \Delta, F)$ that takes  words as input.
A run of $\Amc$ 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 $\Amc$ as $L_\omega(\Amc) = \{\alpha \in \Sigma^\omega \mid \text{there is an accepting run of $\Amc$ on $\alpha$}\}$.
If an $\omega$-language $L$ is recognized by some Büchi automaton $\Amc$, we call $L$ $\omega$-regular.
If every state of a Büchi automaton $\Amc$ is accepting, we call $\Amc$ a safety automaton.
Similarly, a Muller automaton is a tuple $\Amc = (Q, \Sigma, q_0, \Delta, \Fmc)$, where $Q, \Sigma, q_0$, and $\Delta$ are defined as for Büchi automata, and $\Fmc \subseteq 2^Q$ is a collection of sets of accepting states. Runs are defined as for Büchi automata, and a run $r$ is accepting if the sets of states that appear infinitely often in $r$ is contained in $\Fmc$.
Deterministic Muller automata have the same expressiveness as non-deterministic Büchi automata <cit.>. However, deterministic Büchi automata are less expressive than their non-deterministic counterpart <cit.>.
If an $\omega$-language $L$ is recognized by some deterministic Büchi automaton, we call $L$ deterministic $\omega$-regular.
For a (finite word) language $L \subseteq \Sigma^*$, we define $\vec{L} = \{\alpha \in \Sigma^\omega \mid \alpha[1:i] \in L \text{ for infinitely many } i\}$. An $\omega$-language $L$ is deterministic $\omega$-regular if and only if $L = \vec{W}$ for a regular language $W$ <cit.>.

§.§ Semi-linear sets

A linear set (of dimension $d\geq 1$) is a set of the form $C(\bbf, P) = \{\bbf + \pbf_1z_1 + \dots + \pbf_\ell z_\ell \mid z_1, \dots, z_\ell \in \Nbb\} \subseteq \Nbb^d$, where $\bbf \in \Nbb^d$ and $P = \{\pbf_1, \dots, \pbf_\ell\} \subseteq \Nbb^d$ is a finite set of vectors for some $\ell \geq 0$. We call $\bbf$ the base vector and $P$ the set of period vectors.
A semi-linear set is a finite union of linear sets.
We also consider semi-linear sets over $\Nbbinfty^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  for all $z \in \Nbb$, $z \cdot \infty = \infty \cdot z = \infty$ for all $z \geq 1$, and .
For vectors $\ubf = (u_1, \dots, u_c)\in \Nbbinfty^c$ and $\vbf = (v_1, \dots, v_d) \in \Nbbinfty^d$, we denote by $\ubf \cdot \vbf = (u_1, \dots, u_c, v_1, \dots, v_d) \in \Nbbinfty^{c+d}$ the concatenation of $\ubf$ and $\vbf$.
We extend this definition to sets of vectors. Let $C \subseteq \Nbbinfty^c$ and $D \subseteq \Nbbinfty^d$. Then $C \cdot D = \{\ubf \cdot \vbf \mid \ubf \in C, \vbf \in D\} \subseteq \Nbbinfty^{c+d}$.
We denote by $\0^d$ the $d$-dimensional all-zero vector, by $\1^d$ the $d$-dimensional all-one-vector, by $\ebf^d_i$ the $d$-dimensional vector where the $i$th entry is $1$ and all other entries are 0, and by $\ibf^d_i$ the $d$-dimensional vector where the $i$th entry is $\infty$ and all other entries are 0. We often drop the superscript $d$ if the dimension is clear.

§.§ Parikh-recognizable languages

A Parikh automaton (PA) is a tuple $\Amc = (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 \Nbb^d \times Q$, for some , is a finite set of labeled transitions, and $C \subseteq \Nbb^d$ is a semi-linear set.
We call $d$ the dimension of $\Amc$ and interpret $d$ as a number of counters.

Analogously to NFA, we call $\Amc$ deterministic if for every pair $(p,a) \in Q \times \Sigma$ there is exactly one labeled transition of the form  for some $\vbf \in \Nbb^d$ and $q \in Q$.
A run of $\Amc$ 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, \vbf_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} \vbf_i$ (with the convention that the empty sum equals $\0$).
We say $r$ is accepting if $p_n \in F$ and ,
referring to the latter condition as the Parikh condition.
The language recognized by  is  there is an accepting run of $\Amc$ on $w\}$.

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

Let $\Amc = (Q, \Sigma, q_0, \Delta, F, C)$ be a PA. A run of $\Amc$ 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, \vbf_i, p_i)\in \Delta$ such that $p_0 = q_0$.
The automata defined below differ only in their acceptance conditions, hence they are syntactically equivalent but semantically different (the notion of determinism translates directly). In the following, whenever we say that an automaton $\Amc$ accepts an infinite word $\alpha$, we mean that there is an accepting run of $\Amc$ on $\alpha$.
We begin with the models studied by Guha et al. <cit.>, who also studied the deterministic variants of the these models.

* 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 <cit.>.
We define the $\omega$-language recognized by a safety PA $\Amc$ as

\[S_\omega(\Amc) = \{\alpha\in \Sigma^\omega\mid \Amc \text{ accepts }\alpha\}.\]

* 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 <cit.>. We define the $\omega$-language recognized by a reachability PA $\Amc$ as

\[R_\omega(\Amc) = \{\alpha\in \Sigma^\omega\mid \Amc \text{ accepts }\alpha\}.\]

* 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 <cit.>.
We define the $\omega$-language recognized by a Büchi PA $\Amc$ as

\[B_\omega(\Amc) = \{\alpha\in \Sigma^\omega\mid \Amc \text{ accepts }\alpha\}.\]

* 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 .
We call a PA accepting with the co-Büchi condition a co-Büchi PA <cit.>.
We define the $\omega$-language recognized by a co-Büchi PA $\Amc$ as

\[CB_\omega(\Amc) = \{\alpha\in \Sigma^\omega\mid \Amc\text{ accepts }\alpha\}.\]

Furthermore, Guha et al. <cit.> assume that reachability PA are complete, i.e., for every $(p,a)\in Q\times \Sigma$ there are $\vbf\in \Nbb^d$ and $q\in Q$ such that $(p,a,\vbf,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. Observe that their deterministic variants are always complete by definition.

Now we recall the models introduced in <cit.>.

* 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 <cit.>. We define the $\omega$-language recognized by a reachability-regular PA $\Amc$ as
\[RR_\omega(\Amc) = \{\alpha\in \Sigma^\omega\mid \Amc\text{ accepts }\alpha\}.\]

* 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 $\vbf_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 <cit.>.
We define the $\omega$-language recognized by a limit PA $\Amc$ as
\[L_\omega(\Amc) = \{\alpha\in \Sigma^\omega\mid  \Amc\text{ accepts }\alpha\}.\]

* 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 the sequence $k_1, k_2, \dots$ is infinite 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 <cit.>. We define the $\omega$-language recognized by a strong reset PA $\Amc$ as
\[SR_\omega(\Amc) = \{\alpha\in \Sigma^\omega\mid \Amc\text{ accepts }\alpha\}.\]

* 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 <cit.>.
We define the $\omega$-language recognized by a weak reset PA $\Amc$ as
\[W\!R_\omega(\Amc) = \{\alpha\in \Sigma^\omega\mid \Amc\text{ 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.
The equivalence of the (non-deterministic variants of the) two models is shown in <cit.>.
Furthermore, it is shown in <cit.>  that (non-deterministic) limit PA and (non-deterministic) reachability-regular are equivalent, as they recognize exactly $\omega$-languages of the form $\bigcup_i U_i V_i^\omega$, where the $U_i$ are (finite word) languages recognized by PA, and the $V_i$ are regular languages.

§ EXPRESSIVENESS

In this section we study the expressiveness of deterministic PA on infinite words for those models whose deterministic variants were not studied before in the literature.
When we show non-inclusions, we always give the strongest separation. By abuse of notation we simply write that a model is a strict/no subset of another model; by that we mean that the class of $\omega$-languages recognized by the first model is a strict/no subset of the class of $\omega$-languages recognized by the second model.

§.§ omega-regular languages

We begin by showing that every $\omega$-regular language is deterministic limit PA recognizable.

$\omega$-regular $\subsetneq$ deterministic limit PA.

Let $L \subseteq \Sigma^\omega$ be $\omega$-regular and let $\Amc = (Q, \Sigma, q_0, \Delta, \Fmc)$ be a deterministic Muller automaton recognizing $L$.
The idea is to construct an equivalent deterministic limit PA $\Amc' = (Q, \Sigma, q_0, \Delta', Q, C)$ of dimension $|Q|$, where every state is accepting, while encoding the sets in $\Fmc$ into the semi-linear set $C$.
Let $f : Q \rightarrow \{1, \dots, |Q|\}$ be a bijection associating every state with a counter. Hence, we define $\Delta' = \{(p, a, \ebf_{f(q)}^{|Q|}, q) \mid (p, a, q) \in \Delta\}$.

For every $F \in \Fmc$, we define $C_F = C(\sum_{q \in F} \ibf_{f(q)}, \{\ebf_{f(q)} \mid q \notin F\})$.
That is, for every state in $F$ we expect its counter value to be $\infty$, while we expect every other counter value to be a finite number. We choose $C = \bigcup_{F \in \Fmc}C_F$ and hence obtain an equivalent deterministic limit PA.

The strictness is witnessed by the $\omega$-language $\{a^n b^n c^\omega \mid n > 0\}$, which is obviously deterministic limit PA recognizable, but not $\omega$-regular.

It turns out that all other models do not recognize all regular $\omega$-languages.

[anchor=west] at (0,0) $\omega$-regular;

at (1.6, 0) $\not\subseteq$;

[decorate, thick,
decoration = calligraphic brace, raise = 2pt, amplitude = 4pt,mirror] (2.1,0.8) –  (2.1,-0.8);

[anchor=west] at (2.2,0.65) Deterministic reach-reg. PA;
[anchor=west] at (2.2,0.25) Deterministic Büchi PA;
[anchor=west] at (2.2,-0.25) Deterministic strong reset PA;
[anchor=west] at (2.2,-0.65) Deterministic weak reset PA;

None of these PA recognize $L_{a<\infty} = \{\alpha \in \{a,b\}^\omega \mid |\alpha|_a < \infty\}$, which is obviously $\omega$-regular. The proof that these models do not recognize $L_{a<\infty}$ mimics the standard proof showing that this $\omega$-language is not deterministic $\omega$-regular, see .

Observe however these models generalize deterministic Büchi automata. This however is not true for deterministic reach PA, deterministic safety PA nor deterministic , as shown in the next lemma.

[anchor=west] at (0,0) Deterministic $\omega$-regular;

at (3.4, 0) $\not\subseteq$;

[decorate, thick,
decoration = calligraphic brace, raise = 2pt, amplitude = 4pt,mirror] (3.9,0.66) –  (3.9,-0.66);

[anchor=west] at (4,0.47) Deterministic reach PA;
[anchor=west] at (4,0) Deterministic safety PA;
[anchor=west] at (4,-0.4) Deterministic co-Büchi PA;

As an immediate consequence of <Ref> (proved below) we have that no deterministic reach PA recognizes the deterministic  language $a^* b^\omega$.

Guha et al. <cit.> have shown that (even non-deterministic) safety PA do not recognize the det. $\omega$-regular language .

Finally, dually to the previous proof we can show that no co-Büchi PA recognizes the deterministic $\omega$-regular language $L_{a=\infty}=\{\alpha \in \{a,b\}^\omega \mid |\alpha|_a = \infty\}$.

§.§ Deterministic Safety PA and co-Büchi PA

As a consequence of <Ref> we obtain the following corollary.

[anchor=west] at (0,0) Deterministic reach-reg. PA;
[anchor=west] at (0,-0.4) Deterministic limit PA;
[anchor=west] at (0,-0.8) Deterministic Büchi PA;
[anchor=west] at (0,-1.25) Deterministic strong reset PA;
[anchor=west] at (0,-1.6) Deterministic weak reset PA;

decoration = calligraphic brace, raise = 2pt, amplitude = 4pt] (4,0.2) –  (4,-1.8);

at (4.5, -0.8) $\not\subseteq$;

[decorate, thick,
decoration = calligraphic brace, raise = 2pt, amplitude = 4pt,mirror] (5,-0.3) –  (5,-1.3);

[anchor=west] at (5,-0.6) Deterministic safety PA;
[anchor=west] at (5,-1.1) Deterministic co-Büchi PA;

As shown in <cit.> also deterministic reach PA $\not\subseteq$ deterministic safety PA and deterministic reach PA $\not\subseteq$ deterministic co-Büchi PA. Furthermore, the classes of deterministic safety PA and deterministic co-Büchi PA are themselves incomparable as shown in <cit.>.

Vice versa, deterministic safety PA $\not\subseteq$ non-deterministic weak reset PA and deterministic co-Büchi PA $\not\subseteq$ non-deterministic weak reset PA <cit.>. Hence, these classes are no subclasses of any of the other studied classes.

Overall, deterministic safety PA and deterministic co-Büchi PA are incomparable with all other studied models.

§.§ Deterministic Reach PA

We begin by characterizing the class of deterministic reach PA recognizable $\omega$-languages.

An $\omega$-language $L$ is deterministic reach PA recognizable if and only if $L = U \Sigma^\omega$, where $U \subseteq \Sigma^*$ is recognized by a deterministic PA.

Let $\Amc$ be a deterministic reach PA recognizing $L$. Then we have $L(\Amc) = U$. Likewise, if $\Amc$ is a PA recognizing $U$, then  (recall that is complete by the definition of determinism).

We have the following strict inclusion.

Deterministic reach PA $\subsetneq$ deterministic reach-reg. PA.

Let $\Amc$ be a deterministic reach PA. We may assume that every state of $\Amc$ is accepting, as we can project the current state into the semi-linear set. To be precise, we introduce two new counters for each state of $\Amc$, counting the number of visits and exits. Then, the current state is the (unique) state with one more visit than exit, or in case that the number of visits and exits is the same for every state, then the current state is the initial state of $\Amc$.
As these statements can be encoded into a semi-linear set, we can assume that every state is equipped with its own semi-linear set, and can hence make every state accepting (and assign the empty set if we want to simulate a non-accepting state).
If every state is accepting, then $\Amc$ is an equivalent deterministic reach-reg PA.

The strictness is witnessed e.g. by the $\omega$-language $\{a^nb^na^\omega\mid n>0\}$, which is deterministic reach-reg PA recognizable and by <Ref> not deterministic reach PA recognizable.

It remains to show the following incomparability results.

Deterministic reach PA $\not\subseteq$ deterministic limit PA.

We show that the deterministic reach PA recognizable $\omega$-language $L = \{\alpha \mid |\alpha[1:i]|_a = |\alpha[1:i]|_b \text{ for some }i > 0\}$ is not deterministic limit PA recognizable. The proof is similar to the proof of Theorem 3 of (the arXiv version of) <cit.>.
Assume there is an $n$-state deterministic limit PA $\Amc$ recognizing $L$. Consider the unique non-accepting run of $\Amc$ on $a (a^n b^n)^\omega$.
Observe that $\Amc$ visits at least one state twice while reading a $b^n$-block, and there are at least two of the (infinitely many)  such that $\Amc$ visits the same state, say $q$, twice while reading them. Hence, we can shift one such  to the front and obtain the unique run on an infinite word that is in $L$. However, this run is still non-accepting, as the extended Parikh image and number of visits of an accepting state do not change.

Deterministic reach PA $\not\subseteq$ deterministic strong reset PA.

We show that the deterministic reach PA recognizable $\omega$-language $L = \{a^n b^n \mid n \geq 1\} \cdot \{a,b\}^\omega$ is not deterministic strong reset PA recognizable. Assume there is a deterministic strong reset PA $\Amc$ with $n$ states recognizing $L$. Let $\alpha = a^n b^\omega$ with unique accepting run $r = r_1 r_2 r_3 \dots$ of $\Amc$ on $\alpha$.
Let $f_1, f_2, \dots$ be the sequence of reset positions of $r$ and let $i > n$ be minimal such that $i = f_{i'}$ for some $i' \geq 1$ (that is, $f_{i'}$ is the first reset position after reading a $b$).

First observe that $i < 2n$. Assume that this is not the case. As $\Amc$ visits at least one state twice while reading $b^n$, say state $q$, we observe that $\Amc$ is caught in a $q \dots q$ cycle while reading $b^\omega$ due to determinism. That is, every state that is visited while reading $b^\omega$ is already visited while reading the first $n$ many $b$s. Hence we have $i < 2n$.
Now let $j \geq 2n$ be minimal such that $j = f_{j'}$ for some $j' > i'$ is a reset position in $r$ such that the state at position $f_{j'}$ is the same state as the one at position $f_{i'}$ (which exists by the same argument).

Now let $\alpha' = a^n b^{j-n}a^\omega$ with unique accepting run $r' = r'_1 r'_2 r'_3 \dots$ of $\Amc$ on $\alpha'$.
Observe that $\alpha[1:j] = \alpha'[1:j]$, and hence $r[1:j] = r'[1:j]$.
As the partial runs $r[1:i]$ and $r[1:j]$ reach the same accepting state, the run $r[1:i]r'_{j+1}r'_{j+2} \dots$ is an accepting run of $\Amc$ on $a^n b^{i-n} a^\omega$.
However, as $i-n < n$, this infinite word is not contained in $L$, a contradiction.

§.§ Deterministic Reach-Reg PA

We begin by showing that the every deterministic reach-reg. PA (and hence every deterministic reach PA) can be translated into an equivalent deterministic weak reset PA.

Deterministic reach-reg. PA $\subsetneq$ deterministic weak reset PA.

Let $\Amc = (Q, \Sigma, q_0, \Delta, F, C)$ be a det. reach-reg. PA. Let $\Amc' = (Q \cup \{q_0'\}, \Sigma, q_0', \Delta', F, C')$ be a copy of $\Amc$ with a new fresh initial state $q_0'$ inheriting all outgoing transitions of $q_0$ (observe that this modification preserves determinism). We add one new counter that is incremented at every transition leaving $q_0'$, and not modified otherwise, that is,

\begin{align*}
\Delta' =&\ \{(p, a, \vbf \cdot 0, q) \mid (p, a, \vbf, q) \in \Delta\} \\
\cup&\ \{(q_0', a, \vbf \cdot 1, q) \mid (q_0, a, \vbf, q) \in \Delta\}.
\end{align*}

We choose $C' = C \cdot \{1\} \cup \Nbb^d \cdot \{0\}$ and obtain an equivalent weak reset PA $\Amc'$.

The strictness is witnessed by the $\omega$-language , which is obviously deterministic weak reset PA-recognizable, but not even recognized by (non-deterministic) Büchi PA, which are more expressive than reachability-regular PA <cit.>.

§.§ Deterministic Strong Reset PA

Deterministic strong reset PA $\subsetneq$ deterministic weak reset PA.

The inclusion follows by the same argument as in the non-deterministic setting <cit.> (we use an additional counter to force the weak reset PA to reset whenever an accepting state is visited).

The strictness follows from the fact that $\{a^n b^n \mid n \geq 1\} \cdot \{a,b\}^\omega$ is deterministic reach PA recognizable, and hence deterministic weak reset PA recognizable (by <Ref> and <Ref>), but not recognized by any deterministic strong reset PA, as shown in <Ref>.

Deterministic strong reset PA $\not\subseteq$ deterministic Büchi PA.

The argument is as in <Ref>. The $\omega$-language $\{a^n b^n \mid n > 0\}^\omega$ is deterministic strong reset PA recognizable, but there is no Büchi PA recognizing it <cit.>.

Deterministic strong reset PA $\not\subseteq$ deterministic limit PA.

This follows from the previous proof as limit PA are less expressive than Büchi PA <cit.>.

§.§ Deterministic Büchi PA

We show that $\omega$-languages recognized by deterministic Büchi PA can be characterized in a similar way as deterministic $\omega$-regular languages.

An $\omega$-language $L$ is deterministic Büchi PA recognizable if and only of $L = \vec{P}$ where $P$ is recognized by a deterministic PA.

Let $\Amc$ be a deterministic Büchi PA recognizing $L$ and let $\alpha \in B_\omega(\Amc)$ with accepting run $r$. As $r$ has infinitely many accepting hits by definition, we have $\alpha \in \vec{L(\Amc)}$.
Similarly, let $\Amc$ be a deterministic PA recognizing $P$ and let $\alpha \in \vec{P}$. As $\Amc$ is deterministic, the unique run of $\Amc$ on $\alpha$ has infinitely many accepting hits, hence we have $\alpha \in B_\omega(\Amc)$.

Deterministic Büchi PA $\not\subseteq$ deterministic limit PA.

The proof is almost identical to the proof of <Ref>, but this time we consider the $\omega$-language $L_{a=b} = \{\alpha \mid |\alpha[1:i]|_a = |\alpha[1:i]|_b \text{ for $\infty$ many }i \}$. Then we can re-use the same argument as the constructed infinite word has indeed infinitely many balanced $a$-$b$ prefixes.

Deterministic Büchi PA $\not\subseteq$ deterministic weak reset PA.

Let $L_{a=b}$ be as in the last proof and similarly define $L_{a=c} = \{\alpha \mid |\alpha[1:i]|_a = |\alpha[1:i]|_c \text{ for $\infty$ many }i \}$.
We show that the deterministic Büchi PA recognizable $\omega$-language $L_{a=b} \cup L_{a=c}$ is not deterministic weak reset PA recognizable.
Assume there is a deterministic weak reset PA $\Amc$ recognizing $L_{a=b} \cup L_{a=c}$. Consider the unique accepting run $r$ of $\Amc$ on $\alpha = (ab)^\omega$ and let $i,j$ be two positions with $i+1 < j$ such that $r$ resets after reading $\alpha[1:i]$ and $\alpha[1:j]$ in the same state (such a pair of positions does always exists by the infinite pigeonhole principle).
Now consider the infinite word $\alpha[1:i] c^{|\alpha[1:i]|_a} (ac)^\omega$, which is also accepted by $\Amc$. However, this implies that $\Amc$ also accepts $\alpha[1:j] c^{|\alpha[1:i]|_a} (ac)^\omega$, as $\Amc$ is in the same (accepting) state after reading $\alpha[1:i]$ as well as $\alpha[1:j]$, but this infinite word is not contained in $L_{a=b} \cup L_{a=c}$, as $\alpha[1:j]$ contains at least one more $a$ than $\alpha[1:i]$, a contradiction.

We note however that the class of $\omega$-languages recognized by deterministic Büchi PA with a linear set form a subclass of the class of $\omega$-languages recognized by deterministic weak reset PA with a linear set, as clarified in the following lemma.

Let $\Amc$ be a deterministic Büchi PA with a linear set $C(\bbf, P)$. Then there is an equivalent deterministic weak reset PA.

First we observe that if $\bbf = \0$, then we have $B_\omega(\Amc) = WR_\omega(\Amc)$. To see this, let $\alpha \in B_\omega(\Amc)$ with (unique) accepting run $r$. By Dickson's Lemma <cit.>, the run $r$ contains an infinite monotone sequence $s_1 < s_2 < \dots$ of accepting hits, that is, for all $i \geq 0$ we have $\rho(r[1:s_i]) \in C(\bbf , P)$ and for all $j > i$ we have $\rho(r[s_i+1: s_j]) \in C(\bbf, P)$. Hence, the run $r$ also satisfies the weak reset condition.
For the other direction let $\alpha \in WR_\omega(\Amc)$ with (unique) accepting run $r$ and reset positions $0 = k_0 < k_1 < k_2 \dots$. As we assume $\bbf = \0$, it is immediate that $\rho(r[1:k_i]) \in C(\bbf, P)$ for all $i \geq 1$. Hence, the run $r$ also satisfies the Büchi condition.

Finally we argue that we can always assume that $\bbf = \0$. Indeed, we can always encode $\bbf$ into the state space of $\Amc_1$.

§ CLOSURE PROPERTIES

We study the closure properties of the deterministic variants of the models introduced by Grobler et al. <cit.>, that is, deterministic limit PA, deterministic reachability-regular PA, deterministic strong reset PA, and deterministic weak reset PA.

It is well known that semi-linear sets over $\Nbb^d$ are closed under complement <cit.>.
Before we study deterministic limit automata we show that this is also true for semi-linear sets enriched with $\infty$.

Let $C \subseteq \Nbbinfty^d$ be a semi-linear set. Then the complement $\bar{C} = \Nbbinfty^d \setminus C$ is semi-linear.

Let $f : \Nbbinfty \rightarrow\Nbb$ be the bijection with $f(\infty) = 0$ and $f(i) = i+1$ for $i \in \Nbb$.
We extend $f$ to vectors  and sets of vectors $C \subseteq \Nbbinfty^d$ component-wise: $f(v_1, \dots, v_d) = (f(v_1), \dots, f(v_d))$ and $f(C) = \{f(\vbf) \mid \vbf \in C\}$. Note that .

Now we observe that $f(C)$ is semi-linear if and only if $C$ is semi-linear. First assume that $C$ is semi-linear. We may assume that $C = C(\bbf, P)$ is linear, as we can carry out the following procedure for every linear set individually. Assume $\bbf = (b_1, \dots, b_d)$. We define $D_\infty(\bbf) = \{i \mid b_i = \infty\}$.
For a set $D \subseteq \{1, \dots, d\}$ with $D_\infty(\bbf) \subseteq D$ and a vector $\vbf = (v_1, \dots, v_d) \in \Nbbinfty^d$, let $\vbf^D = (v_1^D, \dots, v_d^D)$ with $v_i^D = 0$ if $i \in D$ and $v_i^D = v_i$ if $i \notin D$.
Furthermore, we call a subset $P' \subseteq P$ of period vectors $D$-compatible if for every $i \in D \setminus D_\infty(\bbf)$, the set $P'$ contains at least one vector where the $i$th component is $\infty$, and if for every $i \notin D$, the set $P'$ contains no vector where the $i$th component is $\infty$.
Observe that this definition ensures that for every vector $\vbf \in P'$ we have $\vbf^D \in \Nbb^d$, that is, no component in $\vbf^D$ is $\infty$.
Let $\Pmc^D_\infty \subseteq 2^P$ be the collection of $D$-compatible subsets of $P$.

Then we have $f(C) = \bigcup_{D_\infty(\bbf) \subseteq D \subseteq \{1, \dots, d\}} \bigcup_{P' \in \Pmc^D_\infty} C(\bbf^D + \1^D + \sum_{\pbf \in P'} \pbf^D, \{\pbf^D \mid \pbf \in P'\})$,
which is semi-linear by definition.

For the other direction, we may again assume that $f(C) = C(\bbf, P)$ is linear.
Similar to above, assume $\bbf = (b_1, \dots, b_d)$ and define $D_0(\bbf) = \{i \mid b_i = 0\}$.
For a set $D \subseteq D_0(\bbf)$ we call a subset $P' \subseteq P$ of period vectors $D$-safe if for every $i \in D$ the set $P'$ contains no vector where the $i$th component is not 0, and if for every $i \notin D$ the set $P'$ contains at least one vector where $i$th component is not 0.
Let $\Pmc^D_0 \subseteq 2^P$ be the collection of $D$-safe subsets of $P$.

Let $\ibf_D = (v_1, \dots, v_d)$ with $v_i = \infty$ if $i \in D$ and $v_i = 0$ if $i \notin D$.
Then we have $C = \bigcup_{D \subseteq D_0(\bbf)} \bigcup_{P' \in \mathcal{P}^D_0} C(\ibf_D + \bbf - \1 + \sum_{\pbf \in P'} \pbf, P')$, which is semi-linear by definition (observe that every component in $\ibf_D + \bbf + \sum_{\pbf \in P'} \pbf$ is strictly greater 0, hence we can subtract $\1$ without getting negative; furthermore, we assume $\infty-1=\infty$).

As semi-linear sets over $\Nbb^d$ are closed under complement, we have $C$ is semi-linear iff $f(C)$ is semi-linear iff $\Nbb^d \setminus f(C)$ is semi-linear iff $f^{-1}(\Nbb^d \setminus f(C)) = \bar{C}$ is semi-linear.

The class of deterministic limit PA recognizable languages is closed under union, intersection and complement.

First observe that we can always assume that every state of a (deterministic) limit PA is accepting, as we can check the existence of an accepting state being visited infinitely often in the semi-linear set. To achieve this, we introduce one new counter and increment it at every transition that points to an accepting state. In the semi-linear set we enforce that this counter is $\infty$.

Hence, we can show the closure under union and intersection by a standard product construction. In case of union, we test whether at least one automaton has good counter values, and we can show the closure under intersection by testing whether both automata have good counter values.

Closure under complement follows immediately from <Ref>.

The class of deterministic reach-reg.P̃A recognizable languages is not closed under union, intersection or complement.

First we show non-closure under union.

$$L_1 = \{u c \alpha \mid u \in \{a,b,c\}^*, |u|_a = |u|_b, |\alpha|_c = \infty\}$$

$$L_2 = \{v a \beta \mid v \in \{a,b,c\}^*, |v|_b = |v|_c, |\beta|_a = \infty\}.$$

Both languages are deterministic reach-reg. PA recognizable, as witnessed by the automaton in <Ref> and the fact that $L_2$ can be obtained from $L_1$ by shuffling symbols.
We show that the language $L_1 \mathop{\cup} L_2$ is not deterministic reach-reg. PA recognizable.
Assume there is an $n$-state deterministic reach-reg. PA $\Amc$ recognizing $L$.
Then there is a unique accepting run $r_1 r_2 \dots$ of $\Amc$ on $abc^\omega$. In particular, at some point the automaton verifies the Parikh condition, say after using the transition $r_i$. Let $m = \max\{n+1, i\}$ and consider the infinite word $abc^m b^{m-1} a^\omega$
with the unique accepting run $r'_1 r'_2 \dots$ of $\Amc$. Due to determinism, we have $r_j = r'_j$ for all $j \leq m+2$; in particular, the automaton verifies the Parikh condition within this run prefix. As $m-1 \geq n$, the automaton visits a state, say $q$ twice while reading $b^{m-1}$. Hence, we can pump this $q$-cycle and obtain an accepting run of $\Amc$ on $abc^m b^{m-1+k} a^\omega$ for some $k > 0$, a contradiction.

To show the non-closure under intersection, define $L_1 = \{\alpha \mid |\alpha[1:i]|_a = |\alpha[1:i]|_b \text{ for some }i \}$ and $L_2 = \{\alpha \mid |\alpha[1:i]|_a = |\alpha[1:i]|_c \text{ for some }i \}$.
Suppose there is an $n$-state deterministic reach-reg.  PA recognizing $L_1 \cap L_2$. Let $\alpha = a(a^n b^n)^{n+1} c^{n(n+1) + 1} a^\omega$. The unique run $r$ of $\Amc$ on $\alpha$ is not accepting, as $\alpha$ has no balanced $a$-$b$ prefix.
Observe that $\Amc$ visits at least one state twice while reading a $b^n$-block.
Furthermore, there is a state, say $q$, such that $\Amc$ visits $q$ twice while reading two different $b^n$-blocks, as there are $n+1$ different $b^n$-blocks.
Hence, we can swap the latter $q$-cycle to the front and obtain an infinite word, say $\alpha'$ in $L_1 \cap L_2$, with a unique accepting run $r'$ of $\Amc$. This run verifies the Parikh condition at some point. We distinguish two cases.
If $r'$ verifies the Parikh condition before reading the first $c$, we can depump the $c^{n(n+1)+1}$-block and obtain an accepting run on an infinite word without a balanced $a$-$c$-prefix, a contradiction.
Hence assume that $r'$ verifies the Parikh condition after reading at least one $c$, say at position $k$. However, then we have $\rho(r[1:k]) = \rho(r'[1:k])$, and hence $\Amc$ also accepts $\alpha$, a contradiction.

The non-closure under complement is witnessed by $L_{a<\infty}$, see <Ref>.

[->,>=stealth',shorten >=1pt,auto,node distance=3.5cm, semithick]
every state=[minimum size=1cm]

[state, initial, initial text=] (q0) $q_0$;
[state, accepting] (q1) [right of=q0] $q_1$;

(q0) edge [loop above, align=center] node $a, \begin{pmatrix}1\\0\end{pmatrix};$  $b, \begin{pmatrix}0\\1\end{pmatrix}$ (q0)
(q0) edge [bend left]  node $c, \0$ (q1)
(q1) edge [loop above] node $c, \0$ (q1)
(q1) edge [bend left, align=center] node $a, \begin{pmatrix}1\\0\end{pmatrix}$;  $b, \begin{pmatrix}0\\1\end{pmatrix}$ (q0)

The deterministic reach-reg.  PA with $C = C(\0, \{\1\})$ for $L_1 = \{u c \alpha \mid u \in \{a,b,c\}^*, |u|_a = |u|_b, |\alpha|_c = \infty\}$.

The class of deterministic weak reset PA recognizable languages is not closed under union, intersection or complement.

We begin with the non-closure under union. The $\omega$-languages
$L_{a=b}$ and $L_{a=c}$ (as defined in <Ref>) are both deterministic weak reset PA recognizable. As shown in <Ref>, their union is not.

The argument for the non-closure under intersection is the same as for the non-deterministic setting <cit.>, which follows from <cit.> and <cit.>: Let $L_{2a = b} = \{\alpha \mid 2|\alpha[1:i]|_a = |\alpha[1:i]|_b \text{ for $\infty$ many }i \}$. Then $L_{a=b} \cap L_{2a = b}$ is not even ultimately periodic, and hence not recognized by any weak reset PA, as they only recognize ultimately periodic $\omega$-languages <cit.>.

The non-closure under complement is again witnessed by $L_{b < \infty}$, see <Ref>.

The class of deterministic strong reset PA recognizable languages is not closed under union, intersection or complement.

We begin with the non-closure under union. Let $L = \{c^* a^n c^* b^n \mid n > 0\}^\omega$ and $L_{c=\infty} = \{\alpha \mid |\alpha|_c = \infty\}$.
Observe that $a^n c^\omega \in L \cup L_{c=\infty}$ for every $n \geq 0$.
Assume there is a deterministic strong reset PA recognizing $L \cup L_{c=\infty}$. Let $n_1 \neq n_2$ be such that the unique accepting runs of $\Amc$ on $\alpha_1 = a^{n_1} c^\omega$ resp. $\alpha_2 = a^{n_2} c^\omega$ reset in the same state the first time they reset after reading at least one $c$, say after reading $\alpha_1[1:i_1]$ resp. $\alpha_2[1:i_2]$ (with $i_1 > n_1$ and $i_2 > n_2$).
As $a^{n_1} c^{n_1-i_1} b^{n_1} (ab)^\omega$ is also accepted by $\Amc$, the infinite word $a^{n_2} c^{n_2 - i_2} b^{n_1} (ab)^\omega$ is also accepted by $\Amc$, a contradiction.

To show the non-closure under intersection, we use an argument similar to the non-deterministic setting. Let  and $L_2 = \{a\} \{b^n a^{2n} \mid n > 0\}$. Then $L_1 \cap L_2$ contains only one infinite word, namely $ab a^2 b^2 a^4 b^4 \dots$. Hence $L_1 \cap L_2$ is not ultimately periodic and hence not accepted by any strong reset PA <cit.>.

The non-closure under complement again follows from <Ref>.

Finally we remark that deterministic reach-reg.  PA, deterministic limit PA, deterministic strong reset PA and deterministic weak reset PA are strictly weaker than their non-deterministic counterparts. This follows immediately from their different closure properties: reach-reg.  PA, weak reset PA (and hence strong reset PA) are closed under union, and limit PA are not closed under complement <cit.>. The authors do not explicitly mention that limit PA are not closed under complement. This however follows from their characterization of limit PA and the fact (non-deterministic finite word) PA are not closed under complement <cit.>.

§ DECISION PROBLEMS AND MODEL CHECKING

§.§ Decision Problems

In this section, we consider the following decision problems for PA on infinite words.

* Emptiness: given PA $\Amc$, is the $\omega$-language of $\Amc$ empty?

* Membership: given PA $\Amc$ and finite words $u, v$, does $\Amc$ accept $uv^\omega$?

* Universality: given PA $\Amc$, does $\Amc$ accept every infinite word?

Emptiness for deterministic limit PA, deterministic reach-reg. PA, deterministic weak reset PA and deterministic strong reset PA is $\coNP$-complete.

Containment in $\coNP$ for all models is witnessed by the fact that testing non-emptiness for non-deterministic reset PA is in , and that they generalize all of these models (this follows immediately from <cit.>).

Hardness is very similar to the finite word case <cit.>, as we can reduce subset sum to non-emptiness for all of these models.

Membership for deterministic limit PA, deterministic reach-reg. PA, deterministic weak reset PA and deterministic strong reset PA is $\NP$-complete.

As membership for the non-deterministic counterparts of these models is in $\NP$ <cit.>, the upper bound follows immediately.

Hardness follows from a simple reduction from the membership problem for semi-linear sets, that is the question, given a semi-linear set $C \subseteq \Nbb^d$ and a vector $\vbf \in \Nbb^d$, is $\vbf \in C$? This problem is known to be $\NP$-complete <cit.>.

Universality for deterministic limit PA and deterministic strong reset PA is decidable, while universality for deterministic reach-reg. PA and deterministic weak reset PA is undecidable.

The decidability result for deterministic limit PA follows from the fact that a (deterministic limit) PA $\Amc$ is universal if and only if $\overline{L_\omega(\Amc)}$ is empty. Now, deterministic limit PA are closed under complement by <Ref> and emptiness is decidable by <Ref>.

In contrast Guha et al. have shown that universality is already undecidable for deterministic reach PA <cit.>. Hence, the undecidability for deterministic reach-reg. PA and deterministic weak reset PA follows from <Ref>.

Finally we show that universality for deterministic strong reset PA is decidable by reducing it to checking emptiness of the complement $\omega$-language. Let $\Amc$ be a deterministic strong reset PA. Observe that $\Amc$ rejects an infinite word $\alpha$ whenever one of the following two conditions is met:

* The unique run of $\Amc$ on $\alpha$ visits every accepting state just finitely often.

* The unique run of $\Amc$ on $\alpha$ visits once an accepting state with bad counter values.

The first condition is $\omega$-regular, while the second one can be tested using reach PA. As the union of an $\omega$-regular language and a reach PA recognizable language is recognized by a reach-reg. PA, for which emptiness is decidable <cit.>, we obtain the desired result.

Let us begin be showing how a reach PA can test whether a deterministic strong reset PA $\Amc$ rejects at least one infinite word $\alpha$ because the unique run $r$ of $\Amc$ on $\alpha$ reaches an accepting state with bad counter values. Let $\Amc = (Q, \Sigma, q_0, \Delta, F, C)$ and assume that every state in $\Amc$ is reachable from the initial state (otherwise they can safely be removed), and that $q_0 \notin F$ (this can be done by adding a fresh initial state while preserving determinism).
Say $r = r_0 r_1 r_2 \dots$ and $0 = k_0 < k_1 < k_2 \dots$ are the reset positions. Given that $k_0, k_1, k_2 \dots$ is an infinite sequence, there is $j \geq 0$ such that the partial run $r_{k_j+1} \dots r_{k_{j+1}}$ collects a vector not in $C$. We re-use the following idea from <cit.>. For any two states $p, q \in Q$ let $\Amc_{p \Rightarrow q} = (Q \cup \{q_0'\}, \Sigma, q_0', \Delta_{p \Rightarrow q}, \{q\}, C)$ where $\Delta_{p \Rightarrow q} = \{(q_1, a, \vbf, q_2) \mid (q_1, a, \vbf, q_2) \in \Delta, q_1 \notin F) \cup \{(q_0', a, \vbf, q_2) \mid (p, a, \vbf, q_2) \in \Delta\}$.
Hence, if we interpret $\Amc_{p\Rightarrow q}$ as a finite word PA, then it accepts words all accepted by the finite word PA $\Amc$ when starting in $p$, ending in $q$, and not visiting an accepting state in-between. In other words, if $p,q\in F$, then $\Amc_{p \Rightarrow q}$ accepts all finite infixes that the strong reset PA $\Amc$ may read when the last reset was in $p$, and the next reset is in $q$.
Now let $\bar{\Amc}_{p \Rightarrow q}$ be defined as $\Amc_{p \Rightarrow q}$, but $C$ is complemented. Consider for all $p, q \in F$ the finite-word PA $\bar{\Amc}_{p \Rightarrow q}$. If at least one of these PA accepts at least one word, then the strong reset PA $\Amc$ is not universal.
To see this, assume that $\bar{\Amc}_{p \Rightarrow q}$ accepts a word $w \in \Sigma^*$.
Furthermore, let $v \in \Sigma^*$ be an arbitrary word such that (the unique run of) $\Amc$ is in state $p$ after reading $v$. As $p$ is an accepting state which enforces a reset, the counters of $\Amc$ are all $0$ after reading $v$.
Now, if we feed $w$ to $\Amc$, the automaton reaches the accepting state $q$ (without seeing any other accepting state in between by the definition of $\bar{\Amc}_{p\Rightarrow q}$), and hence rejects at this point, as the counter values are bad.
Hence, $\Amc$ rejects any infinite word with prefix $vw$, and is hence not universal.

Hence, for every $p, q \in F$ we construct a (non-deterministic) reach PA that accepts all infinite words of the form $vw \Sigma^\omega$ such that $\Amc$ is in state $p$ after reading $v$ (there might be several resets before reaching $p$), and $w \in L(\bar{\Amc}_{p \Rightarrow q})$. Finally, we build the union of all these automata for all $p, q \in F$ and obtain a reach PA $\Amc_\cup$ whose $\omega$-language is not empty if and only if there is an infinite word such that the unique run of $\Amc$ visits an accepting state with bad counter values (Condition 2 of the list above).

Let $\Bmc$ be the Büchi automaton obtained from $\Amc$ by forgetting all vectors and let $\overline{\Bmc}$ be a Büchi automaton recognizing the complement of $L_\omega(\Bmc)$.

Then $\Amc$ is universal if and only if $R_\omega(\Amc_\cup) \cup L_\omega(\overline{\Bmc})$ is empty, which can be tested by turning both automata into reach-reg. PA, which are trivially closed under union <cit.>.

§.§ Model Checking

In the classical model checking problem, we are given a system $\Kmc$ and a specification, e.g. represented as an automaton $\Amc$, and the question is whether every run of $\Kmc$ satisfies the specification, , we ask $L(\Kmc) \subseteq L(\Amc)$, which can be equivalently written as $L(\Kmc) \cap \overline{L(\Amc)} = \varnothing$.
However, as complementing is often expensive or not even possible, another approach is to specify the set of all bad runs and ask whether no run of $\Kmc$ is bad, which boils down to the question is $L(\Kmc) \cap L(\Amc) = \varnothing$?
We call the first approach universal model checking and the latter approach existential model checking.
In our setting we assume the specification $\Amc$ to be a PA operating on infinite words, while the system $\Kmc$ may be given as a Kripke-structure (which can be seen as a safety automaton <cit.>), in which case the goal is to solve safety model checking, or also as a PA operating on infinite words, in which case the goal is to solve PA model checking.
Hence, we consider four problems in total.

As shown in <cit.>, the existential safety model checking problem for almost all (non-deterministic variants of the) models considered in this paper is decidable in , the exception being safety PA and co-Büchi PA.

Existential safety model checking is -complete for reach PA, reach-reg.  PA, limit PA Büchi PA, strong reset PA, and weak reset PA.

Hence, this problem is also decidable in $\coNP$ for their deterministic variants. The matching lower-bounds follow from an easy reduction from their emptiness problems by asking whether $\Sigma^\omega \cap L(\Amc) = \varnothing$ (a safety automaton for $\Sigma^\omega$ is easily found).

Existential safety model checking is -complete for deterministic reach PA, deterministic reach-reg.  PA, deterministic limit PA Büchi PA, deterministic strong reset PA, and deterministic weak reset PA.

Guha et al. <cit.> have shown that emptiness is undecidable for deterministic safety PA and deterministic co-Büchi PA. Hence, their existential safety model checking problem is undecidable.

Existential safety model checking is undecidable for deterministic safety PA and deterministic co-Büchi PA.

Similarly, the universal model checking problems are undecidable for all models that already have an undecidable universality problem, as we can easily reduce from universality by asking whether $\Sigma^\omega \subseteq L(\Amc)$. Hence, we obtain the following corollary as an immediate consequence of <Ref> and the results in <cit.>.

Universal safety model checking and universal PA model checking are undecidable for deterministic reach PA, deterministic reach-reg.  PA, deterministic Büchi PA and deterministic weak reset PA.

Guha et al. <cit.> have shown that the universal PA model checking problem is decidable for deterministic safety PA and deterministic co-Büchi PA.
We note that this is also the case for deterministic limit PA, which follows from their closure properties.

Furthermore, we show that the universal PA model checking problem is decidable for deterministic strong reset PA.
As shown in <Ref>, the complement $\omega$-languages of deterministic strong reset PA are recognized by reach-reg. PA.
Hence, given two deterministic strong reset PA $\Amc_1, \Amc_2$, the question whether $SR_\omega(\Amc_1) \subseteq SR_\omega(\Amc_2)$ (which is equivalent to the question whether $SR_\omega(\Amc_1) \cap \overline{SR_\omega(\Amc_2)} = \varnothing$) boils down to deciding intersection emptiness of a deterministic strong reset PA and a reach-reg.  PA.

We first show that deciding intersection emptiness of a deterministic strong reset PA recognizable $\omega$-language and an $\omega$-regular language is decidable.
To achieve that, we begin by showing that the intersection of a deterministic strong reset PA recognizable $\omega$-language and an $\omega$-regular language is still ultimately periodic.

Let $\Amc = (Q_1, \Sigma, p_I, \Delta_1, F_1, C)$ be a deterministic strong reset PA and $\Bmc = (Q_2, \Sigma, q_I, \Delta_2, F_2)$ be a Büchi automaton. Then $SR_\omega(\Amc) \cap L_\omega(\Bmc)$ is ultimately periodic.

Assume $SR_\omega(\Amc) \cap L_\omega(\Bmc) \neq \varnothing$ and let $\alpha$ be an infinite word accepted by both automata, $\Amc$ and $\Bmc$.
If $\alpha = uv^\omega$ for some $u, v \in \Sigma^*$, we are done. Hence assume that this is not the case.
Let $\Amc = (Q_1 \times Q_2, \Sigma, (p_I, q_I), \Delta, F_1 \times Q_2, C)$ with $\Delta = \{((p, q), a, \vbf, (p', q')) \mid (p, a, \vbf, p') \in \Delta_1, (q, a, q') \in \Delta_2\}$ be the product automaton[We note that $\Amc$ interpreted as a strong reset PA does not recognize $SR_\omega(\Amc) \cap L_\omega(\Bmc)$. Instead, it accepts all infinite words $\alpha \in SR_\omega(\Amc)$ such that $\Bmc$ has an infinite but not necessarily accepting run on $\alpha$.] of $\Amc$ and $\Bmc$.
As $\alpha \in SR_\omega(\Amc)$, the unique accepting run $(p_0, \alpha_1, \vbf_1, p_1)$ $(p_1, \alpha_2, \vbf_2, p_2) \dots$ with $p_0 = p_I$ is accepting. Likewise, as $\alpha \in L_\omega(\Bmc)$, there is an accepting run $(q_0, \alpha_1, q_1) (q_1, \alpha_2, q_2) \dots$ with $q_0 = q_I$ of $\Bmc$ on $\alpha$.
Hence, $r = ((p_0, q_0), \alpha_1, \vbf_1, (p_1, q_1)) ((p_1, q_1), \alpha_2, \vbf_2, (p_2, q_2)) \dots$ is a run of $\Amc$ on $\alpha$
with the following properties:

* there is $p_f \in F_1$ such that for infinitely many $i$ we have $p_i = p_f$. Let $f_1, f_2, \dots$ denote the positions of all occurrences of a state of the form $(p_f, \cdot)$ in $r$.

* there is $q_f \in F_2$ such that for infinitely many $i$ we have $q_i = q_f$.

Let $j \geq f_1$ be minimal such that $q_j = q_f$.
Now let $k \leq j$ be maximal such that $k = f_\ell$ for some $\ell \geq 1$.
Then $r[1:f_\ell]r[f_\ell+1 : f_{\ell+1}]^\omega$ is an accepting run of $\Amc$ on an ultimately periodic word, say $uv^\omega$, that visits an accepting state of $\Bmc$ infinitely often. Hence $uv^\omega \in SR_\omega(\Amc) \cap L_\omega(\Bmc)$.

Let $\Amc$ be a deterministic strong reset PA and let $\Bmc$ be a Büchi automaton. The question $SR_\omega(\Amc) \cap L_\omega(\Bmc) = \varnothing$ is -complete.

Hardness is obvious; hence, we focus on the containment in .
By the previous lemma it is sufficient to check the existence of an ultimately periodic word.
Let $\Amc = (Q_1, \Sigma, p_0, \Delta_1, F_1, C)$ and $\Bmc = (Q_2, \Sigma, q_0, \Delta_2, F_2)$.
Recall the algorithm  that decides the non-emptiness problem for reset PA in $\NP$ by exploiting that every non-empty $\omega$-language accepted by a strong reset PA contains an ultimately periodic word.
This algorithm basically guesses an accepting state $p$ of $\Amc$ that is seen infinitely often, and a sequence of distinct accepting states $p_1 \dots p_n$ such that $p_i = p$ for some $i \leq n$.
Then, the algorithm tests for all $0 \leq i < n$ whether the finite word PA $\Amc_{p_i \Rightarrow p_{i+1}}$ accepts at least one word, and whether $\Amc_{p_n \Rightarrow p}$ accept at least one word (where $\Amc_{p\Rightarrow q}$ is defined as in the proof of <Ref>).
We modify the algorithm as follows.

First, let $\Amc$ be the product automaton of $\Amc$ and $\Bmc$ (as in the previous proof; however, the set of accepting states is not important for the algorithm).
We guess a state $q \in F_2$ that we expect to be seen infinitely often to satisfy the acceptance condition of $\Bmc$. Furthermore, similar to the algorithm above we guess a sequence of distinct states $(p_1, q_1) (p_2, q_2) \dots (p_n, q_n)$ such that for some $\ell \leq n$ we have $q_\ell = q$, for some $i \leq \ell$ we have $p_i = p$, and for all $j \neq \ell$ we have that $p_j$ is accepting in $\Amc$.
If the sequence contains a state $(p_i, q_i) \in F_1 \times F_2$, we can interpret $\Amc$ as a reset PA with accepting states $F_1 \times Q_2$ and run the algorithm, as the Büchi condition is automatically satisfied.

Hence assume that $p_\ell \notin F_1$ and $q_j \notin F_2$ for all $j \neq \ell$.
Let $\Amc_{p_{\ell-1} \stackrel{q_\ell}{\Rightarrow} p_{\ell +1}}$ be the finite word PA that accepts all finite infixes accepted by the product automaton $\Amc$ when starting in $(p_{\ell-1}, q_{\ell-1})$, visiting $(p_\ell, q_\ell)$ at some point, and ending in $(p_{\ell+1}, q_{\ell+1})$ such that for all internal states $(p_i, q_i)$ we have $p_i \notin F_1$.
Two achieve this, we take two copies of $\Amc$, where all accepting states in the first copy are not reachable, all accepting states in the second copy have no outgoing transitions, and the second copy can only be reached from the first copy via $(p_\ell, q_\ell)$.

Formally, let

$$\Amc_{p_{\ell-1} \stackrel{q_\ell}{\Rightarrow} p_{\ell +1}} = (Q_1 \times Q_2 \times \{1,2\} \cup \{q_0'\}, \Sigma, q_0', \Delta', \{(p_{\ell+1}, q_{\ell+1})\}, C)$$

\begin{align*}
\Delta' =&\ \{((p,q,1), a, \vbf, (p', q', 1)) \mid ((p,q), a, \vbf, (p', q')) \in \Delta, p, p' \notin F_1\} \\
\cup&\ \{((p,q,2), a, \vbf, (p', q', 2)) \mid ((p,q), a, \vbf, (p', q')) \in \Delta, p \notin F_1\} \\
\cup&\ \{((p,q,1), a, \vbf, (p_\ell, q_\ell, 2) \mid ((p, q), a, \vbf, (p_\ell, q_\ell)) \in \Delta \} \\
\cup&\ \{(q'_0, a, \vbf, (p', q', 1) \mid ((p_{\ell-1}, q_{\ell-1}), a, \vbf, (p', q' )) \in \Delta, p' \notin F_1 \} \\
\cup&\ \{(q'_0, a, \vbf, (p_\ell, q_\ell, 2) \mid ((p_{\ell-1}, q_{\ell-1}), a, \vbf, (p_\ell, q_\ell)) \in \Delta \}.
\end{align*}

Now the algorithm is similar to the original non-emptiness algorithm for reset PA. For every $0 \leq j < \ell-1$ and $\ell+1 \leq j < n$ we test $\Amc_{(p_j, q_j) \Rightarrow (p_{j+1}, q_{j+1})}$ as well as $\Amc_{(p_n, q_n) \Rightarrow (p_i, q_i)}$ for non-emptiness. Furthermore, we test $\Amc_{p_{\ell-1} \stackrel{q_\ell}{\Rightarrow} p_{\ell +1}}$ for non-emptiness.
If all these  accept at least one word, we conclude that , as the guess of our sequence implies that at least one accepting state of $\Bmc$ is seen infinitely often, while the rest follows from the correctness of the algorithm in <cit.>.

In order to show that testing intersection emptiness of a deterministic strong reset PA and a reach-reg. PA is decidable, we combine the algorithm in the previous proof with the -algorithm in <cit.> deciding the reachability problem for $\Zbb$-$\mathsf{VASS}$ with $k$ nested zero-tests ($\Zbb$-$\mathsf{VASS}^\mathsf{nz}_k$).
A $\Zbb$-$\mathsf{VASS}^\mathsf{nz}_k$ (of dimension $d \geq 1$) is a tuple $V = (Q, Z, E)$ where $Q$ is a finite set of states,
$Z \subseteq \{0, 1, \dots, d\}$ is its set of zero tests with $|Z \setminus \{0\}| = k$, and $E \subseteq Q \times \Zbb^d \times Z \times Q$ is a finite set of transitions.
A configuration of $V$ is a pair $(p, \vbf) \in Q \times \Zbb^d$. Assume $\vbf = (v_1, \dots, v_d)$. We write $(p, \vbf) \vdash_V (p', \vbf')$ if there is a transition $(p, \ubf, \ell, p') \in E$ such that $\vbf' = \vbf + \ubf$ and $v_1 = \dots = v_\ell = 0$. Furthermore, we write $(p, \vbf) \vdash^*_V (p', \vbf')$ if there is a sequence $(p_1, \vbf_1) \vdash_V \dots \vdash_V (p_n, \vbf_n)$ for some $n \geq 1$ such that $(p, \vbf) = (p_1, \vbf_1)$ and $(p', \vbf') = (p_n, \vbf_n)$. The reachability problem for $\Zbb$-$\mathsf{VASS}^\mathsf{nz}_k$ is defined as follows: given a $\Zbb$-$\mathsf{VASS}^\mathsf{nz}_k$ $V$ and two configurations $(p, \vbf), (p', \vbf')$, does $(p, \vbf) \vdash_V^* (p', \vbf')$ hold? As shown in <cit.>, this problem is $\NP$-complete[We note that our definition of $\Zbb$-$\mathsf{VASS}^\mathsf{nz}_k$ differs slightly from the definition in <cit.>, as we allow $E\subseteq Q\times \Zbb^d\times Z\times Q$ instead of $E\subseteq Q\times \{-1,0,1\}^d\times Z \times Q$ only. However, this difference does not change the mentioned complexity for the reachability problem <cit.>, see also <cit.>.] for any fixed $k$.

Let $\Amc_1$ be a deterministic strong reset PA and let $\Amc_2$ be a reach-reg. PA. The question $SR_\omega(\Amc_1) \cap RR_\omega(\Amc_2) = \varnothing$ is $\coNP$-complete.

Let $\Amc_1 = (Q_1, \Sigma, p_0, \Delta_1, F_1, C)$ be of dimension $d_1$ and $\Amc_2 = (Q_2, \Sigma, q_0, \Delta_2, F_2, D)$ of dimension $d_2$.
By <cit.> we can write $RR_\omega(\Amc_2)$ as $\bigcup_i U_i V_i^\omega$, where the $U_i$ are finite word PA languages, and $V_i$ are regular languages (in fact, the number of sets in the union is polynomially bounded by $|Q_2|$ and we can compute automata for these languages in polynomial time).

The idea for the proof of the lemma is as follows. Suppose $SR_\omega(\Amc_1) \cap RR_\omega(\Amc_2) \neq \varnothing$ and let $\alpha$ be an infinite word accepted by both automata.
We can write $\alpha = u \beta$ such that $u \in U_i$ for some $i$. Let $(p, \vbf) \in Q_1 \times \Nbb^{d_1}$ be the configuration of $\Amc_1$ after reading $u$ (as $\Amc_1$ is deterministic, there is a unique partial run of $\Amc_1$ on $u$, and as $\alpha = u\beta \in SR_\omega(\Amc_1)$, every visit of an accepting state while reading $u$ is with good counter values). Hence, if we can verify the existence of such a word $u$ and compute $(p, \vbf)$, we can use the algorithm in the previous lemma to test $SR(\Amc_1^{(p,\vbf)}) \cap L_\omega(\Bmc) \neq \varnothing$ where $\Amc_1^{(p,\vbf)}$ is defined as $\Amc_1$ but with initial configuration $(p, \vbf)$ (such a PA can be obtained from $\Amc_1$ by adding a fresh initial state that inherits all transitions from $p$ and adds $\vbf$ to them) and $\Bmc$ is a Büchi automaton for $V_i^\omega$.

In fact, we guess the existence of two finite words $u$ and $v$ such that (1) there is an infinite word $\beta$ with $uv\beta \in SR_\omega(\Amc_1) \cap RR_\omega(\Amc_2)$ (2) $u \in U_i$ for some $i$ and (3) the unique partial run of $\Amc_1$ is in an accepting state after reading $uv$, and every visit of an accepting state while reading $uv$ is with good counter values.
We verify (2) and (3) using the $\NP$-algorithm for the reachability problem for $\Zbb$-$\mathsf{VASS}^\mathsf{nz}_k$, yielding a deterministic strong reset PA $\Amc_1^{(p, \vbf)}$ for a configuration $(p, \vbf) \in Q_1 \times \Nbb^{d_1}$ and a Büchi automaton $\Bmc$ as described above, which we use to call the algorithm in the previous lemma.
To be precise, we build a product $\Zbb$-$\mathsf{VASS}^\mathsf{nz}_2$ $V$ with $d_1 + d_2$ many counters. This system works in two phases: in the first phase it tests the existence of $u$ ensuring that every visit of an accepting state of $\Amc_1$ is with good counter values using a zero test on the first $d_1$ counters. After finding such a $u$, the system transitions into the second phase in which the last $d_2$ counters are not modified any more, and we check the existence of a $v$ as mentioned above. After this check all counter are $0$.

Let us give some more details on how to verify that every visit of an accepting state implies good counter values. Let $C = C(\bbf_1, P_1) \cup \dots \cup C(\bbf_k, P_k)$ for some $k \geq 1$.
For every accepting state $f \in F_1$ we insert $k$ states, say $f^{(1)}, \dots, f^{(k)}$, and a copy of $f$ itself. We connect $f$ to $f^{(i)}$ with a transition with update $-\bbf_i$ and no zero-test.
Then, for every period vector $\pbf_i \in P_i$, we insert a loop on $f^{(i)}$ with update $-\pbf_i$.
Finally, every outgoing transition of $f^{(i)}$ is equipped with a zero-test on the first $d_1$ counters.
This construction allows us to test membership of the current counter values in $C$, while resetting the counters in parallel.

Let $D = C(\cbf_1, R_1) \cup \dots \cup C(\cbf_\ell, R_\ell)$ for some $\ell \geq 1$.
Formally, we define $V = (Q,\{0, d_1, d_1+d_2\},E)$ where

\begin{align*}
Q = Q_1 \times Q_2 \times \{1,2\} & \cup \{f^{(i)} \mid f \in F_1, i \leq k\} \\
& \cup \{c_{f,q}^{(i)}, d_{f,q}^{(j)}, e_{f,q} \mid f \in F_1, q \in Q_2, i \leq k, j \leq \ell\}
\end{align*}

\begin{align*}
E =&\ \{((p,q,1), \ubf \cdot \vbf, 0, (p',q',1)) \mid \\ & \qquad \exists a \in \Sigma: (p,a,\ubf,p') \in \Delta_1, (q,a,\vbf,q') \in \Delta_2, p \notin F_1 \} \\
\cup&\ \{((p,q,2), \ubf \cdot \0, 0, (p',q',2)) \mid \\ & \qquad \exists a \in \Sigma\, \exists v \in \Nbb^{d_2}: (p,a,\ubf,p') \in \Delta_1, \\& \qquad \qquad(q,a,\vbf,q') \in \Delta_2, p \notin F_1 \} \\
\cup&\ \{((f, q, 1), -\bbf_i \cdot \0, 0, (f^{(i)}, q)) \mid f \in F_1, q \in Q_2, i \leq k\} \\
\cup&\ \{((f^{(i)},q), -\pbf_i \cdot \0, 0, (f^{(i)}, q)) \mid \\ & \qquad f \in F_1, q \in Q_2, \pbf_i \in P_i, i \leq k\} \\
\cup&\ \{((f^{(i)},q), \ubf \cdot \vbf, d_1, (p', q', 1)) \mid \\ & \qquad \exists a \in \Sigma: (f,a,\ubf,p') \in \Delta_1, (q,a,\vbf,q') \in \Delta_2, \\ &\qquad \qquad f \in F_1, i \leq k\} \\
\cup&\ \{((p,g,1), \ubf \cdot \0, 0, (p', q', 2)) \mid \\ & \qquad \exists a \in \Sigma\, \exists v \in \Nbb^{d_2}: (p,a,\ubf,p') \in \Delta_1, (g,a,\vbf,q') \in \Delta_2, \\ &\qquad \qquad p \notin F_1, g \in F_2\} \\
\cup&\ \{((f^{(i)},g,1), \ubf \cdot \0, d_1, (p', q', 2)) \mid \\ & \qquad \exists a \in \Sigma\, \exists v \in \Nbb^{d_2}: (f,a,\ubf,p') \in \Delta_1, (g,a,\vbf,q') \in \Delta_2, \\ & \qquad \qquad f \in F_1, g \in F_2, i \leq k\} \\
\cup&\ \{((f, q, 2), -\bbf_i \cdot \0, 0, c_{f,q}^{(i)}) \mid f \in F_1, q \in Q_2, i \leq k\} \\
\cup&\ \{(c_{f,q}^{(i)}, -\pbf_i \cdot \0, 0, c_{f,q}^{(i)}) \mid f \in F_1, q \in Q_2, \pbf_i \in P_i, i \leq k\} \\
\cup&\ \{(c_{f,q}^{(i)}, \0 \cdot -\cbf_j, 0, d_{f,q}^{(j)}) \mid f \in F_1, q \in Q_2, i \leq k, j \leq \ell\} \\
\cup&\ \{(d_{f,q}^{(j)}, \0 \cdot -\rbf_j, 0, d_{f,q}^{(j)}) \mid f \in F_1, q \in Q_2, \rbf_j \in R_j, j \leq\ell\} \\
\cup&\ \{(d_{f,q}^{(j)}, \0, d_1+d_2, e_{f,q}) \mid f \in F_1, q \in Q_2, j \leq \ell\}.
\end{align*}

Observe that $V$ is computable in polynomial time.

We are now ready to present an $\NP$-algorithm deciding whether $SR_\omega(\Amc_1) \cap RR_\omega(\Amc_2) \neq \varnothing$.

* Guess $f \in F_1$ and $q \in Q_2$.

* Construct $V$ as above and test $((p_0, q_0, 1), \0) \vdash_V^* (e_{f,q}, \0)$.

* Finally, use the algorithm in the previous lemma to test $SR_\omega(\Amc_1^{f,\0}) \cap L_\omega(\Bmc_q) \neq \varnothing$, where $\Bmc_q$ is the Büchi automaton obtained from $\Amc_2$ by forgetting all vectors (and dropping $C_2$), and setting $q$ as its initial state.

If all tests succeed, we conclude that the intersection of $SR_\omega(\Amc_1)$ and $RR_\omega(\Amc_2)$ is not empty.

Universal safety model checking and universal PA model checking are decidable for deterministic limit PA and deterministic strong reset PA, deterministic safety PA and deterministic co-Büchi PA.

Recall that the existential PA model checking problem can equivalently be expressed as an intersection emptiness problem. As (non-deterministic) reach PA are closed under intersection and have a decidable emptiness problem, the existential PA model checking problem is decidable for them and hence also for their deterministic variants.
This is also the case for reach-reg. PA: they are equivalent to limit PA <cit.>, and we can show that limit PA are closed under intersection using the same argument as in the deterministic setting (see <Ref>).

To show that the existential PA model checking problem is decidable (even for non-deterministic) Büchi PA, we use a recent result essentially stating that Ramsey-quantifiers in Presburger formulas can be eliminated in polynomial time <cit.>. Furthermore, the authors show how to use the Ramsey-quantifier to check liveness properties for systems with counters. In particular, the existence of an accepting run of a Büchi PA (answering the question whether the accepted $\omega$-language is non-empty) can be expressed with a Presburger formula with a Ramsey-quantifier.
Hence, checking if the intersection of the two $\omega$-languages recognized by two Büchi PA can be tested by intersecting two Presburger-formulas and moving the quantifiers to the front. We refer to sections 4.1 and 8.2 in <cit.> for more information.

Existential PA model checking is decidable for (deterministic) reach PA, (deterministic) reach-reg. PA, (deterministic) limit PA, and (deterministic) Büchi PA.

We show that deciding whether the intersection of two $\omega$-lan-guages recognized by deterministic strong reset PA is empty is undecidable.
The result relies on the fact that the intersection of two such languages can encode non-terminating computations of two-counter machines.

A two-counter machine $\Mmc$ is a finite sequence of instructions

\[(1 : \Isf_1)(2 : \Isf_2) \dots (k-1 : \Isf_{k-1})(k : \mathsf{STOP})\]

where the first component of a pair $(\ell, \Isf_\ell)$ is the line number, and the second component is the instruction in line $\ell$.
An instruction is of one of the following forms:

* $\mathsf{Inc}(Z_i)$, where $i = 0$ or $i = 1$.

* $\mathsf{Dec}(Z_i)$, where $i = 0$ or $i = 1$.

* $\mathsf{If}\ Z_i = 0\ \mathsf{goto}\ \ell'\ \mathsf{else}\ \ell''$, where $i = 0$ or $i = 1$, and $\ell', \ell'' \leq k$.

Instructions of the first or second form are called increments resp. decrements, while instructions of the latter form are called zero-tests.
A configuration of $\Mmc$ is a tuple $c = (\ell, z_0, z_1)$, where $\ell \leq k$ is the current line number, and $z_0, z_1 \in \Nbb$ are the current counter values of $Z_0$ and $Z_1$ respectively. We say $c$ derives into its unique successor configuration $c'$, written $c \vdash c'$, as follows.

* If $\Isf_\ell = \mathsf{Inc}(Z_0)$, then $c' = (\ell + 1, z_0 + 1, z_1)$.

* If $\Isf_\ell = \mathsf{Inc}(Z_1)$, then $c' = (\ell + 1, z_0, z_1 + 1)$.

* If $\Isf_\ell = \mathsf{Dec}(Z_0)$, then $c' = (\ell + 1, \max\{z_0 - 1, 0\}, z_1)$.

* If $\Isf_\ell = \mathsf{Dec}(Z_1)$, then $c' = (\ell + 1, z_0, \max\{z_1 - 1, 0\})$.

* If $\Isf_\ell = \mathsf{If}\ Z_0 = 0\ \mathsf{goto}\ \ell'\ \mathsf{else}\ \ell''$, then $c' = (\ell', z_0, z_1)$ if $z_0 = 0$, and $c' = (\ell'', z_0, z_1)$ if $z_0 > 0$.

* If $\Isf_\ell = \mathsf{If}\ Z_1 = 0\ \mathsf{goto}\ \ell'\ \mathsf{else}\ \ell''$, then $c' = (\ell', z_0, z_1)$ if $z_1 = 0$, and $c' = (\ell'', z_0, z_1)$ if $z_1 > 0$.

* If $\Isf_\ell = \mathsf{STOP}$, then $c$ has no successor configuration.

The unique computation of $\Mmc$ is a finite or infinite sequence of configurations $c_0 c_1 c_2 \dots$ such that $c_0 = (1, 0, 0)$ and $c_i \vdash c_{i+1}$ for all $i \geq 0$.
Observe that the computation is finite if and only of the instruction $(k : \mathsf{STOP})$ is reached. If this is the case, we say $\Mmc$ terminates.
Given a two-counter machine $\Mmc$, it is undecidable to decide whether $\Mmc$ terminates or not <cit.>.

In the following we assume w.l.o.g. that our two-counter machines satisfy the guarded-decrement property <cit.> which guarantees that every decrement does indeed change a counter value: every decrement $(\ell : \mathsf{Dec}(Z_i))$ is preceded by a zero-test of the form $(\ell - 1, \mathsf{If}\ Z_i = 0\ \mathsf{goto}\ \ell+1\ \mathsf{else}\ \ell)$.
Note that this modification does not change the termination behavior of a two-counter machine, as decrementing a counter whose value is already zero does not have an effect.

The intersection emptiness problem for deterministic strong reset PA is undecidable.

We can encode infinite computations of two-counter machines as infinite words over $\Sigma = \{a,b, 1, 2, \dots, k\} \cup \Sigma_\Isf$, where $\Sigma_\Isf = \{I_a, I_b, D_a, D_b, Z_a, Z_b, \bar{Z}_a, \bar{Z}_b\}$. The idea is as follows. Let $c = (\ell, z_0, z_1)$ be a configuration of $\Mmc$. We encode $c$ as a finite word $w_c = \ell u x \in \Sigma^*$, where $\ell \in \{1,2, \dots, k\}$ encodes the current line number, $u \in \{a,b\}^*$ with $|u|_a = z_0$ and $|u|_b = z_1$ encodes the current counter values, and $x \in \Sigma_\Isf$ encodes the instruction $\Isf_\ell$ of line $\ell$ as follows:

* If $\Isf_\ell = \mathsf{Inc}(Z_0)$, then $x = I_a$, and if $\Isf_\ell = \mathsf{Inc}(Z_1)$, then $x = I_b$.

* If $\Isf_\ell = \mathsf{Dec}(Z_0)$, then $x = D_a$, and if $\Isf_\ell = \mathsf{Dec}(Z_1)$, then $x = D_b$.

* If $\Isf_\ell = \mathsf{If}\ Z_0 = 0\ \mathsf{goto}\ \ell'\ \mathsf{else}\ \ell''$, and the line number of the unique successor configuration of $c$ is $\ell'$, then $x = Z_a$ (that is, the zero-test is successful). Analogously with $x = Z_b$.

* If $\Isf_\ell = \mathsf{If}\ Z_0 = 0\ \mathsf{goto}\ \ell'\ \mathsf{else}\ \ell''$, and the line number of the unique successor configuration of $c$ is $\ell''$, then $x = \bar{Z}_a$ (that is, the zero-test fails). Analogously with $x = \bar{Z}_b$.

Let $w_c, w_{c'} \in \Sigma^*$ be two words encoding two configurations of $\Mmc$. We call $w_c \cdot w_{c'}$ correct if $c \vdash c'$. Hence, we can encode a unique infinite computations $c_0 c_1 c_2 \dots$ as an infinite word $w_{c_0} w_{c_1} w_{c_2} \dots$. We show that the $\omega$-language $L = \{w_{c_0} w_{c_1} w_{c_2} \dots \}$ can be written as the intersection of two deterministic strong reset PA $\omega$-languages. Let

\begin{align*}
L_1 &= \{w_{c_0} w_{c_1} w_{c_2} \dots \mid w_{c_{2i}} w_{c_{2i+1}}\text{ is correct for every } i \geq 0\}, \text{ and} \\
L_2 &= \{w_{c_0} w_{c_1} w_{c_2} \dots \mid w_{c_{2i+1}} w_{c_{2i+2}} \text{ is correct for every } i \geq 0\}.
\end{align*}

Observe that $L_1 \cap L_2 = L$, and $L$ is empty if and only if the unique computation of $\Mmc$ terminates.
Hence, it remains to show that $L_1$ and $L_2$ are recognized by deterministic strong reset PA.
We argue for $L_1$; the argument for $L_2$ is very similar.
The idea is as follows: We construct a deterministic strong reset PA $\Amc_1$ with five counters that tests the correctness of two consecutive encodings of configurations, say $w_{c_{2i}} \cdot w_{c_{2i + 1}} = \ell_1 u_1 x_1 \cdot \ell_2 u_2 x_2$ with $\ell_1, \ell_2 \in \{1, 2, \dots, k\}$, $u_1 u_2 \in \{a,b\}^*$ and $x_1, x_2 \in \Sigma_\Isf$.
First observe that checking whether $\ell_2$ is indeed the correct line number (that is, the correct successor of $\ell_1$) can be hard-coded into the state space of $\Amc_1$: if $x_1$ encodes an increment or decrement, we expect $\ell_2 = \ell_1 + 1$, and if $x_1$ encodes a successful or failing zero-test $\mathsf{If}\ Z_i = 0\ \mathsf{goto}\ \ell'\ \mathsf{else}\ \ell''$, we expect $\ell_2 = \ell'$ or $\ell_2 = \ell''$, respectively.
Four counters of $\Amc_1$ are used to count the numbers of $a$'s and $b$'s in $u_1$ and $u_2$, respectively. Then, if $x = I_a$, we expect $|u_2|_a = |u_1|_a + 1$ and $|u_2|_b = |u_1|_b$, and so on.
To be able to perform the correct check, we also encode $x_1$ into the state space as well as the fifth counter by counting modulo $|\Sigma_\Isf|$.
Observe that the guarded-decrement property ensures that decrements are handled correctly.
Hence, $\Amc_1$ has two sets of states counting the numbers of $a$'s and $b$'s of $u_1$ and $u_2$, accordingly, as well as a set of accepting states that is used to check the counter values.

After such a check, $\Amc_1$ resets, and continues with the next two (encodings of) configurations. The automaton for $L_2$ works in the same way, but skips the first configuration.

As shown, the intersection emptiness problem for deterministic strong reset PA is undecidable, implying the same for deterministic weak reset PA, and hence their existential PA model checking problems.
Recall that this problem is also undecidable for deterministic safety PA and deterministic co-Büchi PA.

Existential PA model checking for deterministic strong reset PA, deterministic weak reset PA, deterministic safety PA and deterministic co-Büchi PA is undecidable.

§ CONCLUSION

We have studied the deterministic variants of weak reset PA, strong reset PA, reach-reg. PA, and most notably limit PA. The latter are closed under the Boolean operations and hence all common decision problems are decidable for them, including the classical model checking problems.
Closely related to model checking problems are synthesis problems. Here, the problem is to generate a model from a system specification (which is correct by construction). Gale-Stewart games play a key role in solving such synthesis problems <cit.>. However, these games are undecidable when winning conditions are specified by automata whose emptiness or universality problem is undecidable.
Our decidability results for deterministic limit PA raise the interesting and important question whether Gale-Stewart games can be solved when their winning condition is expressed by these automata.

In future work we further plan to study the regular separability problem for these models, that is, given two $\omega$-languages $L_1, L_2$ recognized by PA operating on infinite words, is there an $\omega$-regular language $L$ with $L_1 \subseteq L$ and $L_2 \cap L = \varnothing$.
Solving this problem can be used as an alternative approach to solving existential PA model checking, as (regular) separability implies intersection emptiness. It has already been studied for some related models, PA on finite words <cit.> and Büchi $\mathsf{VASS}$ <cit.>.
Furthermore, it remains to classify the intersections of all incomparable models and thereby to provide a fine grained “map of the universe” for Parikh recognizable $\omega$-languages.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Baumann et al(2023a)]
authorpersonPascal Baumann, personFlavio D'Alessandro, personMoses Ganardi, personOscar Ibarra, personIan McQuillan, personLia Schütze, and personGeorg Zetzsche. year2023a.
Unboundedness Problems for Machines with Reversal-Bounded Counters. In booktitleFoundations of Software Science and Computation Structures. publisherSpringer Nature Switzerland, addressCham, pages240–264.

[Baumann et al(2023b)]
authorpersonPascal Baumann, personRoland Meyer, and personGeorg Zetzsche. year2023b.
titleRegular Separability in Büchi VASS.
[arxiv]2301.11242 [cs.FL]

[Bergsträßer et al(2024)]
authorpersonPascal Bergsträßer, personMoses Ganardi, personAnthony W. Lin, and personGeorg Zetzsche. year2024.
Ramsey Quantifiers in Linear Arithmetics.
journalProc. ACM Program. Lang. volume8, numberPOPL (year2024).

[Clarke et al(2018)]
authorpersonEdmund M. Clarke, personThomas A. Henzinger, personHelmut Veith, and personRoderick Bloem. year2018.
booktitleHandbook of Model Checking (edition1st ed.).
publisherSpringer Publishing Company, Incorporated.

[Clemente et al(2016)]
authorpersonLorenzo Clemente, personWojciech Czerwiński, personSławomir Lasota, and personCharles Paperman. year2016.
titleRegular Separability of Parikh Automata.
[arxiv]1612.06233 [cs.FL]

authorpersonLeonard Eugene Dickson. year1913.
Finiteness of the Odd Perfect and Primitive Abundant Numbers with n Distinct Prime Factors.
journalAmerican Journal of Mathematics volume35, number4 (year1913), pages413–422.

[Fernau and Stiebe(2008)]
authorpersonHenning Fernau and personRalf Stiebe. year2008.
Blind Counter Automata on omega-Words.
journalFundam. Inform.  volume83 (year2008), pages51–64.

[Figueira and Libkin(2015)]
authorpersonDiego Figueira and personLeonid Libkin. year2015.
Path Logics for Querying Graphs: Combining Expressiveness and Efficiency. In booktitleProceedings of the 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (seriesLICS ’15). publisherIEEE, pages329–340.

[Gale and Stewart(1953)]
authorpersonDavid Gale and personF. M. Stewart. year1953.
booktitleInfinite Games with Perfect Information.
publisherPrinceton University Press, addressPrinceton, pages245–266.

authorpersonSheila A. Greibach. year1978.
Remarks on blind and partially blind one-way multicounter machines.
journalTheoretical Computer Science volume7, number3 (year1978), pages311–324.

[Grobler et al(2023)]
authorpersonMario Grobler, personLeif Sabellek, and personSebastian Siebertz. year2023.
titleRemarks on Parikh-recognizable omega-languages.

[Guha et al(2022)]
authorpersonShibashis Guha, personIsmaël Jecker, personKaroliina Lehtinen, and personMartin Zimmermann. year2022.
Parikh Automata over Infinite Words. In booktitle42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022) (seriesLeibniz International Proceedings in Informatics (LIPIcs), Vol. volume250). publisherSchloss Dagstuhl – Leibniz-Zentrum für Informatik, pages40:1–40:20.

authorpersonChristoph Haase. year2018.
A Survival Guide to Presburger Arithmetic.
journalACM SIGLOG News volume5, number3 (year2018), pages67–82.

[Haase and Halfon(2014)]
authorpersonChristoph Haase and personSimon Halfon. year2014.
booktitleInteger Vector Addition Systems with States.
publisherSpringer International Publishing, pages112–124.

[Haase and Zetzsche(2021)]
authorpersonChristoph Haase and personGeorg Zetzsche. year2021.
Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests. In booktitleProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (Vancouver, Canada) (seriesLICS '19). publisherIEEE Press, Article articleno58, numpages14 pages.

[Herrmann et al(2023)]
authorpersonLuisa Herrmann, personVincent Peth, and personSebastian Rudolph. year2023.
titleDecidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures.
[arxiv]2305.01962 [cs.LO]

authorpersonOscar H. Ibarra. year1978.
Reversal-Bounded Multicounter Machines and Their Decision Problems.
journalJ. ACM volume25, number1 (year1978), pages116––133.

[Klaedtke and Rueß(2003)]
authorpersonFelix Klaedtke and personHarald Rueß. year2003.
Monadic Second-Order Logics with Cardinalities. In booktitleAutomata, Languages and Programming. publisherSpringer, addressBerlin, Heidelberg, pages681–696.

authorpersonLawrence H. Landweber. year1969.
Decision problems for $\omega$-automata.
journalMathematical systems theory  volume3 (year1969), pages376–384.

authorpersonRobert McNaughton. year1966.
Testing and generating infinite sequences by a finite automaton.
journalInformation and control volume9, number5 (year1966), pages521–530.

authorpersonMarvin L. Minsky. year1967.
booktitleComputation: Finite and Infinite Machines.

authorpersonWolfgang Thomas. year1991.
booktitleAutomata on Infinite Objects.
publisherMIT Press, addressCambridge, MA, USA, pages133–191.

[Thomas et al(2002)]
authorpersonWolfgang Thomas et al year2002.
booktitleAutomata, logics, and infinite games: a guide to current research. Vol. volume2500.
publisherSpringer Science & Business Media.