Minor closed properties that are explicitly MSO expressible

Question

Below, MSO denotes the monadic second order logic of graphs with vertex-set and edge-set quantifications.

Let $\mathcal{F}$ be a minor closed family of graphs. It follows from Robertson and Seymour's graph minor theory that $\mathcal{F}$ is characterized by a finite list $H_1,H_2,...,H_k$ of forbidden minors. In other words, for each graph $G$, we have that $G$ belongs to $\mathcal{F}$ if and only if $G$ excludes all graphs $H_i$ as minors.

As a consequence of this fact, we have an MSO formula $\varphi_{\mathcal{F}}$ which is true on a graph $G$ if and only if $G\in \mathcal{F}$. For instance, planar graphs are characterized by the absence of the graphs $K_{3,3}$ and $K_5$ as minors, and therefore it is easy to write explicitly an MSO formula characterizing planar graphs.

The problem is that for many nice minor closed graph properties, the list of forbidden minors is unknown. So, while we know that an MSO formula characterizing that family of graphs exist, we may not know what this formula is.

On the other hand, it may be the case that one is able to come up with an explicit formula for a given property without using the graph minor theorem. My question is related to this possibility.

Question 1: Is there a minor closed family of graphs $\mathcal{F}$, such that the set of forbidden minors is not known, but some MSO formula $\varphi$ characterizing that set of graphs is known?

Question 2: Is some explicit MSO formula $\varphi$ known to characterize some of the following properties?

1. Genus 1 (the graph is embeddable in a torus) (see EDIT below)
2. Genus k for some fixed $k>1$ (see EDIT below)
3. k-outerplanarity for some fixed $k> 1$

I would appreciate any reference or thoughts on this matter. Please feel free to consider other minor closed properties, the list given above is only illustrative.

Obs: By explicit I do not mean necessarily small. It is enough to give an explicit argument or algorithm showing how to construct the formula characterizing the given property. Similarly, in the context of this question I consider a family of forbidden minors to be known if one has given an explicit algorithm constructing that family.

EDIT: I found a paper by Adler, Kreutzer, Grohe which constructs a formula characterizing graphs of genus $k$ with basis on the formula characterizing graphs of genus k-1. So this paper answers the first two items of Question 2. On the other hand this does not answer Question 1 because there is indeed an algorithm that constructs for each k, the family of forbidden minors characterizing graphs of genus k (See section 4.2). Therefore this family is "known" in the sense of the question.

Answer 1

I had an answer here involving apex graphs but it fails the definition of not having an explicit obstruction set given in this question: there is a published algorithm for finding the obstruction set, even though is too slow to run so we don't actually know what the obstruction set is.

So here's another parameterizable family of answers without that flaw (at least, as far as I know). Given a minor closed family $F$, and an integer $k\ge 1$, does the given graph $G$ have a $k$-ply covering graph in $F$? Much about this sort of question remains unknown: in particular, Negami's conjecture, which would characterize the graphs that have a planar covering graph, remains unproven. And it's minor-closed because any steps that you take to make a minor from $G$ can be copied in the cover.

To test for the existence of a $k$-ply cover of $G$ in $F$, in MSO$_2$, do the following steps:

• Use the depth-first-search-tree trick to get an (arbitrary) orientation of $G$.
• For each pair $(i,j)$ with $0\le i,j<k$, choose a set of edges in $G$, supposedly the ones that have a covering edge that goes from ply $i$ to ply $j$.
• Check that each vertex in each ply has exactly one copy of each incident edge, and thus that this information represents a valid covering graph of $G$.
• Emulate the obstruction set based formula for membership in $F$ on the covering graph.