Büchi-Elgot-Trakhtenbrot theorem explained

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

Notes and References

1. Büchi . Julius Richard . Weak second order arithmetic and finite automata . Zeitschrift für Mathematische Logik und Grundlagen der Mathematik . 1960 . 6 . 1–6 . 66–92. 10.1002/malq.19600060105 .
2. Elgot . Calvin C. . Decision problems of finite automata design and related arithmetics . . 1961 . 98 . 21–52. 10.1090/S0002-9947-1961-0139530-9 . 119721061 . free . 2027.42/4758 . free .
3. Trakhtenbrot . Boris A. . Конечные автоматы и логика одноместных предикатов . Russian . Finite automata and the logic of one-place predicates . Siberian Mathematical Journal . 1962 . 3 . 103–131.
4. Trakhtenbrot . Boris A. . Finite automata and the logic of one-place predicates . American Mathematical Society Translations . American Mathematical Society Translations: Series 2 . 1966 . 59 . 23–55. 10.1090/trans2/059/02 . 9780821817599 .