Monadic logic and automata: recent developments

This tutorial surveys selected recent results on the connection between monadic second-order logic and finite automata. As a unifying idea, the role of automata as normal forms of monadic formulas is pursued. In the first part we start from an automata-theoretic interpretation of existential monadic second-order formulas and in this framework explain the monadic quantifier alternation hierarchy over finite graphs. In the second part, infinite models, in particular ω-words, are considered. We analyze the logical significance of central constructions in ω-automata theory and sketch new proofs of decidability results in monadic second-order logic