Model Checking for Successor-Invariant FO on Minor-Closed Graph Classes

Kord Eickmeyer

We show that the model checking problem for successor-invariant first-order logic is fixed-parameter tractable on every class of graphs excluding some minor. This extends a result by Engelmann et al., who showed tractability on planar graphs. Our proof method differs fundamentally from the one in Engelmann et al., and we obtain a much shorter proof for the special case of planar graphs.

This is joint work with Ken-ichi Kawarabayashi and Stephan Kreutzer.