Monadic second-order logic on infinite words and trees - Křetínský, Jan, 1984- (2007)
We present one of the fundamental results on the automata theory, namely the correspondence between finite automata recognizability and monadic second--order logic definability. The types of languages concerned are mainly those of infinite words and trees. As a corollary, we show the monadic second--order logics with one and two successors to be decidable. These results are due to Büchi (1962) and Rabin (1969). We also illustrate the theory by our original examples.