Büchi–Elgot–Trakhtenbrot theorem

In formal language theory, the Büchi–Elgot–Trakhtenbrot theorem states that a language is regular if and only if it can be defined in monadic second-order logic (MSO): for every MSO formula, we can find a finite-state automaton defining the same language, and for every finite-state automaton, we can find an MSO formula defining the same language. The theorem is due to Julius Richard Büchi,^[1] Calvin Elgot,^[2] and Boris Trakhtenbrot.^[3][4]

See also

• Trakhtenbrot's theorem
• Courcelle's theorem