Lecture notes for a course on finite and omega-automata

These notes introduce the theory of finite- and omega-automata from an algorithmic point of view. Courses on data structures teach how to represent sets in a computer so that operations like insertion, deletion, or lookup, can be efficiently implemented. These notes present automata as a data structure for sets that allows for efficient implementations of the basic set-theoretical operations (union, intersection, and complement), decision procedures for basic properties (emptiness, universality, containment), and basic operations on relations (projection, join). Applications to pattern matching, formal verification, and decision procedures for logical and arithmetical theories are discussed.

- Introduction and goal
- Part I: Automata on finite words
- Automata classes and conversions
- Minimization and reduction
- Operations on sets: Implementation with DFAs and NFAs
- Applications I: Pattern Matching
- Operations on relations: Implementation with transducers
- Operations on finite sets: Implementation with minimal DFAs
- Applications II: Verification
- Automata and logic
- Applications III: Presburger arithmetic

- Part II: Automata on infinite words
- Classes of omega-automata and conversions
- Boolean operations: Implementations
- Emptiness check: Implementations
- Applications I: Verification and temporal logic
- Applications II: Monadic second order logic and linear arithmetic

.

There are excellent textbooks on automata theory, ranging from course books for undergraduates to research monographies for specialists. Why another one? During the late 1960s and early 1970s the main application of automata theory was the development of lexicographic analyzers, parsers, and compilers, and so automata were viewed as abstract machines that process inputs and accept or reject them. This view deeply influenced the textbook presentation of the theory. While results about the expressive power} of machines, like pumping lemmas, equivalences between models, and closure properties, were devoted much attention, constructions on automata, like the powerset or product construction, often played a subordinate role as proof tools. To give a simple example, in many textbooks of the time---and in later textbooks written in the same style---the powerset construction is not introduced as an algorithm that constructs a DFA equivalent to a given NFA; instead, the equivalent DFA is mathematically defined by describing its set of states, transition relation, etc.. Sometimes, the simple but computationally important fact that only states reachable from the initial state need be constructed is not mentioned. Since the middle 1980s program verification has progressively replaced compilers as the driving application of automata theory. Automata started to be used to describe the behaviour---and intended behaviour---of hardware and software systems, not their syntactic descriptions. This shift from syntax to semantics had important consequences. While automata for lexical or syntactical analysis typically have at most some thousands of states, automata for semantic descriptions can easily be many orders of magnitude larger. Efficient constructions and algorithmic issues became imperative, and research in this direction made great progress. At the same time, automata on infinite words and the connection between logic and automata became more relevant. While these research developments certainly influenced textbooks, and algorithmic issues gradually received more attention, undergraduate texts still retain many concepts from the past. This book intends to reflect the evolution of automata theory. Automata on infinite words can hardly be seen as machines accepting or rejecting an input: they could only do so after infinite time! And the view of automata as abstract machines puts an emphasis expressibility that no longer corresponds to its relevance for modern applications. We think that modern automata theory is better captured by the slogan ''automata as data structures''. Just as hash tables and Fibonacci heaps are both adequate data structures for sets when the operations one needs are those of a dictionary or a priority queue, automata are the right data structure for sets and relations when the required operations are union, intersection, complement, projections and joins. In this view, the algorithmic implementation of the operations must get the limelight, and, as a consequence, algorithms constitute the spine of this book. A second goal of these notes is concerned with presentation. Experience tells that automata-theoretic constructions are best explained by means of examples, and that examples are best presented with the help of pictures. Automata on words are blessed with a graphical representation of instantaneous appeal. In this book we have invested much effort into finding illustrative, non-trivial examples whose graphical representation still fits in one page.

Back to: Javier Esparza