@article{4573,
  author = {Hongbin yuan, Chenyao yuan, Huiqun cao},
  title = {Fixed-Parameter Tractability of Successor-Invariant First- Order Logic on Graphs Excluding Topological Subgraphs},
  journal = {Journal of Multimedia Processing and Technologies},
  year = {2025},
  volume = {16},
  number = {3},
  doi = {https://doi.org/10.6025/jmpt/2025/16/3/138-154},
  url = {https://www.dline.info/jmpt/fulltext/v16n3/jmptv16n3_2.pdf},
  abstract = {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},
}