# What is the parameterized complexity of following model checking problem?

Input: Graph $G$ and formula $\varphi_1(\vec x),\varphi_2(\vec x)$

Parameter: $tw(G)+|\varphi_1|+|\varphi_2|$

Problem: Decide if $|\varphi_1(G)|=|\varphi_2(G)|$

where $tw(G)$ is the treewidth of $G$ and $\varphi(G):=\{\vec a|(G,\vec a)\models\varphi\}$.

What is the parametrized complexity of this problem for $\varphi_i\in FO$ or $\varphi_i\in MSO$?

• What is tw(G) ? – Sylvain Peyronnet Jan 12 '11 at 9:52
• @Sylvain: maybe the treewidth of a graph? – Hsien-Chih Chang 張顯之 Jan 12 '11 at 10:02
• @Sylvain: Sorry, I added the explanation. – Regularity Jan 12 '11 at 10:34
• Pardon my ignorance, but what is the meaning of "the absolute value of a formula applied to a graph" : $\vert \varphi_{1}(G)\vert$ ? – gphilip Jan 12 '11 at 12:00
• I guess it is the number of good assignments. – Mathieu Chapelle Jan 12 '11 at 12:05

This problem is $\mathsf{FPT}$ for $\varphi_i \in MSO$ (and hence also for $\varphi_i \in FO$).

More precisely, Courcelle et al. prove in [1] the following:

Theorem [1, Thm. 32]
Let $\mathcal{C}$ be a class of graphs which is of bounded tree-width $k$.
Then any $MSO_2$ definable counting problem, given by $\varphi$, can be solved in time $c_k \cdot \mathcal{O}(|V| + |E|)$, where $c_k$ is a constant which depends only on $\varphi$ and $k$.

$MSO_2$ stands for monadic second-order logic where the universe is $V \cup E$ (vertices and edges), and we are given a binary relation $R(v,e)$ for the incidence between a vertex $u$ and an edge $e$. This is a quite natural representation of graphs, sufficiently powerful to e.g. define Hamiltonicity.

• I am not sure, if I remember well this paper is about bounded tree width structure, which is not the case here. – Sylvain Peyronnet Jan 12 '11 at 12:26
• In this paper (and usually in parameterized complexity), "bounded measure" means "as parameter". I should precise that Theorem 32 in this paper precisely states that any $MSO_2$ formula $\varphi$ can be decided on an input graph $G$ in $\mathcal{O}\big(f(tw(G),\varphi) \cdot |G|\big)$ time. – Mathieu Chapelle Jan 12 '11 at 15:00
• So, my mistake then, sorry. – Sylvain Peyronnet Jan 12 '11 at 22:41