Open problems suggested by Bruno Courcelle during the workshop
For definitions, see the slides
of the talk or
http://www.labri.fr/~courcell/ActSci.html
1. Conjecture (Seese) : If C is a class of finite graphs for which
the satisfiability problem for monadic second-order logic (MS logic) is decidable,
then this class is the image of a set T of finite trees under a monadic second-order
transduction, equivalently C has bounded clique-width.
Reference: D. Seese, The structure of the models of decidable monadic
theories of graphs, Ann. Pure Appl. Logic 53 (1991) 169-195.
Observation: For proving Seese's Conjecture, one need to find a monadic
second-order compatible graph transformation S and a function f such that,
for every graph G, if G has clique-width more than f(k), then S(G) is a k
x k square grid.
2. A stronger conjecture: If C and T are as above, then T is also
the image of C under a monadic second-order transduction. Hence a decision
algorithm for the satisfiability problem for MS logic in graphs of C can
be derived from one for T and vice-versa.
3. Reductions between specific cases
Let C and D be two classes of graphs.
We write C => D, if one can prove the conjecture for all subsets of D
assuming it is proved for all subsets of C.
Do we have "finite graphs" => "countable graphs" (the conjecture
is actually stated by D. Seese for finite and infinite graphs) ?
Do we have "finite graphs" => "finite relational structures with
relations of arity more than 2" ?
4. Which structure transformations are monadic second-order compatible
(MS compatible)?
The following transformations are known to be MS compatible : MS transductions,
the Shelah-Stupp-Muchnik tree expansion.
Compositions of MS compatible transformations are MS compatible. (Unfolding
is a composition of an MS -transduction and a tree-expansion.)
Question: Can one find MS-compatible transformations that cannot be
obtained as finite compositions of transformations of the above two basic
forms.
5. For a Noetherian and confluent term rewriting system, the normal form
mapping goes from finite terms to finite terms .
When is it an MS-transduction ? When is it MS-compatible?