@book {MATHEDUC.05869418,
author = {Hofmann, Martin and Lange, Martin},
title = {Automata theory and logic. (Automatentheorie und Logik.)},
year = {2011},
isbn = {978-3-642-18089-7},
pages = {x, 240~p.},
publisher = {Berlin: Springer},
doi = {10.1007/978-3-642-18090-3},
abstract = {Since B\"uchi employed automata theory to prove decidability results for logical theories, the strong connection of automata theory and logic belongs to the most important foundational issues of computer science and should therefore be fully understood by every master student of computer science. So, good textbooks on this subject are always welcome. The present one grew out of a course that the authors held a couple of times for advanced students of computer science and mathematics at the LMU in Munich. It is self-contained with respect to automata theory in that all necessary notions and results from an elementary course in automata and formal language theory are compiled in the first chapter in order to give a coherent account of the subject. Nevertheless, some basic knowledge in other areas, such as symbolic logic and computational complexity, is presupposed. The book is divided into four parts. In each one the authors consider, in a number of chapters, automata theory over certain structures: finite words, infinite words, finite trees, and infinite trees, respectively. Part 1 starts, as already mentioned above, with a chapter that recalls the necessary notions and results of formal language and automata theory from a basic course: regular languages, nondeterministic and deterministic finite automata, recognisabilty of formal languages by automata, and decidability and complexity of important decision problems for regular languages. Chapter 2 sets the stage for the second protagonist of this book: logic, in fact weak monadic second-order logic (WMSO) with its syntax and semantics. Automata are then employed to show WMSO-definability of regular languages as well as the complexity of the decision problem for WMSO-formulas. A short section on Presburger arithmetic concludes this chapter. Alternating automata are the subject of Chapter 3, while Chapter 4 deals with star-free languages and the corresponding first-order logic (FO). Using Ehrenfeucht-Fra\"{\i}ss\'e games, it is shown that the star-free languages are a proper subclass of the regular languages. Part 2, on automata theory over infinite words, is by far the longest one, comprising some 100 pages. It starts with Chapter 5, in which B\"uchi automata are introduced as the first of several automaton models that are able to recognise infinite words. $\omega$-regular languages are defined and shown to be exactly the language class recognised by nondeterministic B\"uchi automata (NBA). Chapter 6 deals with B\"uchi's construction of an NBA recognizing exactly the complement of a given $\omega$-language, thus paving the way to showing decidability of (not any more weak) monadic second-order logic (MSO), which corresponds exactly to the class of $\omega$-regular languages. Chapter 7 investigates different acceptance conditions for $\omega$-words in more depth, leading to the automaton models of Rabin, Streett, parity, Muller and co-B\"uchi automata, the last model being the only one of them not recognizing exactly the $\omega$-regular languages. Chapter 8 then turns towards deterministic automata and their recognition abilities. Central here is the construction of a deterministic Muller automaton for a given NBA that recognises the same $\omega$-language. Chapter 9 is on decision procedures for $\omega$-automata, in particular for the emptiness problem and the universality problem. The last section of this chapter shows how B\"uchi automata are applied to decide the termination problem for recursive programs. Chapter 10 takes up the alternating automata from Chapter 3 and generalises them to the case of infinite words. Finally, the last chapter of Part 2 deals with the important topic of linear-time temporal logic (LTL) and its application to specification and verification of reactive and parallel systems. Part 3 starts with Chapter 12, where trees come into play; here, finite $\Sigma$-trees over a finite alphabet $\Sigma$. Bottom-up and top-down tree automata are defined, both in their nondeterministic and deterministic variants, and their recognition properties with respect to tree languages are investigated. Finally, decidability of some decision problems for tree automata is shown. Chapter 13 comes with applications of tree automata to higher-order matching in simply typed $\lambda$-calculus and to the processing of XML-documents. The fourth part of the book is its natural completion with generalisations of its major concepts to infinite trees. First, Chapter 14 introduces parity as well as B\"uchi automata on infinite trees and their (differing) abilities to recognise infinite-tree languages. Parity games are then quite extensively studied at the start of Chapter 15 in order to construct in the sequel the complement of parity tree automata and to show the decidability of their emptiness problem. The final Chapter 16 comes back to the realm of logic, applying the developed machinery of automata on infinite trees to obtain decidability results for monadic second-order logic on infinite trees, the temporal logic $\mathrm{CTL}^*$ and the modal $\mu$-calculus. Each of the four parts of the book is complemented with exercises and a section with ``notes" putting the contents of the respective part into historical and conceptual context with extensive references to the literature, even up to the most recent research. At the end of the book, this concept is supplemented with a section on further perspectives, giving some broader view on related subjects that are not dealt with in the book and on open problems and suggestions of rewarding themes for dissertations. A subject index and a good list of references complete the book. This is a very good advanced textbook. It has a high standard, is written with mathematical rigour, and is nevertheless very clear in its exposition. It should get an Englisch edition in order to receive the broader audience it deserves.},
reviewer = {Klaus D. Kiermeier (Berlin)},
msc2010 = {P25xx (E35xx)},
identifier = {2013f.00849},
}