## Lampis, Michael - Model Checking Lower Bounds for Simple Graphs

lmcs:976 - Logical Methods in Computer Science, March 25, 2014, Volume 10, Issue 1
Model Checking Lower Bounds for Simple Graphs

Authors: Lampis, Michael

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.

Source : oai:arXiv.org:1302.4266
DOI : 10.2168/LMCS-10(1:18)2014
Volume: Volume 10, Issue 1
Published on: March 25, 2014
Submitted on: September 16, 2013
Keywords: Computer Science - Computational Complexity,Computer Science - Logic in Computer Science