Abstract
We show that the modelchecking problem for successorinvariant firstorder logic is fixedparameter tractable on graphs with excluded topological subgraphs when parameterised by both the size of the input formula and the size of the exluded topological subgraph. Furthermore, we show that modelchecking for orderinvariant firstorder logic is tractable on coloured posets of bounded width, parameterised by both the size of the input formula and the width of the poset.
Results of this form, i.e. showing that modelchecking for a certain logic is tractable on a certain class of structures, are often referred to as algorithmic metatheorems since they give a unified proof for the tractability of a whole range of problems. Firstorder logic is arguably one of the most important logics in this context since it is powerful enough to express many computational problems (e.g. the existence of cliques, dominating sets etc.) and yet its modelchecking problem is tractable on rich classes of graphs. In fact, Grohe et al have shown that modelchecking for FO is tractable on all nowhere dense classes of graphs.
Successorinvariant FO is a semantic extension of FO by allowing the use of an additional binary relation which is interpreted as a directed Hamiltonian cycle, restricted to formulae whose truth value does not depend on the specific choice of a Hamiltonian cycle. While this is very natural in the context of modelchecking (after all, storing a structure in computer memory usually brings with it a linear order on the structure), the question of how the computational complexity of the modelchecking problem for this richer logic compares to that of plain FO is still open.
Our result for successorinvariant FO extends previous results for this logic on planar graphs and graphs with excluded minors, further narrowing the gap between what is known for FO and what is known for successorinvariant FO. The proof uses Grohe and Marx's structure theorem for graphs with excluded topological subgraphs. For orderinvariant FO we show that Gajarský et al.'s recent result for FO carries over to orderinvariant FO.
BibTeX  Entry
@InProceedings{eickmeyer_et_al:LIPIcs:2016:6558,
author = {Kord Eickmeyer and Kenichi Kawarabayashi},
title = {{SuccessorInvariant FirstOrder Logic on Graphs with Excluded Topological Subgraphs}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {18:118:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770224},
ISSN = {18688969},
year = {2016},
volume = {62},
editor = {JeanMarc Talbot and Laurent Regnier},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/6558},
URN = {urn:nbn:de:0030drops65583},
doi = {10.4230/LIPIcs.CSL.2016.18},
annote = {Keywords: modelchecking, algorithmic metatheorem, successorinvariant, firstorder logic, topological subgraphs, parameterised complexity}
}
Keywords: 

modelchecking, algorithmic metatheorem, successorinvariant, firstorder logic, topological subgraphs, parameterised complexity 
Collection: 

25th EACSL Annual Conference on Computer Science Logic (CSL 2016) 
Issue Date: 

2016 
Date of publication: 

29.08.2016 