Lower Bounds on the Complexity of MSO_1 Model-Checking

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F14%3A00073428" target="_blank" >RIV/00216224:14330/14:00073428 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1016/j.jcss.2013.07.005" target="_blank" >http://dx.doi.org/10.1016/j.jcss.2013.07.005</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1016/j.jcss.2013.07.005" target="_blank" >10.1016/j.jcss.2013.07.005</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Lower Bounds on the Complexity of MSO_1 Model-Checking

Popis výsledku v původním jazyce

Kreutzer and Tazari proved in 2010 that MSO2 model-checking is not polynomial (XP) wrt. the formula size as parameter for graph classes that are subgraph-closed and whose tree-width is poly-logarithmically unbounded. We prove that MSO1 model-checking with a fixed set of vertex labels---i.e., without edge-set quantification---is not solvable even in quasi-polynomial time for fixed MSO-formulas in such graph classes. Both the lower bounds hold modulo a certain complexity-theoretic assumption, namely, theExponential Time Hypothesis (ETH) in the former case and the nonuniform ETH in the latter case. In comparison to Kreutzer and Tazari, we show a different set of problems to be intractable, and our stronger complexity assumption of nonuniform ETH slightlyweakens assumptions on the graph class and greatly simplifies important lengthy parts of the former proof. Our result also has an interesting consequence in the realm of digraph width measures.

Název v anglickém jazyce

Lower Bounds on the Complexity of MSO_1 Model-Checking

Popis výsledku anglicky

Kreutzer and Tazari proved in 2010 that MSO2 model-checking is not polynomial (XP) wrt. the formula size as parameter for graph classes that are subgraph-closed and whose tree-width is poly-logarithmically unbounded. We prove that MSO1 model-checking with a fixed set of vertex labels---i.e., without edge-set quantification---is not solvable even in quasi-polynomial time for fixed MSO-formulas in such graph classes. Both the lower bounds hold modulo a certain complexity-theoretic assumption, namely, theExponential Time Hypothesis (ETH) in the former case and the nonuniform ETH in the latter case. In comparison to Kreutzer and Tazari, we show a different set of problems to be intractable, and our stronger complexity assumption of nonuniform ETH slightlyweakens assumptions on the graph class and greatly simplifies important lengthy parts of the former proof. Our result also has an interesting consequence in the realm of digraph width measures.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GAP202%2F11%2F0196" target="_blank" >GAP202/11/0196: Třídy dobře strukturovaných kombinatorických objektů, šířkové parametry a návrh efektivních algoritmů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2014

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Journal of Computer and System Sciences

ISSN

0022-0000

e-ISSN

—

Svazek periodika

80

Číslo periodika v rámci svazku

1

Stát vydavatele periodika

NL - Nizozemsko

Počet stran výsledku

15

Strana od-do

180-194

Kód UT WoS článku

000325386500013

EID výsledku v databázi Scopus

—