Change search
ReferencesLink to record
Permanent link

Direct link
Model checking lower bounds for simple graphs
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
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)
Abstract [en]

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
National Category
Computer and Information Science
URN: urn:nbn:se:kth:diva-124888DOI: 10.1007/978-3-642-39206-1_57ISI: 000342686600057ScopusID: 2-s2.0-84880317242ISBN: 978-364239205-4OAI: diva2:638718
40th International Colloquium on Automata, Languages, and Programming, ICALP 2013, 8 July 2013 through 12 July 2013, Riga

QC 20130801

Available from: 2013-08-01 Created: 2013-08-01 Last updated: 2014-11-07Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Lampis, Michail
By organisation
Theoretical Computer Science, TCS
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 38 hits
ReferencesLink to record
Permanent link

Direct link