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

摘要

Finite-state tree automata are a well studied formalism for representing termlanguages. This paper studies the problem of determining the regularity of theset of instances of a finite set of terms with variables, where each variableis restricted to instantiations of a regular set given by a tree automaton. Theproblem was recently proved decidable, but with an unknown complexity. Here,the exact complexity of the problem is determined by provingEXPTIME-completeness. The main contribution is a new, exponential timealgorithm that performs various exponential transformations on the involvedterms and tree automata, and decides regularity by analyzing formulas overinequality and height predicates.