Model checking separator logic on graphs that exclude a fixed topological minor.

We consider separator logic on graphs introduced recently by Bojańczyk, and independently by Siebertz, Shrader, and Vigny. This logic extends first-order logic by atomic predicates of arity k+2, for each k, expressing that every path from a vertex s to a vertex t must pass through one of the vertices v_1,...,v_k. We prove that the model checking problem for this logic is fixed parameter tractable on every class of graphs that excludes a fixed topological minor. To this end, we decompose each graph from such a class in a treelike fashion and run a variant of a tree automaton on the obtained tree decomposition. This is joint work with Siebertz, Shrader, Mi. Pilipczuk, and Vigny.