Automatic Structures

Origin. Bernard R. Hodgson, "Décidabilité par automate fini" (Annales des sciences mathématiques du Québec 7, 1983, 39–57), developing his thesis "Théories décidables par automate fini" (Université de Montréal, 1976), defined structures whose relations are recognized by finite automata and proved their first-order theories decidable; the work went unnoticed through the 1980s. Bakhadyr Khoussainov and Anil Nerode, "Automatic presentations of structures" (Logic and Computational Complexity workshop, Indianapolis 1994; LNCS 960, 1995, 367–392), rediscovered the notion and began the systematic theory. Achim Blumensath and Erich Grädel, "Automatic structures" (LICS 2000, 51–62), the third independent formalization, added the ω-automatic case, the characterization by first-order interpretations, and the non-automaticity of Skolem arithmetic and the divisibility order.

Models. A structure presented by finite automata: a regular language of words names the elements, and automata reading the names synchronously, one symbol per tape, recognize name-equality and each atomic relation. The restriction's purpose is effectivity. Recursive structures admit effective evaluation, in general, only of quantifier-free queries; automatic structures keep effective semantics for all of first-order logic, because regular relations are closed under Boolean combinations and projection — the same closure that proves Büchi's theorem (see Buchi Automata.md). Blumensath and Grädel framed the class as the extension of finite model theory's program to infinite structures (see Finite Model Theory.md), and it is the setting in which the automata–arithmetic correspondences become presentations: Presburger arithmetic presented in base k, and Büchi arithmetic ⟨ℕ, +, V_k⟩ as the exact logical measure of base-k recognizability (see Presburger Arithmetic.md).

Formalism.

Presentation: A = (A, R₁, …, Rₘ) is automatic iff there are a regular L ⊆ Σ* and a surjection ν : L → A such that {(u, v) : ν(u) = ν(v)} and each ν⁻¹(Rᵢ) are regular relations.

Convolution: conv(w₁, …, wₙ) interleaves the words position by position, padding exhausted words with #; a relation is regular iff its convolution language is — the synchronous n-tape automaton.

Fundamental theorem (Khoussainov–Nerode 1995; decidability already Hodgson 1983): From a presentation of A and a first-order φ(x̄), an automaton recognizing {ā : A ⊨ φ(ā)} is computable. Hence Th(A) is decidable, uniformly in the presentation; per fixed formula, query evaluation is linear time. Corollary: anything first-order definable in an automatic structure, with parameters, is again automatic.

Extended quantifiers: the theorem persists for FO + ∃^∞ + ∃^(n,m) — the infinity quantifier (Blumensath 1999; algorithm in Blumensath–Grädel 2000) and the modulo-counting quantifiers (Khoussainov–Rubin–Stephan, "Definability and regularity in automatic structures", STACS 2004, LNCS 2996, 440–451).

Complete structure (Blumensath–Grädel 2000): A is automatic iff A is first-order interpretable in N_p = ⟨ℕ, +, |_p⟩ for some (equivalently every) p ≥ 2, where x |_p y iff x is a power of p dividing y. Automatic structures = the interpretation closure of one decidable structure.

Canonical examples: ⟨ℕ, +⟩: least-significant-digit-first base-k names; the carry makes addition a small automaton. ⟨ℕ, +, V_k⟩, Büchi arithmetic: V_k(x) = the largest power of k dividing x. Büchi–Bruyère theorem: X ⊆ ℕⁿ is k-recognizable iff definable in ⟨ℕ, +, V_k⟩ (survey: Bruyère–Hansel–Michaux–Villemaire, "Logic and p-recognizable sets of integers", Bull. Belg. Math. Soc. 1, 1994, 191–238). Definable in ⟨ℕ, +⟩ iff recognizable in every base — the hard direction is Cobham–Semenov. Also automatic: the ordinals below ω^ω, binary strings with prefix and equal-length, configuration graphs of Turing machines.

Growth lemma (Khoussainov–Nerode 1995; Blumensath 1999): an automatic function adds at most a constant to the length of its longest argument, so n generations from a linearly-spaced seed stay within length C·n. Consequences: the free semigroup on two generators, free groups of rank > 1, pairing bijections ω × ω → ω, and ⟨ℕ, ×⟩ are not automatic.

Generalizations (named by the presenting automaton): ω-automatic — Büchi automata over infinite words (Blumensath–Grädel 2000), reaching uncountable domains such as ⟨ℝ, +⟩; tree-automatic — automata over finite trees (Blumensath 1999), where ⟨ℕ, ×⟩ is presentable; Rabin automata over infinite trees for the ω-tree case (see Rabin Tree Theorem.md).

Symbols.

Metatheory. The fundamental theorem is uniform twice over: one algorithm serves every automatic structure and every formula, and it extends to ∃^∞ and the modulo-counting quantifiers without losing decidability. The negative results fix the class's size. Khoussainov, Nies, Rubin, and Stephan, "Automatic structures: richness and limitations" (LICS 2004; LMCS 3(2), 2007), proved that the random graph has no automatic presentation (see Random Graph.md) and that no infinite integral domain has one; Christian Delhommé, "Automaticité des ordinaux et des graphes homogènes" (C. R. Acad. Sci. Paris Sér. I 339, 2004, 5–10), proved in the same year that the random graph is neither automatic nor tree-automatic, that the automatic ordinals are exactly those below ω^ω, and that the tree-automatic ordinals are exactly those below ω^(ω^ω). The Khoussainov–Nies–Rubin–Stephan paper also fixed the complexity of classification: the isomorphism problem for automatic structures is Σ¹₁-complete, exactly as hard as for computable structures, so automaticity of the presentation does not lower it. Skolem arithmetic ⟨ℕ, ×⟩ and the divisibility poset ⟨ℕ, |⟩ are not automatic (Blumensath–Grädel 2000), and ⟨ℕ, ×⟩ becoming presentable one level up, by tree automata, locates the word/tree boundary.

Applies to. Infinite-state model checking, where state spaces and transitions of protocols, counter systems, and rewriting systems are regular. Automata-based decision procedures for Presburger and Büchi arithmetic. The theory of automatic groups, where the Thurston notion (automata for left multiplication by each generator) covers a wider class of finitely generated groups than automaticity of the group operation itself. Computable model theory, where automatic structures are the subclass with a decidable first-order theory rather than only a computable atomic diagram.

Limitations. The growth lemma caps every automatic function at constant length growth, so multiplication, exponentiation, pairing, and free group multiplication are excluded, and the automatic ordinals stop at ω^ω; since first-order interpretation preserves automaticity and every automatic theory is decidable, no structure with an undecidable first-order theory is interpretable in any automatic structure. Word-automatic domains are countable; reaching ⟨ℝ, +⟩ requires ω-automata. Decidability is uniform and effective, but each quantifier alternation passes through projection and complementation, and the complementation is a powerset construction, so the automata can grow by an exponential per alternation. And the Σ¹₁-completeness of isomorphism means the class supports no classification theory: deciding whether two presentations present the same structure is as hard as any analytic problem, although it becomes decidable on the subclass of automatic ordinals.

© 2026 Lingenic LLC