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, roč. 80, č. 1, s. 180-194. ISSN 0022-0000. doi:10.1016/j.jcss.2013.07.005. 2014.
Další formáty:   BibTeX LaTeX RIS
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í Journal of Computer and System Sciences, Elsevier, 2014, 0022-0000.
Další údaje
Originální jazyk angličtina
Typ výsledku Článek v odborném periodiku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Nizozemské království
Utajení není předmětem státního či obchodního tajemství
Impakt faktor Impact factor: 1.138
Kód RIV RIV/00216224:14330/14:00073428
Organizační jednotka Fakulta informatiky
Doi http://dx.doi.org/10.1016/j.jcss.2013.07.005
UT WoS 000325386500013
Klíčová slova anglicky Monadic Second-Order Logic; Treewidth; Lower Bounds; Exponential Time Hypothesis; Parameterized Complexity
Štítky formela-journal
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Petr Hliněný, Ph.D., učo 168881. Změněno: 1. 4. 2015 23:00.
Anotace
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.
Anotace č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 VaVNá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 MUNá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
VytisknoutZobrazeno: 19. 4. 2024 20:05