Automata Theory

An Algorithmic Approach

A textbook that presents automata theory from a fresh viewpoint inspired by its main modern application, program verification, where automata are viewed as data structures for the algorithmic manipulation of sets and relations.

Published by MIT Press with open access

Free PDF Buy copy Errata

This book uses the novel approach of automata as data structures. It is suitable for undergraduate/graduate courses on automata theory; for programmers looking to broaden their skill set; and for researchers in automata theory and formal verification. The book offers a good balance of descriptions, theoretical results, examples, illustrations and solved exercises.

Automata on finite words

Automata classes and conversions
Minimization and reduction
Operations on sets: implementations
Application I: pattern matching
Operations on relations: implementations
Finite universes and decision diagrams
Application II: verification
Automata and logic
Application III: Presburger arithmetic

Automata on infinite words

Classes of ω-automata and conversions
Boolean operations: implementations
Emptiness check: implementations
Application I: verification and temporal logic
Application II: MSO logics on ω-words and linear arithmetic

Authors

Javier Esparza

Professor and chair of Foundations of Software Reliability and Theoretical Computer Science at the Technical University of Munich (Germany). Coauthor of Free Choice Petri Nets and Unfoldings: A Partial-Order Approach to Model Checking.

Michael Blondin

Associate professor of computer science at the Université de Sherbrooke (Canada). Researcher at the intersection of theoretical computer science and formal methods (formal verification, automata theory, concurrency, logic, computational complexity theory).

More information

Versions of the book:
Slides: Javier Esparza has produced freely available slides for a master's course based on this book at the Technical University of Munich. Their sources can be requested by instructors from MIT Press.
Exercise solutions: around 2/3 of the solutions appear in the appendix; the remaining ones can be requested by instructors from MIT Press.
Typos, mistakes and such can be listed and reported here.

Slides

These slides have been produced by Javier Esparza for a master's course based on this book at the Technical University of Munich. The sources can be requested by instructors from MIT Press.