On a conjecture by D. Seese

B. Courcelle,
Labri, Bordeaux-1 University, France


In order to obtain decidability results for logical theories, one may restrict the language and/or the class of structures under consideration.
Among the logical languages for which decidability results can be obtained without restrictions on the structure of quantifications, Monadic Second-order Logic (the extension of First-order Logic with quantified variables denoting subsets of the domain) is a favorite one.
All decidability results concerning it are based on the equivalence between  Monadic Second-order formulas and finite-state automata, a fundamental result established by M. Rabin for infinite trees, that subsumes
the special cases of infinite words and of finite binary trees established previously by other authors.
The decidability problem for MS logic (MS abreviates Monadic Second-order) on a  class of structures C
can be stated as follows:

        Does there exist an algorithm that, for every MS formula over the relevant vocabulary,
        says whether it holds in some structure of the class C (or equivalently, since MS logic is
        closed under negation, in all structures of the considered class)?

(A class may consist of a single infinite structure. The problem is trivial  for a finite class of finite structures.)
From Rabin's theorem and the existence of an emptyness algorithm for sets of trees defined by finite-state tree automata, it follows that MS logic is decidable on  the infinite binary tree and on  the class of all finite binary trees. A suitable adaptation of the "interpretation method" makes it possible to extend this decidability result to  classes of structures that can be constructed from trees. Such structures are said to
be "interpretable in trees" or constructed from trees by MS definable transductions.
Hence, if a class of structures is interpretable in a class of trees having a decidable MS theory, then it has a decidable MS theory. The corresponding transformation of structures is said to be MS-compatible.

D. Seese formulated in 1991  the conjecture that, conversely, if a class of structures has a decidable MS theory, then it is interpretable in a class of trees.
A stronger  form of this conjecture would require that such a class of structures is interpretable in a class of trees having a decidable MS theory.

D. Seese proved this conjecture for every class of planar graphs and for every class  of incidence graphs. (The class of all finite planar graphs has an undecidable  MS theory because one can build large square grids inside large planar graphs).
More precisely, every class of planar graphs having a decidable  MS theory has bounded tree-width, hence is obtained from trees by an MS transduction.
If a class of graphs is such that the class of its incidence graphs has a decidable MS theory, then it also has bounded tree-width, and by a result of D. Lapoire, the strong form of Seese's conjecture holds in these two cases.
However, the conjecture is still open in its full generality.

This lecture will present:
- alternative formulations of Seese's conjecture in terms of clique-width, another complexity measure for graphs, more powerful than tree-width,
- the special cases established so far (and the  techniques behind these proofs),
- a discussion of some reductions of the conjecture to special cases, like that of finite undirected graphs.

It  will also consider the following extension of Seese's conjecture  formulated as a question:

Which transformations of structures are MS compatible?

The  known  MS compatible  transductions are  MS transductions, unfoldings, the "tree construction"  of Shelah-Stupp-Muchnik-Walukiewicz, and their compositions. Are there others?


D. Seese: The structure of the models of decidable monadic theories of graphs,  Annals of Pure and Applied Logic, 53 (1991) 169-195.

B. Courcelle, I. Walukiewicz,  Monadic second-order logic, graph coverings and unfoldings of transition systems, Annals of Pure and Applied Logic, 92 (1998) 35-62.

B. Courcelle: The monadic second-order logic of graphs XIV:  Uniformly sparse graphs and edge set quantifications. To appear in Theoretical Computer Science.

B.Courcelle: A monadic second-order definition of the structure of convex hypergraphs, september 1999,
to appear in Information and Computation,

D. Lapoire:Recognizability equals Monadic Second-order definability for sets of graphs of bounded tree-width, STACS 1998, LNCS 1373, pp.618-628.

I. Walukiewicz: Monadic Second order logic on tree-like structures, STACS, 1996, LNCS 1046, pp. 401-414.