Detailed Information on Publication Record
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.Basic information
Original name
Lower Bounds on the Complexity of MSO_1 Model-Checking
Name in Czech
Dolní meze složitosti MSO1 model checking
Authors
GANIAN, Robert (840 United States of America, belonging to the institution), Petr HLINĚNÝ (203 Czech Republic, guarantor, belonging to the institution), Jan OBDRŽÁLEK (203 Czech Republic, belonging to the institution), Alexander LANGER (276 Germany), Peter ROSSMANITH (276 Germany) and Somnath SIKDAR (356 India)
Edition
2012. vyd. Dagstuhl, Germany, 29th International Symposium on Theoretical Aspects of Computer Science STACS2012, p. 326-337, 12 pp. 2012
Publisher
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, LIPICS
Other information
Language
English
Type of outcome
Stať ve sborníku
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
France
Confidentiality degree
není předmětem státního či obchodního tajemství
Publication form
electronic version available online
References:
RIV identification code
RIV/00216224:14330/12:00057595
Organization unit
Faculty of Informatics
ISBN
978-3-939897-35-4
ISSN
UT WoS
000325386500013
Keywords in English
Monadic Second-Order Logic; Treewidth; Lower Bounds; Exponential Time Hypothesis; Parameterized Complexity
Tags
Tags
International impact, Reviewed
Změněno: 31/3/2013 13:29, prof. RNDr. Petr Hliněný, Ph.D.
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.
In Czech
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ů.
Links
| GAP202/11/0196, research and development project |
| ||
| MUNI/A/0758/2011, interní kód MU |
|