Fixed-parameter tractability, definability, and model-checking

Authors
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.