A New Perspective on FO Model Checking of Dense Graph Classes

J 2020

A New Perspective on FO Model Checking of Dense Graph Classes

GAJARSKÝ, Jakub, Petr HLINĚNÝ, Daniel LOKSHTANOV, Jan OBDRŽÁLEK, M S RAMANUJAN et. al.

Základní údaje

Originální název

A New Perspective on FO Model Checking of Dense Graph Classes

Autoři

GAJARSKÝ, Jakub (703 Slovensko, domácí), Petr HLINĚNÝ (203 Česká republika, garant, domácí), Daniel LOKSHTANOV (578 Norsko), Jan OBDRŽÁLEK (203 Česká republika, domácí) a M S RAMANUJAN (356 Indie)

Vydání

ACM Transactions on Computational Logic, New York, NY, USA, Association for Computing Machinery, 2020, 1529-3785

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

není předmětem státního či obchodního tajemství

Odkazy

URL

Impakt faktor

Impact factor: 0.625

Kód RIV

RIV/00216224:14330/20:00114779

Organizační jednotka

Fakulta informatiky

DOI

http://dx.doi.org/10.1145/3383206

UT WoS

000586733900002

Klíčová slova anglicky

FO Logic; Model-Checking; Logic Interpretations; Sparse Graph Classes; Parameterized Complexity

Štítky

formela-journal

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 29. 4. 2021 08:15, RNDr. Pavel Šmerk, Ph.D.

Anotace

ORIG CZ

V originále

We study the FO model checking problem of dense graph classes, namely those which are FO-interpretable in some sparse graph classes. Note that if an input dense graph is given together with the corresponding FO interpretation in a sparse graph, one can easily solve the model checking problem using the existing algorithms for sparse graph classes. However, if the assumed interpretation is not given, then the situation is markedly harder. In this paper we give a structural characterization of graph classes which are FO interpretable in graph classes of bounded degree. This characterization allows us to efficiently compute such an interpretation for an input graph. As a consequence, we obtain an FPT algorithm for FO model checking of graph classes FO interpretable in graph classes of bounded degree. The approach we use to obtain these results may also be of independent interest.

Česky

Podáváme strukturální charakteristiku a algoritmicky efektivní zpracování tříd grafů, které mají FO interpretaci v grafech omezených stupňů.

Návaznosti

GA17-00837S, projekt VaV

Název: Strukturální vlastnosti, parametrizovaná řešitelnost a těžkost v kombinatorických problémech

Investor: Grantová agentura ČR, Structural properties, parameterized tractability and hardness in combinatorial problems

Citovat

GAJARSKÝ, Jakub, Petr HLINĚNÝ, Daniel LOKSHTANOV, Jan OBDRŽÁLEK a M S RAMANUJAN. A New Perspective on FO Model Checking of Dense Graph Classes. ACM Transactions on Computational Logic. New York, NY, USA: Association for Computing Machinery, 2020, roč. 21, č. 4, s. "28:1"-"28:23", 23 s. ISSN 1529-3785. Dostupné z: https://dx.doi.org/10.1145/3383206.

@article{1759916,
   author = {Gajarský, Jakub and Hliněný, Petr and Lokshtanov, Daniel and Obdržálek, Jan and Ramanujan, M S},
   article_location = {New York, NY, USA},
   article_number = {4},
   doi = {http://dx.doi.org/10.1145/3383206},
   keywords = {FO Logic; Model-Checking; Logic Interpretations; Sparse Graph Classes; Parameterized Complexity},
   language = {eng},
   issn = {1529-3785},
   journal = {ACM Transactions on Computational Logic},
   title = {A New Perspective on FO Model Checking of Dense Graph Classes},
   url = {http://dx.doi.org/10.1145/3383206},
   volume = {21},
   year = {2020}
}

TY  - JOUR
ID  - 1759916
AU  - Gajarský, Jakub - Hliněný, Petr - Lokshtanov, Daniel - Obdržálek, Jan - Ramanujan, M S
PY  - 2020
TI  - A New Perspective on FO Model Checking of Dense Graph Classes
JF  - ACM Transactions on Computational Logic
VL  - 21
IS  - 4
SP  - "28:1"-"28:23"
EP  - "28:1"-"28:23"
PB  - Association for Computing Machinery
SN  - 15293785
KW  - FO Logic
KW  - Model-Checking
KW  - Logic Interpretations
KW  - Sparse Graph Classes
KW  - Parameterized Complexity
UR  - http://dx.doi.org/10.1145/3383206
N2  - We study the FO model checking problem of dense graph classes, namely those which are FO-interpretable in some sparse graph classes. Note that if an input dense graph is given together with the corresponding FO interpretation in a sparse graph, one can easily solve the model checking problem using the existing algorithms for sparse graph classes. However, if the assumed interpretation is not given, then the situation is markedly harder. In this paper we give a structural characterization of graph classes which are FO interpretable in graph classes of bounded degree. This characterization allows us to efficiently compute such an interpretation for an input graph. As a consequence, we obtain an FPT algorithm for FO model checking of graph classes FO interpretable in graph classes of bounded degree. The approach we use to obtain these results may also be of independent interest.
ER  -

GAJARSKÝ, Jakub, Petr HLINĚNÝ, Daniel LOKSHTANOV, Jan OBDRŽÁLEK a M S RAMANUJAN. A New Perspective on FO Model Checking of Dense Graph Classes. \textit{ACM Transactions on Computational Logic}. New York, NY, USA: Association for Computing Machinery, 2020, roč.~21, č.~4, s.~''28:1''-''28:23'', 23 s. ISSN~1529-3785. Dostupné z: https://dx.doi.org/10.1145/3383206.

Podrobný výpis o publikaci