J 2014

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í

Journal of Computer and System Sciences, Elsevier, 2014, 0022-0000

Další údaje

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

UT WoS

000325386500013

Klíčová slova anglicky

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

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 1. 4. 2015 23:00, prof. RNDr. Petr Hliněný, Ph.D.

Anotace

ORIG CZ

V originále

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.

Č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