Deterministic Parikh automata on infinite words
Mario Grobler, Sebastian Siebertz
TL;DR
This work analyzes the deterministic variants of Parikh automata on infinite words, identifying deterministic limit PA as the most expressive and well-behaved, capable of generalizing $ω$-regular languages while remaining closed under Boolean operations and supporting standard decision problems. It provides a detailed comparison of expressiveness among deterministic limit PA, deterministic reachability PA, deterministic reachability-regular PA, deterministic strong/weak reset PA, and deterministic Büchi PA, revealing several incomparabilities and inclusions. The paper also maps the complexity landscape for core decision problems and model checking across these models, showing decidability for deterministic limit PA in many cases (often Pi$_2^P$-hardness in general) and highlighting undecidability in several other deterministic variants, particularly for strong/weak reset PA. The results have implications for verification and synthesis, including model checking, regular separability, and potential advancements in Gale–Stewart games when winning conditions are specified by Parikh-automata-derived ω-languages.
Abstract
Various variants of Parikh automata on infinite words have recently been introduced in the literature. However, with some exceptions only their non-deterministic versions have been considered. In this paper we study the deterministic versions of all variants of Parikh automata on infinite words that have not yet been studied. We compare the expressiveness of the deterministic models and investigate 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 $ω$-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.