Automata over infinite trees are used in many areas of theoretical computer science, such as model checking or description logics. This is because deciding the satisfiability of many types of logical formulae can be reduced to checking the emptiness of the tree language defined by such an automaton. Weighted automata can be used to compute quantifiable properties of formulae. The language inclusion problem for certain types of automata over infinite trees is analyzed, as well as a generalization of this problem to weighted automata. Several constructions are presented and compared for different automata models.