Automata Theory and Logic

Summary

Hofmann and Lange’s textbook develops the correspondence between automata, formal languages, games, and logics over finite words, infinite words, finite trees, and infinite trees. It is a broad foundation text rather than a single research paper, so this note records the main reusable technical spine for the wiki.

The book starts with regular languages over finite words, finite automata, and monadic second-order logic (MSO), then extends the automata-logic bridge to omega-words, Buchi/parity/Rabin/Streett/Muller acceptance, determinisation, alternating automata, LTL model checking, finite and infinite tree automata, parity games, CTL*, modal logic, and the modal mu-calculus.

Key Claims

• Automata theory and logic are deeply interchangeable specification languages: many logical definability questions can be reduced to automata decision problems.
• Over finite words, regular languages are exactly the MSO-definable languages.
• Automata translations give decidability procedures for logical satisfiability, validity, and equivalence, but not always with practical complexity.
• Infinite-word properties require acceptance conditions such as Buchi, co-Buchi, parity, Rabin, Streett, or Muller conditions; the choice changes determinisation, complementation, and decision-problem workflows.
• LTL model checking is naturally automata-theoretic: a transition-system trace language is intersected with an automaton for the negated specification, and correctness reduces to emptiness.
• Parity games provide the game-theoretic core behind automata on infinite trees and richer branching-time logics.

Methods / Formalism

• Regular languages over finite words are introduced by regular expressions and NFA/DFA, with closure properties and standard decision problems such as word, emptiness, universality, inclusion, and equivalence.
• MSO over finite words is related to finite automata in both directions:
  • an NFA run can be encoded by second-order state-position sets;
  • an MSO formula can be normalized and translated into an NFA over multi-track encodings of variable assignments.
• The central finite-word correspondence is:

$$L\subseteq {\Sigma }^{+}\text{ is regular iff }L\text{ is MSO-definable}.$$

• Infinite words are handled with omega-regular expressions and automata with Buchi-style acceptance. Later chapters compare Buchi, co-Buchi, parity, Rabin, Streett, Muller, and transition-based acceptance.
• LTL is interpreted over infinite words over 2^P; X, U, F, and G describe next, until, eventually, and always. LTL is translated to Buchi automata and very weak alternating Buchi automata.
• For finite labelled transition systems T and LTL formula phi, model checking is reduced to:

$$L(T)\subseteq L(\varphi )\text{iff}L(T)\cap L(\neg \varphi )=\varnothing .$$

• See MSO Automata Correspondence for the finite-word automata/MSO construction that underlies many later translations.

Evidence / Experiments

• This is a textbook, not an empirical paper. Its evidence is proof-theoretic and constructive: definitions, closure constructions, translations, decidability reductions, worked examples, bibliographic notes, and exercises.
• The table of contents spans finite words, infinite words, trees, parity games, and logics on infinite trees, giving the wiki a single reference point for the shared technical background behind LTL model checking, omega-automata, and tree-automata arguments.
• The LTL chapter gives a direct program-verification application: finite labelled transition systems are converted to weak nondeterministic Buchi automata, LTL formulas to Buchi automata, and model checking becomes an emptiness test for their product.

Connections

• Seeds Automata-Theoretic Logic as the broad concept connecting automata recognizers and logical definability.
• Supports Linear Temporal Logic by making explicit the automata-theoretic route from temporal formulas to model checking.
• Supports Safety and Co-Safety Properties and Safety LTL Automata and Games by placing finite-prefix safety automata in the larger omega-automata setting.
• Supports Emerson-Lei Objectives and Emerson-Lei Game Solving through the shared parity/Rabin/Streett/Muller acceptance and parity-game background.
• Complements Automata Learning: learned automata in RL inherit their semantics from the finite-automata and regular-language theory treated here.
• Belongs in Formal Methods and Temporal Logic as a foundation reference for verification, synthesis, monitoring, and automata-based specification.

Open Questions

• Should the wiki split out separate concept pages later for monadic second-order logic, Buchi automata, parity games, and tree automata?
• Which future ingests should cite this as background rather than recreating automata-theoretic definitions inside source notes?
• How much of the book’s tree-automata and modal mu-calculus material should be surfaced now versus waiting for a source that actively uses those tools?

Citation

Hofmann, M., and Lange, M. (2025). Automata Theory and Logic. Springer Vieweg. https://doi.org/10.1007/978-3-662-72154-4