The aim of this book is to present a theory of several types of automata and applications of these facts in logic, concurrency and algebra. It contains lectures concerning the theory and applications of finite automata, Büchi automata, games on finite graphs, and Rabin automata. The chapter on finite automata is extended by finite automata recognisable relations and finite automata with equational constraints. The final section of this chapter proves the decidability of the monadic second-order logic of finite strings. The chapter on Büchi automata contains basic results and results on the relationship to Müller automata and sequential Rabin automata. Among the applications, the authors prove that the monadic second-order theory of one successor (S1S) is decidable. The purpose of the chapter on games is to give a game-theoretic models for concurrent processes of infinite duration: this chapter introduces the concept of the last visitation record, which plays an important role in proofs of some fundamental results. The chapter on Rabin automata uses game-theoretic techniques from the previous chapter: special (Rabin) automata are also studied in this chapter. The final chapter contains examples of applications of Rabin automata to mathematical theories, such as the monadic second-order theory of n successors. The book contains a representative bibliography, divided according to individual applications.

The book contains suitable material for a two-semester course for students of computer science or mathematics. It is completely self-contained and one can really enjoy reading it. It is strongly recommended for researchers and postgraduate students interested in logic, automata and/or concurrency.

Reviewer:

mpl