Introduction to automaton theory on infinite trees

We study tree automaton here, and mainly on infinite trees. In the first part of thesis,we will introduce how there is a generalization from words to trees and what is the definition of infinite tree. Then we introduce the tree automata working on finite and infinite trees. Büchi automata and Muller automata classically corresponds to the acceptance mode of infinite trees. We will introduce them and their recognizability and later the theoretical importance will be introduced together. Next a game used to simulate the possible runs of a tree automaton will be introduced, which can prove Rabin's complementation theorem. In the next part, we shall study the trees from the topological aspects. Subsequently, the relations between logics and tree automata will be showed. Last but not least, the practical uses of the tree automaton will be showed.