Non-Global Parikh Tree Automata

TL;DR

This paper introduces non-global Parikh tree automata, a new model where counter configurations are distributed at each node, leading to incomparability with global PTA and varying decidability results for non-emptiness.

Contribution

It presents a novel non-global PTA model, analyzes its properties, and compares it with global PTA, including decidability results under specific restrictions.

Findings

Non-global PTA and global PTA recognize incomparable tree languages.

Non-emptiness is undecidable for non-global PTA with three or more counters.

Decidability of non-emptiness is achievable under linear configuration passing restrictions.

Abstract

Parikh (tree) automata are an expressive and yet computationally well-behaved extension of finite automata -- they allow to increment a number of counters during their computations, which are finally tested by a semilinear constraint. In this work, we introduce and investigate a new perspective on Parikh tree automata (PTA): instead of testing one counter configuration that results from the whole input tree, we implement a non-global automaton model. Here, we copy and distribute the current configuration at each node to all its children, incrementing the counters pathwise, and check the arithmetic constraint at each leaf. We obtain that the classes of tree languages recognizable by global PTA and non-global PTA are incomparable. In contrast to global PTA, the non-emptiness problem is undecidable for non-global PTA if we allow the automata to work with at least three counters, whereas the membership problem stays decidable. However, for a restriction of the model, where counter configurations are passed in a linear fashion to at most one child node, we can prove decidability of the non-emptiness problem.