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. Journal of Computer and System Sciences. Elsevier, 2014, roč. 80, č. 1, s. 180-194. ISSN 0022-0000. Dostupné z: https://dx.doi.org/10.1016/j.jcss.2013.07.005. |
Další formáty:
BibTeX
LaTeX
RIS
@article{1130258, author = {Ganian, Robert and Hliněný, Petr and Obdržálek, Jan and Langer, Alexander and Rossmanith, Peter and Sikdar, Somnath}, article_number = {1}, doi = {http://dx.doi.org/10.1016/j.jcss.2013.07.005}, keywords = {Monadic Second-Order Logic; Treewidth; Lower Bounds; Exponential Time Hypothesis; Parameterized Complexity}, language = {eng}, issn = {0022-0000}, journal = {Journal of Computer and System Sciences}, title = {Lower Bounds on the Complexity of MSO_1 Model-Checking}, volume = {80}, year = {2014} }
TY - JOUR ID - 1130258 AU - Ganian, Robert - Hliněný, Petr - Obdržálek, Jan - Langer, Alexander - Rossmanith, Peter - Sikdar, Somnath PY - 2014 TI - Lower Bounds on the Complexity of MSO_1 Model-Checking JF - Journal of Computer and System Sciences VL - 80 IS - 1 SP - 180-194 EP - 180-194 PB - Elsevier SN - 00220000 KW - Monadic Second-Order Logic KW - Treewidth KW - Lower Bounds KW - Exponential Time Hypothesis KW - Parameterized Complexity N2 - 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, the Exponential 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 slightly weakens 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. 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. \textit{Journal of Computer and System Sciences}. Elsevier, 2014, roč.~80, č.~1, s.~180-194. ISSN~0022-0000. Dostupné z: https://dx.doi.org/10.1016/j.jcss.2013.07.005.
|