  This thesis is focused on techniques for finite automata and their use in
practice, with the main emphasis on nondeterministic tree automata. This
concerns namely techniques for size reduction and language inclusion testing,
which are two problems that are crucial for many applications of tree automata.
For size reduction of tree automata, we adapt the simulation quotient technique
that is well established for finite word automata. We give efficient algorithms
for computing tree automata simulations and we also introduce a new type of
relation that arises from a combination of tree automata downward and upward
simulation and that is very well suited for quotienting. The combination
principle is relevant also for word automata. We then generalise the so called
antichain universality and language inclusion checking technique developed
originally for finite word automata for tree automata. Subsequently, we improve
the antichain technique for both word and tree automata by combining it with
the simulation-based inclusion checking techniques, significantly improving
efficiency of the antichain method. We then show how the developed reduction
and inclusion checking methods improve the method of abstract regular tree
model checking, the method that was the original motivation for starting the
work on tree automata. Both the reduction and the language inclusion methods
are based on relatively simple and general principles that can be further
extended for other types of automata and related formalisms. An example is our
adaptation of the reduction methods for alternating B\"uchi automata, which
results in an efficient alternating automata size reduction technique.
