Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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, p. 673-683Conference paper, Published 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, p. 673-683
Series
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 Sciences
Identifiers
URN: urn:nbn:se:kth:diva-124888DOI: 10.1007/978-3-642-39206-1_57ISI: 000342686600057Scopus ID: 2-s2.0-84880317242ISBN: 978-364239205-4 (print)OAI: oai:DiVA.org:kth-124888DiVA, id: diva2:638718
Conference
40th International Colloquium on Automata, Languages, and Programming, ICALP 2013, 8 July 2013 through 12 July 2013, Riga
Note

QC 20130801

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

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Search in DiVA

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

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 62 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf