B.
Courcelle,
Labri, Bordeaux-1
University, France
courcell@labri.fr
Abstract:
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 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?
References:
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.