The Community for Technology Leaders
Logic in Computer Science, Symposium on (2002)
Copenhagen, Denmark
July 22, 2002 to July 25, 2002
ISSN: 1043-6871
ISBN: 0-7695-1483-9
pp: 215
Markus Frick , University of Edinburgh
Martin Grohe , University of Edinburgh
<p>The model-checking problem for a logic L on a class C of structures asks whether a given L-sentence holds in a given structure in C. In this paper, we give super-exponential lower bounds for fixed-parameter tractable model-checking problems for first-order and monadic second-order logic.</p> <p>We show that unless PTIME = NP, the model-checking problem for monadic second-order logic on finite words is not solvable in time f(k) ?p(n),for any elementary function f and any polynomial p. Here k denotes the size of the input sentence and n the size of the input word. We prove the same result for first-order logic under a stronger complexity theoretic assumption from parameterized complexity theory.</p> <p>Furthermore, we prove that the model-checking problems for first-order logic on structures of degree 2 and of bounded degree d\leqslant 3 are not solvable in time 2^(2^{0(k)}} ?p(n) (for degree 2), and 2^{2^{2^{0(k)}}} ?p(n) (for degree d) for any polynomial p, again under an assumption from parameterized complexity theory. We match these lower bounds by corresponding upper bounds.</p>

M. Grohe and M. Frick, "The Complexity of First-Order and Monadic Second-Order Logic Revisited," Logic in Computer Science, Symposium on(LICS), Copenhagen, Denmark, 2002, pp. 215.
95 ms
(Ver 3.3 (11022016))