Book excerpts:

Tree automata have been designed a long time ago in the context of circuit verification. Since then many new ideas had came out, such as the connections between automata and logic.

In the 70’s many new results were established concerning tree automata, which lose a bit their connections with the applications and were studied for their own. In particular, a problem was the very high complexity of decision procedures for the monadic second order logic. Applications of tree automata to program verification revived in the 80’s, after the relative failure of automated deduction in this field. It is possible to verify temporal logic formulas (which are particular Monadic Second Order Formulas) on simpler (small) programs. Automata, and in particular tree automata, also appeared as an approximation of programs on which fully automated tools can be used. New results were obtained connecting properties of programs or type systems or rewrite systems with automata.

The goal of this book is to fill in the existing gap and to presents the basics of tree automata and several variants of tree automata which have been devised for applications in the aforementioned domains. This book shall discuss only finite tree automata, and the reader interested in infinite trees should consult any recent survey on automata on infinite objects and their applications (See the bibliography).

The second main restriction that this book have is to focus on the operational aspects of tree automata. This book should appeal the reader who wants to have a simple presentation of the basics of tree automata, and to see how some variations on the idea of tree automata have provided a nice tool for solving difficult problems. Therefore, specialists of the domain probably know almost all the material embedded. However, this book can still be helpful for many researchers who need some knowledge on tree automata. This is typically the case of PhD a student who may find new ideas and guess connections with his (her) own work.