Monadic Second-Order Logic with Arbitrary Monadic Predicates

TL;DR

This paper explores Monadic Second-Order Logic extended with arbitrary monadic predicates over finite words, providing algebraic and automata-theoretic characterizations, and addressing regularity and decidability questions.

Contribution

It introduces a comprehensive framework for MSO with arbitrary monadic predicates, proving key conjectures and establishing decidability results.

Findings

MSO with monadic predicates characterizes a broad class of languages.

The Straubing and Crane Beach Conjectures hold for all fragments of MSO with monadic predicates.

Decidability of language regularity from MSO formulas with morphic predicates is established.

Abstract

We study Monadic Second-Order Logic (MSO) over finite words, extended with (non-uniform arbitrary) monadic predicates. We show that it defines a class of languages that has algebraic, automata-theoretic and machine-independent characterizations. We consider the regularity question: given a language in this class, when is it regular? To answer this, we show a substitution property and the existence of a syntactical predicate. We give three applications. The first two are to give very simple proofs that the Straubing Conjecture holds for all fragments of MSO with monadic predicates, and that the Crane Beach Conjecture holds for MSO with monadic predicates. The third is to show that it is decidable whether a language defined by an MSO formula with morphic predicates is regular.