Citation

J. Flum et M. Grohe, Fixed-parameter tractability, definability, and model-checking, SIAM J COMP, 31(1), 2001, pp. 113-145

Citations number

31

Language

INGLESE

art.tipo

Article

Categorie Soggetti

Computer Science & Engineering

Journal title

SIAM JOURNAL ON COMPUTING

ISSN journal

0097-5397
→ ACNP

Volume

31

Issue

1

Year of publication

2001

Pages

113 - 145

Database

ISI

SICI code

0097-5397(20010729)31:1<113:FTDAM>2.0.ZU;2-2

Abstract

In this article, we study parameterized complexity theory from the perspect
ive of logic, or more specifically, descriptive complexity theory.
We propose to consider parameterized model-checking problems for various fr
agments of first-order logic as generic parameterized problems and show how
this approach can be useful in studying both fixed-parameter tractability
and intractability. For example, we establish the equivalence between the m
odel-checking for existential first-order logic, the homomorphism problem f
or relational structures, and the substructure isomorphism problem. Our mai
n tractability result shows that model-checking for first-order formulas is
fixed-parameter tractable when restricted to a class of input structures w
ith an excluded minor. On the intractability side, for every t greater than
or equal to 0 we prove an equivalence between model-checking for first-ord
er formulas with t quanti er alternations and the parameterized halting pro
blem for alternating Turing machines with t alternations. We discuss the cl
ose connection between this alternation hierarchy and Downey and Fellows W-
hierarchy.
On a more abstract level, we consider two forms of definability, called Fag
in definability and slicewise definability, that are appropriate for descri
bing parameterized problems. We give a characterization of the class FPT of
all fixed-parameter tractable problems in terms of slicewise definability
in finite variable least fixed-point logic, which is reminiscent of the Imm
erman-Vardi theorem characterizing the class PTIME in terms of definability
in least fixed-point logic.