On model-theoretic approaches to monadic second-order logic evaluation
Φουστούκου, Ευγενία
Κοσμαδάκης, Σταύρος
Cosmadakis, Stavros
Foustoucos, Eugenie
--
We review the model-theoretic approaches to Monadic Second-Order Logic
(MSO) evaluation, especially to model-checking on MSOL-inductive classes
of structures.
Starting our study with finite strings and finite trees, we then focus
on classes of structures of bounded treewidth.
For these classes we define the ``model-theoretical automaton'' which
generalizes the corresponding automaton defined by Ladner for strings.
First we prove that the model-theoretical automaton cannot be used as an
MSO model-checking algorithm on any of these classes of structures.
Then we study its relationship with other classical model-theoretic
methods as well as its relationship with recent datalog-based
approaches to the MSO model-checking problem.
Technical Report
Monadic second-order logic (MSO) evaluation problem
