# Two-way Parikh Automata

## TL;DR

This paper investigates two-way Parikh automata, revealing undecidability of emptiness in nondeterministic cases and providing complexity bounds for key decision problems under various constraints.

## Contribution

It introduces the study of two-way Parikh automata, establishing decidability results, complexity bounds, and precise characterizations for classical decision problems.

## Key findings

- Emptiness is undecidable for nondeterministic two-way Parikh automata.
- PSpace-complete complexity for bounded visits with existential Presburger constraints.
- Exact complexity characterizations for inclusion, equivalence, and universality problems.

## Abstract

Parikh automata extend automata with counters whose values can only be tested at the end of the computation, with respect to membership into a semi-linear set. Parikh automata have found several applications, for instance in transducer theory, as they enjoy decidable emptiness problem. In this paper, we study two-way Parikh automata. We show that emptiness becomes undecidable in the non-deterministic case. However, it is PSpace-C when the number of visits to any input position is bounded and the semi-linear set is given as an existential Presburger formula. We also give tight complexity bounds for the inclusion, equivalence and universality problems. Finally, we characterise precisely the complexity of those problems when the semi-linear constraint is given by an arbitrary Presburger formula.