wiki

MSO Automata Correspondence

2 min read

MSO Automata Correspondence

Context

Hofmann2025 - Automata Theory and Logic treats the finite-word MSO/automata equivalence as the first major bridge between logic and automata. The same proof idea recurs throughout verification: logical structure becomes automata structure, and automata decision problems become logical decision procedures.

Formal Statement

For finite non-empty words over alphabet Sigma:

Equivalently, regular expressions, NFA/DFA, and MSO sentences define the same class of finite-word languages.

Given an NFA

the automata-to-logic direction introduces one second-order variable X_q per state q. The formula asserts:

  • uniq(X): each word position carries exactly one state label;
  • init(X): the first position matches a transition out of q_I;
  • run(X): adjacent state labels respect delta;
  • acc(X): the final position is labelled by a state in F.

The logic-to-automata direction encodes assignments for free second-order variables as extra 0/1 tracks on the word. Atomic normalized MSO formulas have small NFA; disjunction uses union, negation uses complement, and existential second-order quantification uses alphabet-track projection.

Derivation / Construction

Automata to MSO:

  1. Take an accepting run of an NFA and represent the run by sets of positions labelled with each state.
  2. Write an MSO formula whose existentially quantified state-position sets satisfy uniqueness, initialization, transition consistency, and final acceptance.
  3. A word satisfies the formula iff the NFA has an accepting run on it.

MSO to automata:

  1. Normalize first-order variables into singleton second-order variables.
  2. View an interpretation (w,I) as a multi-track word over Sigma x {0,1}^n.
  3. Build NFA for the normalized atomic formulas.
  4. Use automata closure under union/complement for Boolean structure.
  5. Use projection of a variable track to model existential second-order quantification.

This construction yields decidability of MSO satisfiability and equivalence by reducing them to automata non-emptiness and equivalence. The construction is effective but can incur non-elementary blowup for MSO formulas.

Implications

The correspondence explains why automata appear as verification backends for logical specification languages. It also cautions against treating decidability as practicality: direct MSO-to-automata translation may be far too large, which is why fragments such as Linear Temporal Logic and safety/co-safety logics get specialized translations and algorithms.

Graph View

Backlinks