It is also of fundamental importance in automata theory, where the Büchi–Elgot–Trakhtenbrot theorem gives a logical characterization of the regular languages.
In the variant considered in automata theory and the Büchi–Elgot–Trakhtenbrot theorem, all predicates, including those in the formula itself, must be monadic, with the exceptions of equality (
By analogy to Fagin's theorem, according to which existential (non-monadic) second-order logic captures precisely the descriptive complexity of the complexity class NP, the class of problems that may be expressed in existential monadic second-order logic has been called monadic NP.
For MSO formulas that have free variables, when the input data is a tree or has bounded treewidth, there are efficient enumeration algorithms to produce the set of all solutions,[6] ensuring that the input data is preprocessed in linear time and that each solution is then produced in a delay linear in the size of each solution, i.e., constant-delay in the common case where all free variables of the query are first-order variables (i.e., they do not represent sets).
There are also efficient algorithms for counting the number of solutions of the MSO formula in that case.
The monadic second-order theory of the infinite complete binary tree, called S2S, is decidable.
Decision procedures for MSO satisfiability[10][11][12] have been used to prove properties of programs manipulating linked data structures,[13] as a form of shape analysis, and for symbolic reasoning in hardware verification.