Další formáty:
BibTeX
LaTeX
RIS
@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.
|