Journal of Multimedia Processing and Technologies Hongbin yuan, Chenyao yuan, Huiqun cao 16 3 2025 https://doi.org/10.6025/jmpt/2025/16/3/138-154 https://www.dline.info/jmpt/fulltext/v16n3/jmptv16n3_2.pdf This paper establishes that model checking for successor invariant first order logic (FO) is fixed parameter tractable on graph classes that exclude a fixed graph H as a topological subgraph. While model checking for plain FO is well understood on sparse graph classes, extending these tractability results to successor invariant FO where a successor relation is added but formulas must be invariant under its choice has been challenging. The authors extend prior results on planar and minor excluded graphs by proving tractability for the broader class of graphs excluding a topological subgraph. The proof utilises a decomposition theorem by Grohe and Marx, which constructs ak walk in a super graph while preserving structural sparsity, thereby enabling the simulation of the successor relation via FO interpretation. This allows application of existing FO model checking algorithms on bounded expansion classes. The work narrows the gap between plain and successor invariant FO, and also shows that model checking for order invariant FO is tractable on colored posets of bounded width. The results contribute to algorithmic meta theorems, highlighting how structural graph properties can be leveraged in logic based algorithm design