  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.
