Michael Lampis - Model Checking Lower Bounds for Simple Graphs

lmcs:976 - Logical Methods in Computer Science, March 25, 2014, Volume 10, Issue 1 - https://doi.org/10.2168/LMCS-10(1:18)2014
Model Checking Lower Bounds for Simple GraphsArticle

Authors: Michael Lampis

    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 Hlin\u{e}n\`{y} is essentially optimal.


    Volume: Volume 10, Issue 1
    Published on: March 25, 2014
    Imported on: September 16, 2013
    Keywords: Computer Science - Computational Complexity,Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Approximation of NP-hard optimization problems; Funder: European Commission; Code: 226203

    5 Documents citing this article

    Consultation statistics

    This page has been seen 1054 times.
    This article's PDF has been downloaded 310 times.