Algorithm to determine if a top-down non deterministic tree automata accepts some tree?
Yes, you can do it in linear time.  Associate to each pair of a state $q$ a boolean variable $x_q$; the intended meaning is $x_{q,s}$ should be true if there exists a tree that is accepted by the automaton if we start with state $q$ at the root.  Then, each transition rule of the automaton corresponds to a Horn clause on these boolean variables. For instance, the transition rule $f(q_1,\dots,q_n) \to q'(f)$ corresponds to the Horn clause $(x_{q_1} \land \cdots \land x_{q_n}) \implies x_{q'}$.  Now, solve the associated HornSAT problem using any standard algorithm to find the minimal satisfying assignment to all of these clauses; this can be done in linear time.  If you find any final state $q$ of the automaton such that $x_q$ is set to true by this assignment, then the answer is yes, there exists a tree that's accepted by this automaton; otherwise, the answer is no.