The structure of polynomial growth for tree automata/transducers and MSO set queries

TL;DR

This paper provides decision procedures and algorithms for analyzing polynomial and exponential growth in tree automata, transducers, and MSO set queries, with applications to classifying growth rates and subclass membership.

Contribution

It introduces new algorithms for determining growth rates and degrees in tree automata and MSO queries, generalizing existing results and providing tools for classifying tree-to-tree functions.

Findings

Quadratic time decision procedure for exponential vs polynomial growth.

Cubic time algorithm to compute the exact polynomial degree of growth.

Reparameterization theorem for MSO set queries with polynomial growth.

Abstract

Given an $\mathbb{N}$-weighted tree automaton, we give a decision procedure for exponential vs polynomial growth (with respect to the input size) in quadratic time, and an algorithm that computes the exact polynomial degree of growth in cubic time. As a special case, they apply to the growth of the ambiguity of a nondeterministic tree automaton, i.e. the number of distinct accepting runs over a given input. We deduce analogous decidability results (ignoring complexity) for the growth of the number of results of set queries in Monadic Second-Order logic (MSO) over ranked trees. In the case of polynomial growth of degree $k$, we also prove a reparameterization theorem for such queries: their results can be mapped to $k$-tuples of input nodes in a finite-to-one and MSO-definable fashion. We then apply these tools to study growth rates and subclass membership problems for tree-to-tree functions. Using new proof strategies, we recover and generalize known results concerning polyregular functions, total deterministic macro tree transducers, and partial nondeterministic top-down tree transducers. In particular, we give a procedure to decide polynomial size-to-height increase for both macro tree transducers and MSO set interpretations, and compute the degree. The paper concludes with a survey of a wide range of related work.