Deciding Regularity of the Set of Instances of a Set of Terms with Regular Constraints is EXPTIME-Complete

TL;DR

This paper establishes that deciding the regularity of instances of terms with regular constraints is EXPTIME-complete, providing a precise complexity classification and an exponential time decision algorithm.

Contribution

The paper proves EXPTIME-completeness for the problem and introduces a new exponential time algorithm based on transformations and predicate analysis.

Findings

The problem is EXPTIME-complete.

An exponential time algorithm is proposed.

The algorithm uses transformations and predicate analysis.

Abstract

Finite-state tree automata are a well studied formalism for representing term languages. This paper studies the problem of determining the regularity of the set of instances of a finite set of terms with variables, where each variable is restricted to instantiations of a regular set given by a tree automaton. The problem was recently proved decidable, but with an unknown complexity. Here, the exact complexity of the problem is determined by proving EXPTIME-completeness. The main contribution is a new, exponential time algorithm that performs various exponential transformations on the involved terms and tree automata, and decides regularity by analyzing formulas over inequality and height predicates.