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, Calvin Elgot, and Boris Trakhtenbrot.

• Trakhtenbrot's theorem
• Courcelle's theorem