Open problems suggested by Bruno Courcelle during the workshop
For definitions, see the slides
of the talk or
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
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?