# Minor closed properties that are explicitly MSO expressible

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.

• Any forbidden minor class can be expressed by forbidding an infinite number of subgraphs for each of the finitely many forbidden minors. You are therefore asking: is there a minor-closed graph class such that the (implicitly existing) infinite MSO definition that one by one forbids each of these infinitely many subgraphs can be replaced by a finite MSO formula (that we know explicitly)? Hadwiger's Conjecture has this form, for each $k$, since $(k-1)$-colourability is expressible by a finite MSO formula. If the conjecture is true then these are the $K_k$-minor-free graphs, but this is open. – András Salamon Jan 13 '16 at 2:40
• I would think that embeddability on the torus can be expressed explicitly as “the graph can be split in two planar pieces” or something of that sort, and similarly for higher genera. – Emil Jeřábek Jan 13 '16 at 11:08
• Thanks for the suggestion Emil. I found a paper that constructs the formula characterizing graphs of genus k with basis on the formula characterizing graphs of genus k-1. This does not answer my question on the other hand. See the edit. – Mateus de Oliveira Oliveira Jan 13 '16 at 13:26
• @AndrásSalamon — it's easy to express a forbidden minor in an explicit and finite MSO expression. The issue is that we don't necessarily know which minors to forbid. – David Eppstein Jan 13 '16 at 15:06
• @DavidEppstein: ah, missed that: thanks, so the first part of my comment can be simplified. However, $k$-Hadwiger's still seems to answer Q1? We have a hypothesised singleton set of minors $\{K_k\}$ for each $k$, but "only" lack a proof that $\{K_k\}$-minor-free is the same class as that defined by the MSO formula $\phi_k =$ "$(k-1)$-colourable". – András Salamon Jan 13 '16 at 17:05

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.
• David, if I'm not missing something, Adler-Kreutzer-Grohe-2008 gave an algorithm that computes an excluded minor characterization for appex-C provided you give as input the minor characterization for the class C. But this algorithm may be too inefficient. I think that Addler hopes that the list of excluded minors for appex-PLANAR is small and therefore she is asking for an explicit list, because it would be too complicated to construct it using their algorithm. I'm interested in an a property for which the MSO formula is known, but no algorithm for constructing the minors is known. – Mateus de Oliveira Oliveira Jan 15 '16 at 6:33
• Is it true for any minor-closed class C that the class of graphs having a cover in C is minor-closed? – Denis Feb 1 '16 at 15:57
• Yes. See the sentence already in my answer about "And it's minor-closed because...". – David Eppstein Feb 1 '16 at 17:00
• thanks for the new answer. I didn't see that the answer had been edited until now. – Mateus de Oliveira Oliveira Apr 18 '16 at 21:45