B\"uchi-like characterizations for Parikh-recognizable omega-languages

TL;DR

This paper extends Büchi's theorem to Parikh automata, providing automata-theoretic characterizations of omega-languages with Parikh-recognizable and regular components, connecting various models and introducing a new one.

Contribution

It offers a novel automata-theoretic characterization of Parikh-recognizable omega-languages and links existing models with new variants.

Findings

Characterization of languages of the form $U_i V_i^omega$ with Parikh automata.

Equivalence of certain language classes with models by Klaedtke-Ruess and Guha et al.

Introduction of a new model capturing languages with regular $U_i$ and Parikh-recognizable $V_i$.

Abstract

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