Lecture Notes on Monadic First- and Second-Order Logic on Strings

TL;DR

This paper explains monadic first- and second-order logics on strings, showing their expressive power, relationships with automata, and applications in automatic verification, highlighting the differences and connections between these logical systems.

Contribution

It provides an introductory comparison of monadic first- and second-order logics on strings, including their expressive capabilities and automata translations.

Findings

Monadic First-Order logic captures only non-counting regular languages.

Monadic Second-Order logic captures all regular languages.

Automata can be transformed into logical formulas and vice versa.

Abstract

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.