Lower Bounds on the Complexity of MSO_1 Model-Checking

D 2012

Lower Bounds on the Complexity of MSO_1 Model-Checking

GANIAN, Robert, Petr HLINĚNÝ, Jan OBDRŽÁLEK, Alexander LANGER, Peter ROSSMANITH et. al.

Základní údaje

Originální název

Lower Bounds on the Complexity of MSO_1 Model-Checking

Název česky

Dolní meze složitosti MSO1 model checking

Autoři

GANIAN, Robert (840 Spojené státy, domácí), Petr HLINĚNÝ (203 Česká republika, garant, domácí), Jan OBDRŽÁLEK (203 Česká republika, domácí), Alexander LANGER (276 Německo), Peter ROSSMANITH (276 Německo) a Somnath SIKDAR (356 Indie)

Vydání

2012. vyd. Dagstuhl, Germany, 29th International Symposium on Theoretical Aspects of Computer Science STACS2012, od s. 326-337, 12 s. 2012

Nakladatel

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, LIPICS

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Francie

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Odkazy

STACS2012

Kód RIV

RIV/00216224:14330/12:00057595

Organizační jednotka

Fakulta informatiky

ISBN

978-3-939897-35-4

ISSN

DOI

http://dx.doi.org/10.4230/LIPIcs.STACS.2012.326

UT WoS

000325386500013

Klíčová slova anglicky

Monadic Second-Order Logic; Treewidth; Lower Bounds; Exponential Time Hypothesis; Parameterized Complexity

Štítky

formela-conference

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 31. 3. 2013 13:29, prof. RNDr. Petr Hliněný, Ph.D.

Anotace

ORIG CZ

V originále

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. We show that even MSO1 model-checking with a fixed set of vertex labels, but without edge-set quantifications, is not in XP wrt the formula size as parameter for graph classes which are subgraph-closed and whose tree-width is poly-logarithmically unbounded unless the non-uniform ETH fails. In comparison to Kreutzer and Tazari, (1) we use a stronger prerequisite, namely non-uniform instead of uniform ETH, to avoid the effectiveness assumption and the construction of certain obstructions used in their proofs; and (2) we assume a different set of problems to be efficiently decidable, namely MSO1-definable properties on vertex labeled graphs instead of MSO2-definable properties on unlabeled graphs. Our result has an interesting consequence in the realm of digraph width measures: Strengthening a recent result, we show that no subdigraph-monotone measure can be algorithmically useful, unless it is within a poly-logarithmic factor of (undirected) tree-width.

Česky

Rozšiřujeme výsledky Kreutzera a Tazariho o neřešitelnosti MSO2 logiky na třídách grafů s výrazně rostoucí tree-width na MSO1 logiku s barvami vrcholů.

Návaznosti

GAP202/11/0196, projekt VaV

Název: Třídy dobře strukturovaných kombinatorických objektů, šířkové parametry a návrh efektivních algoritmů

Investor: Grantová agentura ČR, Třídy dobře strukturovaných kombinatorických objektů, šířkové parametry a návrh efektivních algoritmů

MUNI/A/0758/2011, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

GANIAN, Robert, Petr HLINĚNÝ, Jan OBDRŽÁLEK, Alexander LANGER, Peter ROSSMANITH a Somnath SIKDAR. Lower Bounds on the Complexity of MSO_1 Model-Checking. Online. In 29th International Symposium on Theoretical Aspects of Computer Science STACS2012. 2012. vyd. Dagstuhl, Germany: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, LIPICS, 2012, s. 326-337. ISBN 978-3-939897-35-4. Dostupné z: https://dx.doi.org/10.4230/LIPIcs.STACS.2012.326.

@inproceedings{992001,
   author = {Ganian, Robert and Hliněný, Petr and Obdržálek, Jan and Langer, Alexander and Rossmanith, Peter and Sikdar, Somnath},
   address = {Dagstuhl, Germany},
   booktitle = {29th International Symposium on Theoretical Aspects of Computer Science STACS2012},
   doi = {http://dx.doi.org/10.4230/LIPIcs.STACS.2012.326},
   edition = {2012},
   keywords = {Monadic Second-Order Logic; Treewidth; Lower Bounds; Exponential Time Hypothesis; Parameterized Complexity},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Dagstuhl, Germany},
   isbn = {978-3-939897-35-4},
   pages = {326-337},
   publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, LIPICS},
   title = {Lower Bounds on the Complexity of MSO_1 Model-Checking},
   url = {http://stacs2012.lip6.fr/},
   year = {2012}
}

TY  - JOUR
ID  - 992001
AU  - Ganian, Robert - Hliněný, Petr - Obdržálek, Jan - Langer, Alexander - Rossmanith, Peter - Sikdar, Somnath
PY  - 2012
TI  - Lower Bounds on the Complexity of MSO_1 Model-Checking
PB  - Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, LIPICS
CY  - Dagstuhl, Germany
SN  - 9783939897354
KW  - Monadic Second-Order Logic
KW  - Treewidth
KW  - Lower Bounds
KW  - Exponential Time Hypothesis
KW  - Parameterized Complexity
UR  - http://stacs2012.lip6.fr/
L2  - http://stacs2012.lip6.fr/
N2  - 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. We show that even MSO1 model-checking with a fixed set of vertex labels, but without edge-set quantifications, is not in XP wrt the formula size as parameter for graph classes which are subgraph-closed and whose tree-width is poly-logarithmically unbounded unless the non-uniform ETH fails. In comparison to Kreutzer and Tazari, (1) we use a stronger prerequisite, namely non-uniform instead of uniform ETH, to avoid the effectiveness assumption and the construction of certain obstructions used in their proofs; and (2) we assume a different set of problems to be efficiently decidable, namely MSO1-definable properties on vertex labeled graphs instead of MSO2-definable properties on unlabeled graphs. Our result has an interesting consequence in the realm of digraph width measures: Strengthening a recent result, we show that no subdigraph-monotone measure can be algorithmically useful, unless it is within a poly-logarithmic factor of (undirected) tree-width.
ER  -

GANIAN, Robert, Petr HLINĚNÝ, Jan OBDRŽÁLEK, Alexander LANGER, Peter ROSSMANITH a Somnath SIKDAR. Lower Bounds on the Complexity of MSO\_{}1 Model-Checking. Online. In \textit{29th International Symposium on Theoretical Aspects of Computer Science STACS2012}. 2012. vyd. Dagstuhl, Germany: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, LIPICS, 2012, s.~326-337. ISBN~978-3-939897-35-4. Dostupné z: https://dx.doi.org/10.4230/LIPIcs.STACS.2012.326.

Podrobný výpis o publikaci