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
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 C 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.