ECCC
Electronic Colloquium on Computational Complexity
Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR09-131 | 2nd December 2009 19:19

Parameterized Complexity of First-Order Logic

RSS-Feed




TR09-131
Authors: Stephan Kreutzer, Anuj Dawar
Publication: 3rd December 2009 01:58
Downloads: 810
Keywords: 


Abstract:

We show that if $\mathcal C$ is a class of graphs which is
"nowhere dense" then first-order model-checking is
fixed-parameter tractable on $\mathcal C$. As all graph classes which exclude a fixed minor, or are of bounded local tree-width or locally exclude a minor are nowhere dense, this generalises algorithmic meta-theorems obtained for these classes in the past
(see \cite{FlumGro01,FrickGro01,DawarGroKre07}).

Conversely, if $\mathcal C$ is not nowhere dense and in addition is closed under taking sub-graphs and
satisfies some effectivity conditions then FO-model
checking is not FPT on $\mathcal C$ unless FPT = AW[*].

Hence, for classes of graphs closed under sub-graphs, this essentially gives a precise characterisation of classes for which FO model-checking is tractable.

However, our result generalises to much more general classes of graphs. In particular we show that every class which can efficiently be coloured "over a class with the type representation property" allows tractable first-order model-checking. Such classes include all classes which are nowhere dense and also all classes of bounded clique-width. This result therefore unifies all known meta-theorems for first-order logic.



ISSN 1433-8092 | Imprint