Deciding first-order properties for sparse graphs

J 2010

Deciding first-order properties for sparse graphs

KRÁĽ, Daniel; Daniel KRÁĽ and R THOMAS

Basic information

Original name

Deciding first-order properties for sparse graphs

Authors

KRÁĽ, Daniel; Daniel KRÁĽ and R THOMAS

Edition

2010 IEEE 51ST ANNUAL SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE, LOS ALAMITOS, IEEE COMPUTER SOC, 2010, 0272-5428

Other information

Language

English

Type of outcome

Article in a journal

Confidentiality degree

is not subject to a state or trade secret

DOI

https://doi.org/10.1109/FOCS.2010.20

UT WoS

000287040100015

Keywords in English

algorithmic metatheorems; graphs with bounded expansion; graphs with bounded degree; minor-closed classes of graphs; graphs with locally bounded tree-width

Changed: 6/11/2020 10:00, Mgr. Darina Boukalová

Abstract

In the original language

We present a linear-time algorithm for deciding first-order logic (FOL) properties in classes of graphs with bounded expansion. Many natural classes of graphs have bounded expansion: graphs of bounded tree-width, all proper minor-closed classes of graphs, graphs of bounded degree, graphs with no subgraph isomorphic to a subdivision of a fixed graph, and graphs that can be drawn in a fixed surface in such a way that each edge crosses at most a constant number of other edges. We also develop an almost linear-time algorithm for deciding FOL properties in classes of graphs with locally bounded expansion; those include classes of graphs with locally bounded tree-width or locally excluding a minor. More generally, we design a dynamic data structure for graphs belonging to a fixed class of graphs of bounded expansion. After a linear-time initialization the data structure allows us to test an FOL property in constant time, and the data structure can be updated in constant time after addition/deletion of an edge, provided the list of possible edges to be added is known in advance and their addition results in a graph in the class. In addition, we design a dynamic data structure for testing existential properties or the existence of short paths between prescribed vertices in such classes of graphs. All our results also hold for relational structures and are based on the seminal result of Nesetril and Ossona de Mendez on the existence of low tree-depth colorings.

Cite

KRÁĽ, Daniel; Daniel KRÁĽ and R THOMAS. Deciding first-order properties for sparse graphs. 2010 IEEE 51ST ANNUAL SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE. LOS ALAMITOS: IEEE COMPUTER SOC, 2010, p. 133-142. ISSN 0272-5428. Available from: https://doi.org/10.1109/FOCS.2010.20.

@article{1689684,
   author = {Kráľ, Daniel and Kráľ, Daniel and Thomas, R},
   article_location = {LOS ALAMITOS},
   doi = {https://doi.org/10.1109/FOCS.2010.20},
   keywords = {algorithmic metatheorems; graphs with bounded expansion; graphs with bounded degree; minor-closed classes of graphs; graphs with locally bounded tree-width},
   language = {eng},
   issn = {0272-5428},
   journal = {2010 IEEE 51ST ANNUAL SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE},
   title = {Deciding first-order properties for sparse graphs},
   year = {2010}
}

TY  - JOUR
ID  - 1689684
AU  - Kráľ, Daniel - Kráľ, Daniel - Thomas, R
PY  - 2010
TI  - Deciding first-order properties for sparse graphs
JF  - 2010 IEEE 51ST ANNUAL SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE
SP  - 133-142
EP  - 133-142
PB  - IEEE COMPUTER SOC
SN  - 02725428
KW  - algorithmic metatheorems
KW  - graphs with bounded expansion
KW  - graphs with bounded degree
KW  - minor-closed classes of graphs
KW  - graphs with locally bounded tree-width
N2  - We present a linear-time algorithm for deciding first-order logic (FOL) properties in classes of graphs with bounded expansion. Many natural classes of graphs have bounded expansion: graphs of bounded tree-width, all proper minor-closed classes of graphs, graphs of bounded degree, graphs with no subgraph isomorphic to a subdivision of a fixed graph, and graphs that can be drawn in a fixed surface in such a way that each edge crosses at most a constant number of other edges. We also develop an almost linear-time algorithm for deciding FOL properties in classes of graphs with locally bounded expansion; those include classes of graphs with locally bounded tree-width or locally excluding a minor. More generally, we design a dynamic data structure for graphs belonging to a fixed class of graphs of bounded expansion. After a linear-time initialization the data structure allows us to test an FOL property in constant time, and the data structure can be updated in constant time after addition/deletion of an edge, provided the list of possible edges to be added is known in advance and their addition results in a graph in the class. In addition, we design a dynamic data structure for testing existential properties or the existence of short paths between prescribed vertices in such classes of graphs. All our results also hold for relational structures and are based on the seminal result of Nesetril and Ossona de Mendez on the existence of low tree-depth colorings.
ER  -

KRÁĽ, Daniel; Daniel KRÁĽ and R THOMAS. Deciding first-order properties for sparse graphs. \textit{2010 IEEE 51ST ANNUAL SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE}. LOS ALAMITOS: IEEE COMPUTER SOC, 2010, p.~133-142. ISSN~0272-5428. Available from: https://doi.org/10.1109/FOCS.2010.20.

Přehled o publikaci