What is the parameterized complexity of following model checking problem?
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)