  A successor-invariant first-order formula is a formula that has access to an
auxiliary successor relation on a structure's universe, but the model relation
is independent of the particular interpretation of this relation. It is well
known that successor-invariant formulas are more expressive on finite
structures than plain first-order formulas without a successor relation. This
naturally raises the question whether this increase in expressive power comes
at an extra cost to solve the model-checking problem, that is, the problem to
decide whether a given structure together with some (and hence every) successor
relation is a model of a given formula. It was shown earlier that adding
successor-invariance to first-order logic essentially comes at no extra cost
for the model-checking problem on classes of finite structures whose underlying
Gaifman graph is planar [Engelmann et al., 2012], excludes a fixed minor
[Eickmeyer et al., 2013] or a fixed topological minor [Eickmeyer and
Kawarabayashi, 2016; Kreutzer et al., 2016]. In this work we show that the
model-checking problem for successor-invariant formulas is fixed-parameter
tractable on any class of finite structures whose underlying Gaifman graphs
form a class of bounded expansion. Our result generalises all earlier results
and comes close to the best tractability results on nowhere dense classes of
graphs currently known for plain first-order logic.
