# MSO

## Monadic second-order logic with cardinality predicates ★★

Author(s): Courcelle

The problem concerns the extension of Monadic Second Order Logic (over a binary relation representing the edge relation) with the following atomic formulas:

\item \item

where is a fixed recursive set of integers.

Let us fix and a closed formula in this language.

Conjecture   Is it true that the validity of for a graph of tree-width at most can be tested in polynomial time in the size of ?

## Order-invariant queries ★★

Author(s): Segoufin

Question
\item Does hold over graphs of bounded tree-width? \item Is included in over graphs? \item Does have a 0-1 law? \item Are properties of Hanf-local? \item Is there a logic (with an effective syntax) that captures ?