On the parameterized intractability of monadic second-order logic

DOI10.2168/LMCS-8(1:27)2012MaRDI QIDQ2881095zbMATH OpenFDO

Authors Stephan Kreutzer

Publication date 3 April 2012

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1203.3167

zbMATH Keywords

algorithmic meta-theoremsfinite model theoryparameterized complexity

Mathematics Subject Classification ID

Model theory of finite structures (03C13) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: One of Courcelle's celebrated results states that if C is a class of graphs of bounded tree-width, then model-checking for monadic second order logic (MSO_2) is fixed-parameter tractable (fpt) on C by linear time parameterized algorithms, where the parameter is the tree-width plus the size of the formula. An immediate question is whether this is best possible or whether the result can be extended to classes of unbounded tree-width. In this paper we show that in terms of tree-width, the theorem cannot be extended much further. More specifically, we show that if C is a class of graphs which is closed under colourings and satisfies certain constructibility conditions and is such that the tree-width of C is not bounded by log^{84} n then MSO_2-model checking is not fpt unless SAT can be solved in sub-exponential time. If the tree-width of C is not poly-logarithmically bounded, then MSO_2-model checking is not fpt unless all problems in the polynomial-time hierarchy can be solved in sub-exponential time.

Recommendations

• On the Parameterised Intractability of Monadic Second-Order Logic
• Lower bounds on the complexity of \(\mathrm{MSO}_1\) model-checking
• Lower bounds on the complexity of \(\mathsf{MSO}_1\) model-checking
• The complexity of first-order and monadic second-order logic revisited
• Tree-width and the monadic quantifier hierarchy.

Cited in

(20)

• Tree-width and the monadic quantifier hierarchy.
• The complexity of first-order and monadic second-order logic revisited
• Computability by monadic second-order logic
• Lower bounds on the complexity of \(\mathrm{MSO}_1\) model-checking
• Special tree-width and the verification of monadic second-order graph properties
• Parameters tied to treewidth
• Parameterized Complexity Results for 1-safe Petri Nets
• SAT in Monadic Gödel Logics: A Borderline between Decidability and Undecidability
• On the Parameterised Intractability of Monadic Second-Order Logic
• scientific article; zbMATH DE number 4097355 (Why is no real title available?)
• On the model-checking of monadic second-order formulas with edge set quantifications
• Practical algorithms for MSO model-checking on tree-decomposable graphs
• Bisimulation Invariant Monadic-Second Order Logic in the Finite
• Reducing CMSO model checking to highly connected graphs
• Monadic second order finite satisfiability and unbounded tree-width
• Model checking lower bounds for simple graphs
• Model checking lower bounds for simple graphs
• Directed Nowhere Dense Classes of Graphs
• Twin-width. IV: Ordered graphs and matrices
• Advances in algorithmic meta theorems (invited paper)

This page was built for publication: On the parameterized intractability of monadic second-order logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2881095)