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

<p>More precisely, Courcelle <em>et al.</em> prove in [1] the following:</p>

<blockquote>
  <p><strong>Theorem [1, Thm. 32]</strong><br>
  Let $\mathcal{C}$ be a class of graphs which is of bounded tree-width $k$.<br>
  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$.</p>
</blockquote>

<p>$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 <em>e.g.</em> define Hamiltonicity.</p>

<p>[1]: <a href="http://dx.doi.org/10.1016/S0166-218X%2800%2900221-3" rel="nofollow">B.Courcelle, J.A.Makowsky, U.Rotics. On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic. Discrete Applied Mathematics 108, pp. 23-52 (2001)</a></p>

CC BY-SA 2.5
2011-01-12T12:26:17.780Z
I am not sure, if I remember well this paper is about bounded tree width structure, which is not the case here.
Sylvain Peyronnet
CC BY-SA 2.5
2011-01-12T15:00:01.860Z
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
CC BY-SA 2.5
2011-01-12T22:41:31.393Z
So, my mistake then, sorry.
Sylvain Peyronnet
CC BY-SA 2.5
2011-01-12T12:03:30.640Z
2011-01-12T15:12:05.343Z
2011-01-12T15:12:05.343Z
Mathieu Chapelle
<hr>

<p>Input: Graph $G$ and formula $\varphi_1(\vec x),\varphi_2(\vec x)$ </p>

<p>Parameter: $tw(G)+|\varphi_1|+|\varphi_2|$</p>

<p>Problem: Decide if $|\varphi_1(G)|=|\varphi_2(G)|$</p>

<hr>

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

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

CC BY-SA 2.5
2011-01-12T09:52:42.500Z
What is tw(G) ?
Sylvain Peyronnet
CC BY-SA 2.5
2011-01-12T10:02:20.243Z
@Sylvain: maybe the treewidth of a graph?
Hsien-Chih Chang 張顯之
CC BY-SA 2.5
2011-01-12T10:34:18.767Z
@Sylvain: Sorry, I added the explanation.
Regularity
CC BY-SA 2.5
2011-01-12T12:00:46.617Z
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
CC BY-SA 2.5
2011-01-12T12:05:26.253Z
I guess it is the number of good assignments.
Mathieu Chapelle
<cc.complexity-theory><descriptive-complexity><parameterized-complexity><finite-model-theory><model-checking>
What is the parameterized complexity of following model checking problem?
Regularity
# What is the parameterized complexity of following model checking problem?

(Asked by: username_0 on 2011-01-12)

---

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$?

**Tags:** cc.complexity-theory, descriptive-complexity, parameterized-complexity, finite-model-theory, model-checking
> **Comments:**
> **username_1**: What is tw(G) ?  
> **username_2**: @Sylvain: maybe the treewidth of a graph?  
> **username_0**: @Sylvain: Sorry, I added the explanation.  
> **username_3**: Pardon my ignorance, but what is the meaning of "the absolute value of a formula applied to a graph" : $\vert \varphi_{1}(G)\vert$ ?  
> **username_4**: I guess it is the number of good assignments.  

---

## 1 answers

### Answer by username_4 on 2011-01-12. Score: 10 | Accepted answer

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.

[1]: [B.Courcelle, J.A.Makowsky, U.Rotics. On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic. Discrete Applied Mathematics 108, pp. 23-52 (2001)](http://dx.doi.org/10.1016/S0166-218X%2800%2900221-3)

> **Comments:**
> **username_1**: I am not sure, if I remember well this paper is about bounded tree width structure, which is not the case here.  
> **username_4**: 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.  
> **username_1**: So, my mistake then, sorry.  

---

