Parikh Automata on Finite and Infinite Words

TL;DR

This paper develops a comprehensive theory of Parikh automata on finite and infinite words, introducing and analyzing several nondeterministic and deterministic models that extend classical automata with counting via semi-linear (Presburger-definable) constraints. It proves core equivalences between models (e.g., reachability-regular PA and limit PA), establishes omega-closure properties, and provides automata-characterizations for target omega-language classes such as $L_{\mathsf{PA, Reg}}^\omega$ and $L_{\mathsf{Reg, PA}}^\omega$. A central contribution is the detailed map of expressiveness, closure properties, and decision problems (emptiness, membership, universality, and model checking) across nondeterministic and deterministic variants, including a complete view of how epsilon-transitions affect power (notably eliminating epsilon for almost all models except safety and co-Büchi PA). The results offer practical model-checking implications by identifying decidable fragments (e.g., deterministic limit PA universality) and provide a framework to compare Parikh-based counting with blind-counter and Presburger-augmented automata in infinite-word settings. Overall, the work significantly advances the understanding of counting automata on infinite words and lays groundwork for synthesis and regular-separability questions in this richer automata landscape.

Abstract

We study Parikh automata on finite and infinite words. First we establish some results for Parikh automata on finite words. Following, we present several definitions of Parikh automata on infinite words. We consider the deterministic as well as the non-deterministic variants and study closure properties, expressiveness, and common decision problems with applications to model checking. Furthermore, we compare our models to other models with counting mechanisms operating on infinite words.

Figures (10)

• Figure 1: The semi-linear set $C = C((0,0), \{(1,1)\}) \cup C((1,2), \{(0,1), (2,1)\})$.
• Figure 2: Illustration of the construction of a linear set from an integer expression.
• Figure 3: Illustration of the construction of a deterministic acyclic PA from an integer expression.
• Figure 4: The automaton $\mathcal{A}\xspace$ with $C=\{(z,z'), (z, \infty) \mid z' \geq z\}$ from \ref{['ex']}.
• Figure 5: The strong reset PA for $\{a^n b^n \mid n \geq 1\}^\omega \cup \{a^n b^n \mid n \geq 1\}^* \cdot$$\{a\}^\omega$ with semi-linear set $C = \{(z,z) \mid z \in \mathbb{N}\xspace\}$.

Theorems & Definitions (140)

• Theorem 2.1: Büchi buechi
• lemma 1
• proof
• proof : Proof
• proof : Proof
• Remark
• corollary 1
• proof
• lemma 2
• proof