Automata Theory
An Algorithmic Approach
by Esparza, Blondin
ISBN: 9780262376945 | Copyright 2023
Instructor Requests
A comprehensive introduction to automata theory that uses the novel approach of viewing automata as data structures.
This textbook 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. This novel “automata as data structures†paradigm makes holistic connections between automata theory and other areas of computer science not covered in traditional texts, linking the study of algorithms and data structures with that of the theory of formal languages and computability. Esparza and Blondin provide incisive overviews of core concepts along with illustrated examples and exercises that facilitate quick comprehension of rigorous material.
•Uses novel “automata as data structures†approach
•Algorithm approach ideal for programmers looking to broaden their skill set and researchers in automata theory and formal verification
•The first introduction to automata on infinite words that does not assume prior knowledge of finite automata
•Suitable for both undergraduate and graduate students
•Thorough, engaging presentation of concepts balances description, examples, and theoretical results
•Extensive illustrations, exercises, and solutions deepen comprehension
| Expand/Collapse All | |
|---|---|
| Contents (pg. vii) | |
| Preface (pg. xiii) | |
| Why This Book (pg. xiii) | |
| Acknowledgments (pg. xv) | |
| 0 Overview (pg. 1) | |
| 0.1 Introduction (pg. 1) | |
| 0.2 Outline and Structure (pg. 3) | |
| 0.3 On the Exercises (pg. 6) | |
| I AUTOMATA ON FINITEWORDS (pg. 7) | |
| 1 Automata Classes and Conversions (pg. 9) | |
| 1.1 Alphabets, Letters, Words, and Languages (pg. 9) | |
| 1.2 Regular Expressions: A Language to Describe Languages (pg. 10) | |
| 1.3 Automata Classes (pg. 12) | |
| 1.4 Conversion Algorithms (pg. 22) | |
| 1.5 A Tour of Conversions (pg. 35) | |
| 1.6 Exercises (pg. 38) | |
| 2 Minimization and Reduction (pg. 49) | |
| 2.1 Minimal DFAs (pg. 50) | |
| 2.2 Minimizing DFAs (pg. 55) | |
| 2.3 Reducing NFAs (pg. 63) | |
| 2.4 A Characterization of Regular Languages (pg. 68) | |
| 2.5 Exercises (pg. 69) | |
| 3 Operations on Sets: Implementations (pg. 75) | |
| 3.1 Implementation on DFAs (pg. 77) | |
| 3.2 Implementation on NFAs (pg. 84) | |
| 3.3 Exercises (pg. 94) | |
| 4 Application I: Pattern Matching (pg. 101) | |
| 4.1 The General Case (pg. 101) | |
| 4.2 The Word Case (pg. 103) | |
| 4.3 Exercises (pg. 110) | |
| 5 Operations on Relations: Implementations (pg. 113) | |
| 5.1 Encodings (pg. 114) | |
| 5.2 Transducers and Regular Relations (pg. 115) | |
| 5.3 Implementing Operations on Relations (pg. 117) | |
| 5.4 Relations of Higher Arity (pg. 124) | |
| 5.5 Exercises (pg. 125) | |
| 6 Finite Universes and Decision Diagrams (pg. 131) | |
| 6.1 Fixed-Length Languages and the Master Automaton (pg. 132) | |
| 6.2 A Data Structure for Fixed-Length Languages (pg. 133) | |
| 6.3 Operations on Fixed-Length Languages (pg. 135) | |
| 6.4 Determinization and Minimization (pg. 141) | |
| 6.5 Operations on Fixed-Length Relations (pg. 145) | |
| 6.6 Decision Diagrams (pg. 149) | |
| 6.7 Exercises (pg. 159) | |
| 7 Application II: Verification (pg. 163) | |
| 7.1 The Automata-Theoretic Approach to Verification (pg. 163) | |
| 7.2 Programs as Networks of Automata (pg. 167) | |
| 7.3 Concurrent Programs (pg. 173) | |
| 7.4 Coping with the State-Explosion Problem (pg. 177) | |
| 7.5 Safety and Liveness Properties (pg. 189) | |
| 7.6 Exercises (pg. 190) | |
| 8 Automata and Logic (pg. 193) | |
| 8.1 Predicate Logic on Words: An Informal Introduction (pg. 194) | |
| 8.2 Syntax and Semantics (pg. 195) | |
| 8.3 Macros and Examples (pg. 201) | |
| 8.4 Expressive Power of FO(E) (pg. 203) | |
| 8.5 Monadic Second-Order Logic on Words (pg. 206) | |
| 8.6 Syntax and Semantics (pg. 207) | |
| 8.7 Macros and Examples (pg. 209) | |
| 8.8 All Regular Languages Are Expressible in MSO(E) (pg. 212) | |
| 8.9 All Languages Expressible in MSO(E) Are Regular (pg. 215) | |
| 8.10 Exercises (pg. 225) | |
| 9 Application III: Presburger Arithmetic (pg. 229) | |
| 9.1 Syntax and Semantics (pg. 229) | |
| 9.2 An NFA for the Solutions over the Naturals (pg. 231) | |
| 9.3 An NFA for the Solutions over the Integers (pg. 236) | |
| 9.4 Exercises (pg. 242) | |
| II AUTOMATA ON INFINITE WORDS (pg. 245) | |
| 10 Classes of ω-Automata and Conversions (pg. 247) | |
| 10.1 ω-Languages and ω-Regular Expressions (pg. 247) | |
| 10.2 ω-Automata and the Quest for an ω-Trinity (pg. 249) | |
| 10.3 Beyond ω-Trinities (pg. 266) | |
| 10.4 Summary (pg. 283) | |
| 10.5 Exercises (pg. 284) | |
| 11 Boolean Operations: Implementations (pg. 289) | |
| 11.1 Generalized Büchi Automata (pg. 290) | |
| 11.2 Union and Intersection (pg. 291) | |
| 11.3 Complement (pg. 295) | |
| 11.4 Exercises (pg. 308) | |
| 12 Emptiness Check: Implementations (pg. 313) | |
| 12.1 Emptiness Algorithms Based on Depth-First Search (pg. 315) | |
| 12.2 Algorithms Based on Breadth-First Search (pg. 332) | |
| 12.3 Exercises (pg. 337) | |
| 13 Application I: Verification and Temporal Logic (pg. 341) | |
| 13.1 Automata-Based Verification of Liveness Properties (pg. 341) | |
| 13.2 Linear Temporal Logic (pg. 347) | |
| 13.3 From LTL Formulas to Generalized Büchi Automata (pg. 351) | |
| 13.4 Automatic Verification of LTL Formulas (pg. 358) | |
| 13.5 Exercises (pg. 361) | |
| 14 Application II: MSO Logics on ω-Words and Linear Arithmetic (pg. 365) | |
| 14.1 Monadic Second-Order Logic on ω-Words (pg. 365) | |
| 14.2 Linear Arithmetic (pg. 368) | |
| 14.3 Exercises (pg. 375) | |
| Solutions (pg. 377) | |
| Solutions for Chapter 1 (pg. 377) | |
| Solutions for Chapter 2 (pg. 403) | |
| Solutions for Chapter 3 (pg. 412) | |
| Solutions for Chapter 4 (pg. 430) | |
| Solutions for Chapter 5 (pg. 437) | |
| Solutions for Chapter 6 (pg. 445) | |
| Solutions for Chapter 7 (pg. 456) | |
| Solutions for Chapter 8 (pg. 463) | |
| Solutions for Chapter 9 (pg. 469) | |
| Solutions for Chapter 10 (pg. 478) | |
| Solutions for Chapter 11 (pg. 485) | |
| Solutions for Chapter 12 (pg. 492) | |
| Solutions for Chapter 13 (pg. 506) | |
| Solutions for Chapter 14 (pg. 517) | |
| Bibliographic Notes (pg. 523) | |
| Bibliography (pg. 531) | |
| Index (pg. 539) | |
Javier Esparza
Michael Blondin
| Instructors Only | |
|---|---|
|
You must have an instructor account and submit a request to access instructor materials for this book.
|
|
eTextbook
Go paperless today! Available online anytime, nothing to download or install.
Features
|
