Large Induced Subgraphs Via Triangulations and CMSO

Many classical graph problems consist in finding a maximum induced subgraph with some property. We can cite the Maximum Independent Set, Maximum Induced Forest, Longest Induced Path, Maximum Induced Matching, etc. We generalize them through the following optimization problem.
Let φ be a Counting Monadic Second Order Logic formula and t be an integer. Given a graph G=(V,E), the task is to find a maximum induced subgraph G[F] of treewidth at most t, that models φ.  Using the theory of potential maximal cliques, we show that the general problem ant thus all the particular cases can be solved 
in polynomial time for classes of graphs with polynomially many minimal separators, and in time O(1.7347^n) for arbitrary graphs.