Novices to automata theory may want to start with Dines Bjørner’s narrative on principles and techniques, found in the automata theory chapter of his enjoyable three-volume set [1], which covers intuition, motivation, and pragmatics. Bjørner’s objective:

to help make sure that the reader can freely choose and usefully apply, when appropriate, the modeling principles and techniques of [...] automata and machines, as well as to encourage the reader to more seriously study more specialized textbooks on automata and formal languages.

Automata theory is one such “ specialized ” textbook. Its authors state that “automata are the right data structure for represent[ing] sets and relations when the required operations are union, intersection, complement, projections and joins.” In these applications, automata are used “to describe the behavior--or intended behavior--of hardware and software systems, not their syntax, and this shift from syntax to semantics had important consequences.”

The purpose of this book is “to teach a new master course on automata theory.” The authors “have invested much effort into finding illustrative, non-trivial examples whose graphical representation still fits in one page.” The book includes many end-of-chapter exercises, some introducing new and interesting concepts. Worked-out detailed solutions (144 pages in total) are provided in the text for many of the exercises. Note that already at the very beginning (p. 15), there are “four examples of [deterministic finite automata (DFA)] representing interesting sets, which also illustrate the theory and applications described in the coming chapters.” Regretfully, here and there the reader encounters forward references.

The first five chapters are “an introduction to finite automata at bachelor level ... with more examples and greater emphasis on algorithms.” Chapter 1 introduces classical data structures for the representation of various automata and describes the conversion algorithms between these representations. Chapter 2, on minimization and reduction, is specifically about the existence and construction of a unique minimal DFA recognizing a given regular language, and about approaches to reducing the size of a given nondeterministic finite automaton (NFA). Chapter 3 presents implementations of Boolean operations on sets using DFAs and NFAs as data structures. Chapter 4 discusses pattern matching, specifically the Knuth-Morris-Pratt algorithm, as a classical application of the techniques and results of chapter 3. I think it might be interesting to compare and contrast the authors’ presentation of this algorithm with a (substantially) longer narrative “showing how each next step in the argument, if not actually forced, is at least something sweetly reasonable to try” [2] in R. G. Dromey’s somewhat forgotten but still excellent book [3]. Chapter 5 discusses operations on relations using transducers as a data structure. This foundational material may, in the authors’ opinion, be “complemented by any subset” of the descriptions of the applications presented in chapters 6 through 9. Chapter 7 on the automata-theoretic approach to verification, with interesting exercises, may be of special note.

The following chapters 10 through 12 also belong to the “spine” of the book, but at the master’s level, and deal with regular languages of infinite words. The authors observe that “automata on infinite words can be used to finitely represent the set of executions” of routines of operating systems, communication protocols, and so on. Chapter 10 presents, in detail, various automata types and shows that for each application one must choose the appropriate type of automata on infinite words. Chapter 11 uses a special type of automata on infinite words for implementing Boolean operations on sets: union, intersection, and complement. Chapter 12 shows different implementations of the emptiness test on sets using algorithms based on depth-first search and those based on breadth-first search. The final two chapters (13 and 14) are about the application of concepts and constructs presented earlier to verify liveness properties of programs (using linear temporal logic) and to extend certain earlier results to the case of infinite words (in particular, from properties of integers to properties of real numbers).

The algorithms in the book are in clear pseudocode, with proofs, and their explanations use guards and invariants. However, as in many other texts, algorithm design considerations and the design process may at times appear to be absent, that is, to quote E. W. Dijkstra,

[...when the authors] pull ad libitum rabbits out of [their] hats. (“Rabbit” is the technical term for the unmotivated and surprising turn in an argument that eventually and miraculously “does the job” but leaves the reader with the gnawing question of how, the hell, the trick was invented.) [4]