Book cover

Automata Theory

An Algorithmic Approach

Javier Esparza and Michael Blondin

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

  1. Automata classes and conversions
  2. Minimization and reduction
  3. Operations on sets: implementations
  4. Application I: pattern matching
  5. Operations on relations: implementations
  6. Finite universes and decision diagrams
  7. Application II: verification
  8. Automata and logic
  9. Application III: Presburger arithmetic

Automata on infinite words

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


Picture of Michael Blondin

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