# 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: \begin{itemize} \item $\text{}\,\mathrm{Card}(X) = \mathrm{Card}(Y)\,\text{''}$ \item $\text{}\,\mathrm{Card}(X) \text{ belongs to } A\,\text{''}$ \end{itemize} where $A$ is a fixed recursive set of integers.

Let us fix $k$ and a closed formula $F$ in this language.

\begin{conjecture} Is it true that the validity of $F$ for a graph $G$ of tree-width at most $k$ can be tested in polynomial time in the size of $G$? \end{conjecture}

## Order-invariant queries ★★

Author(s): Segoufin

\begin{question} \begin{enumerate} \item Does ${<}\text{-invariant\:FO} = \text{FO}$ hold over graphs of bounded tree-width? \item Is ${<}\text{-invariant\:FO}$ included in $\text{MSO}$ over graphs? \item Does ${<}\text{-invariant\:FO}$ have a 0-1 law? \item Are properties of ${<}\text{-invariant\:FO}$ Hanf-local? \item Is there a logic (with an effective syntax) that captures ${<}\text{-invariant\:FO}$? \end{enumerate} \end{question}