Automata theory and its applications (Q5936849)

This textbook studies the many facets of finite automata with a special emphasis on finite automata on infinite strings and trees (Büchi, Rabin, etc.) and their applications. After an introduction of basic set-theoretic concepts and notations (in Chapter~1), the second chapter turns to finite automata on finite input words and their basic results (closure properties, the Myhill-Nerode theorem, Kleene's characterization of regular sets, pumping lemma and applications). As an appetizer for the later decidability results, monadic second-order logic on strings is introduced and shown to be decidable. The third chapter studies finite automata on infinite words and their different acceptance conditions (Büchi, Müller) and gives a proof of McNaughton's theorem equating both conditions in acceptance power. Then the monadic second-order theory of the natural numbers with one successor, S1S, is shown to be decidable. After a preparatory chapter on games played on graphs, Chapter~5 turns to finite automata on infinite trees, a.k.a.~Rabin automata. The main result in this chapter is Rabin's theorem stating that the complement of any Rabin recognizable language of trees is again Rabin recognizable. The proof, following Gurevich and Harrington, uses the equivalence of Rabin automata with so-called game automata. The final chapter presents a number of applications of Rabin automata, in particular proofs that a number of logical theories are decidable, the most prominent of which is certainly the monadic second-order theory of two successors, S2S. The book gives a gentle introduction to the theory of finite automata working on infinite objects and will be useful for anybody looking for a coherent treatment of the basic theoretical results from this area as well as an exposition of its applications in mathematical logic and computer science.