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%2F12%3A00057595" target="_blank" >RIV/00216224:14330/12:00057595 - isvavai.cz</a>

Výsledek na webu

<a href="http://stacs2012.lip6.fr/" target="_blank" >http://stacs2012.lip6.fr/</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.4230/LIPIcs.STACS.2012.326" target="_blank" >10.4230/LIPIcs.STACS.2012.326</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

One of the most important algorithmic meta-theorems is a famous result by Courcelle, which states that any graph problem definable in monadic second-order logic with edge-set quantifications (MSO2) is decidable in linear time on any class of graphs of bounded tree-width. In the parlance of parameterized complexity, this means that MSO2 model-checking is fixed-parameter tractable with respect to the tree-width as parameter. Recently, Kreutzer and Tazari proved a corresponding complexity lower-bound---that MSO2 model-checking is not even in XP wrt the formula size as parameter for graph classes that are subgraph-closed and whose tree-width is poly-logarithmically unbounded. Of course, this is not an unconditional result but holds modulo a certain complexity-theoretic assumption, namely, the Exponential Time Hypothesis (ETH). In this paper we present a closely related result.

Název v anglickém jazyce

Lower Bounds on the Complexity of MSO_1 Model-Checking

Popis výsledku anglicky

One of the most important algorithmic meta-theorems is a famous result by Courcelle, which states that any graph problem definable in monadic second-order logic with edge-set quantifications (MSO2) is decidable in linear time on any class of graphs of bounded tree-width. In the parlance of parameterized complexity, this means that MSO2 model-checking is fixed-parameter tractable with respect to the tree-width as parameter. Recently, Kreutzer and Tazari proved a corresponding complexity lower-bound---that MSO2 model-checking is not even in XP wrt the formula size as parameter for graph classes that are subgraph-closed and whose tree-width is poly-logarithmically unbounded. Of course, this is not an unconditional result but holds modulo a certain complexity-theoretic assumption, namely, the Exponential Time Hypothesis (ETH). In this paper we present a closely related result.

Druh

D - Stať ve sborníku

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í

2012

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 statě ve sborníku

29th International Symposium on Theoretical Aspects of Computer Science STACS2012

ISBN

9783939897354

ISSN

1868-8969

e-ISSN

—

Počet stran výsledku

12

Strana od-do

326-337

Název nakladatele

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, LIPICS

Místo vydání

Dagstuhl, Germany

Místo konání akce

Paris

Datum konání akce

1. 1. 2012

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—