Model checking lower bounds for simple graphs

DOI10.1007/978-3-642-39206-1_57MaRDI QIDQ5326601zbMATH OpenOpenAlexFDO

Authors Michael Lampis

Publication date 6 August 2013

Published in Automata, Languages, and Programming (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: A well-known result by Frick and Grohe shows that deciding FO logic on trees involves a parameter dependence that is a tower of exponentials. Though this lower bound is tight for Courcelle's theorem, it has been evaded by a series of recent meta-theorems for other graph classes. Here we provide some additional non-elementary lower bound results, which are in some senses stronger. Our goal is to explain common traits in these recent meta-theorems and identify barriers to further progress. More specifically, first, we show that on the class of threshold graphs, and therefore also on any union and complement-closed class, there is no model-checking algorithm with elementary parameter dependence even for FO logic. Second, we show that there is no model-checking algorithm with elementary parameter dependence for MSO logic even restricted to paths (or equivalently to unary strings), unless E=NE. As a corollary, we resolve an open problem on the complexity of MSO model-checking on graphs of bounded max-leaf number. Finally, we look at MSO on the class of colored trees of depth d. We show that, assuming the ETH, for every fixed d>=1 at least d+1 levels of exponentiation are necessary for this problem, thus showing that the (d+1)-fold exponential algorithm recently given by Gajarsk`{y} and Hlinu{e}n`{y} is essentially optimal.

Recommendations

• Model checking lower bounds for simple graphs
• Lower bounds on the complexity of \(\mathrm{MSO}_1\) model-checking
• Lower bounds on the complexity of \(\mathsf{MSO}_1\) model-checking
• On the parameterized intractability of monadic second-order logic
• On the Parameterised Intractability of Monadic Second-Order Logic

Cited in

(10)

• FO model checking on geometric graphs
• Lower bounds on the complexity of \(\mathrm{MSO}_1\) model-checking
• scientific article; zbMATH DE number 1756016 (Why is no real title available?)
• scientific article; zbMATH DE number 7029306 (Why is no real title available?)
• Treewidth with a quantifier alternation revisited
• Kernelizing MSO properties of trees of fixed height, and some consequences
• Model checking lower bounds for simple graphs
• First-Order Model-Checking in Random Graphs and Complex Networks
• A tight Monte-Carlo algorithm for Steiner tree parameterized by clique-width
• On low tree-depth decompositions

This page was built for publication: Model checking lower bounds for simple graphs

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