Beyond regularity: Equational tree automata for associative and commutative theories

Abstract

A new tree automata framework, called equational tree automata, is presented. In the newly introduced setting, congruence closures of recognizable tree languages are recognizable. Furthermore, we prove that in certain useful cases, recognizable tree languages are closed under union and intersection. To compare with early related work, e.g. [7], we discuss the relationship between linear bounded automata and equational tree automata. As a consequence, we obtain some (un)decidability results. We further present a hierarchy of 4 classes of tree languages.