Model Checking for Successor-Invariant First-Order Logic on Minor-Closed Graph Classes

Model checking problems for first- and monadic second-order logic on graphs have received considerable attention in the past, not the least due to their connections to problems in algorithmic graph structure theory. While the model checking problem for these logics on general graphs is computationally intractable, it becomes tractable on important classes of graphs such as those of bounded tree-width, planar graphs or more generally, classes of graphs excluding a fixed minor. It is well known that allowing an order relation or successor function can greatly increase the expressive power of the respective logics. This remains true even in cases where we require the formulas to be order- or successor-invariant, that is, while they can use an order relation, their truth in a given graph must not depend on the particular ordering or successor function chosen. Naturally, the question arises whether this increase in expressive power comes at a cost in terms of tractability on specific classes of graphs. In LICS 2012, Engelmann et al. studied this problem and showed that order-invariant monadic second-order logic (MSO) remains tractable on the same classes of graphs than MSO without an ordering. That is, adding order-invariance to MSO essentially comes at no extra cost in terms of model checking complexity. For successor-invariant first-order logic something similar should be true. However, they only managed to show that successor-invariant first-order logic is tractable on the class of planar graphs which is very far from the best tractability results currently known for first-order logic. In this paper we significantly improve the latter result and show that successor-invariant first-order logic is tractable on any class of graphs excluding a fixed minor. This is much closer to the best results known for FO without an ordering. The proof relies on the construction of k-walks in suitable supergraphs of the input graphs, i.e., walks which visit every vertex at least once and at most k times, for some k depending on the excluded minor H. The supergraphs may in general contain H minors, but they still exclude some possible larger minor H', so by results of Flum and Grohe [20] model checking on these graphs is still fixed-parameter tractable.