Model Checking Lower Bounds for Simple Graphs

TL;DR

This paper establishes strong non-elementary lower bounds for model-checking problems on various graph classes, demonstrating fundamental complexity barriers and optimality of existing algorithms in logic and graph theory.

Contribution

It provides new non-elementary lower bounds for FO and MSO model-checking on specific graph classes, clarifying the limits of algorithmic efficiency and meta-theorems.

Findings

No elementary parameter dependence for FO logic on threshold graphs.

No elementary parameter dependence for MSO logic on paths unless E=NE.

Optimality of exponential bounds for MSO model-checking on colored trees of fixed depth.

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