Parikh Automata on Finite and Infinite Words

TL;DR

This paper investigates Parikh automata on finite and infinite words, analyzing their properties, variants, and relationships to other counting models, with implications for model checking.

Contribution

It introduces multiple definitions of Parikh automata on infinite words and compares their expressiveness and decision problems to related models.

Findings

Parikh automata on finite words have established properties.

Multiple definitions for infinite words are proposed and analyzed.

Comparative analysis with other counting models on infinite words.

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.