MSO = regular (the logic ↔ automata bridge)

Parent: regular-equivalences

Regular languages are exactly the ones you can describe in a logic — the deepest of the coincidences, and the foundation of model checking.

Monadic second-order logic (MSO)

The ladder is what you may quantify over:

first-order (FOL) — over elements (∀x, ∃x);

second-order (SO) — over relations of any arity (∀R, ∀f) — very strong, generally undecidable;

MSO — second-order restricted to unary relations, i.e. sets: ∀X, ∃X over subsets, with membership x ∈ X.

So MSO = FOL + quantification over sets, strictly between FOL and full SO. Over strings, trees, and ⟨ℕ,<⟩ it stays decidable (translate to automata) — unlike full SO — and over the infinite binary tree it is Rabin's S2S.

Instantiated on strings:

MSO over strings

View a string as a structure: positions 1…n, the order <, and a predicate Qₐ(x) = "position x holds letter a". Monadic second-order logic (MSO) adds, to first-order logic, quantifiers over sets of positions (∃X. …).

Büchi–Elgot–Trakhtenbrot (1960)

A language is regular iff it is MSO-definable.

Why (sketch). A run of a k-state automaton is a colouring of the positions by states; "there is an accepting run" = "there exist sets X₁…Xₖ (put position i into the set for whichever state q the run occupies there) satisfying the local transition constraints and ending accepting." That's an MSO sentence (the set quantifiers do the work). Conversely, each MSO connective/quantifier is matched by an automaton operation (union, product, projection, complement), building an automaton from any formula.

Why it matters

This is the logic ↔ automata correspondence: a specification (formula) can be compiled to a machine (automaton) and checked. Extended to infinite words it becomes Büchi automata and temporal logic (LTL) — the theory behind model checking. Same theme as Curry–Howard's proofs=programs: here, specifications = machines.