The HOM Problem Is Decidable

We close affirmatively a question that has been open for long time: decidability of the HOM problem. The HOM problem consists in determining, given a tree homomorphism H and a regular tree language L represented by a tree automaton, whether H(L) is regular. In order to decide the HOM problem, we develop new constructions and techniques that are interesting by themselves, and provide several significant intermediate results. For example, we prove that the universality problem is decidable for languages represented by tree automata with equality constraints, and that the equivalence and inclusion problems are decidable for images of regular languages through tree homomorphisms. Our contributions are based on the following new constructions. We describe a simple transformation for converting a tree automaton with equality constraints into a tree automaton with disequality constraints recognizing the complementary language. We also define a new class of tree automata with arbitrary disequality constraints and a particular kind of equality constraints. An automaton of this new class essentially recognizes the intersection of a tree automaton with disequality constraints and the image of a regular language through a tree homomorphism. We prove decidability of emptiness and finiteness for this class by a pumping mechanism. We combine the above constructions adequately to provide an algorithm deciding the HOM problem. This is the journal version of a paper presented in the 42nd ACM Symposium on Theory of Computing (STOC 2010). Here, we provide all proofs and examples. Moreover, we obtain better complexity results via the modification of some proofs and a careful complexity analysis. In particular, the obtained time complexity for the decision of HOM is a tower of three exponentials.