The complexity of first-order and monadic second-order logic revisited
type: Item
instance of: scholarly article
title: The complexity of first-order and monadic second-order logic revisited
zbMATH Open document ID: 1062.03032
author: Markus Frick
author: Martin Grohe
published in: Annals of Pure and Applied Logic
publication date: 2004-11-18T00:00:00Z
review text: The model-checking problem for a logic \(L\) is defined as follows. The inputs are (1) \(\phi\), a sentence in \(L\), and (2) a structure \(A\), and the goal is to determine whether \(\phi\) holds in \(A\). It was known that for first-order logic and for monadic second-order logic the model-checking problem is fixed-parameter tractable when the structure \(A\) is restricted to be a word. This means that for each of the two logics there exists a computable function \(f\) so that the problem is solvable in \(f(k) \cdot n\) time, where \(k\) is the length of \(\phi\) and \(n\) is the length of the word \(A\). This paper shows that, unless some implausible facts hold (such as P = NP), the function \(f\) is larger than any elementary function, in particular larger than any \(h\)-fold exponential function for any fixed \(h\). Some related hardness results are established for other types of structures (e.g., trees).
Mathematics Subject Classification ID: 03D15
Mathematics Subject Classification ID: 68Q17
Mathematics Subject Classification ID: 03C13
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 2116234
zbMATH Keywords: first-order logic
zbMATH Keywords: monadic second-order logic
zbMATH Keywords: parameterized complexity
reviewed by: Marius Zimand
MaRDI profile type: Publication
full work available at URL: j.apal.2004.01.007
OpenAlex ID: W2066585576
cites work: On the computational power of pushdown automata
cites work: Weak Second‐Order Arithmetic and Finite Automata
cites work: Q4385531
cites work: Q3893911
cites work: Q4393480
cites work: Parameterized circuit complexity and the \(W\) hierarchy
cites work: Q4298571
cites work: Q4736854
cites work: Model-Checking Problems as a Basis for Parameterized Intractability
cites work: Deciding first-order properties of locally tree-decomposable structures
cites work: Q5551141
cites work: Logics with counting and local properties
cites work: Automata, logics, and infinite games. A guide to current research
cites work: Q5284545
cites work: Q4131648
cites work: Q4385524
DOI: 10.1016/J.APAL.2004.01.007
description: scientific article; zbMATH DE number 2116234