Model checking lower bounds for simple graphs
2013 (English)In: Automata, Languages, and Programming: 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part I, Springer, 2013, no PART 1, 673-683 p.Conference paper (Refereed)
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 EXP=NEXP. 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ý and Hliněnỳ is essentially optimal.
Place, publisher, year, edition, pages
Springer, 2013. no PART 1, 673-683 p.
, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN 0302-9743 ; 7965
Computer and Information Science
IdentifiersURN: urn:nbn:se:kth:diva-124888DOI: 10.1007/978-3-642-39206-1_57ISI: 000342686600057ScopusID: 2-s2.0-84880317242ISBN: 978-364239205-4OAI: oai:DiVA.org:kth-124888DiVA: diva2:638718
40th International Colloquium on Automata, Languages, and Programming, ICALP 2013, 8 July 2013 through 12 July 2013, Riga
QC 201308012013-08-012013-08-012014-11-07Bibliographically approved