  These notes present the essentials of first- and second-order monadic logics
on strings with introductory purposes. We discuss Monadic First-Order logic and
show that it is strictly less expressive than Finite-State Automata, in that it
only captures a strict subset of Regular Languages -- the non-counting ones. We
then introduce Monadic Second-Order logic; such a logic is, syntactically, a
superset of Monadic First-Order logic and captures Regular Languages exactly.
We also show how to transform an automaton into a corresponding formula and
vice versa. Finally, we discuss the use of logical characterizations of classes
of languages as the basis for automatic verification techniques.
