Compact labelings for efficient first-order model-checking

DOI10.1007/S10878-009-9260-7MaRDI QIDQ626458zbMATH OpenOpenAlexFDO

Authors Cyril Gavoille, Mamadou Moustapha Kanté, Bruno Courcelle

Publication date 18 February 2011

Published in Journal of Combinatorial Optimization (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/0811.4713

zbMATH Keywords

first-order logiclabeling schemelocal clique-widthlocal tree widthlocally bounded clique width

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Graph theory (including graph drawing) in computer science (68R10) Combinatorial optimization (90C27)

Abstract: We consider graph properties that can be checked from labels, i.e., bit sequences, of logarithmic length attached to vertices. We prove that there exists such a labeling for checking a first-order formula with free set variables in the graphs of every class that is emph{nicely locally cwd-decomposable}. This notion generalizes that of a emph{nicely locally tree-decomposable} class. The graphs of such classes can be covered by graphs of bounded emph{clique-width} with limited overlaps. We also consider such labelings for emph{bounded} first-order formulas on graph classes of emph{bounded expansion}. Some of these results are extended to counting queries.

Review text

The paper considers graph properties that can be checked from labels of logarithmic length attached to vertices. It is proved that there exists such a labeling for checking a first-order formula with free set variables in the graphs of every class that is ``nicely locally clique-width-decomposable. This notion generalizes that of a nicely locally tree-decomposable class. The graphs of such classes can be covered by graphs of bounded clique-width with limited overlaps. Labelings for bounded first-order formulas on graph classes of bounded expansion are also considered.

Recommendations

• Efficient First-Order Model-Checking Using Short Labels
• Generalized model-checking over locally tree-decomposable classes
• scientific article; zbMATH DE number 2086422
• Logical labeling schemes
• Deciding first-order properties of locally tree-decomposable structures

Cites work

• A Linear-Time Algorithm for Finding Tree-Decompositions of Small Treewidth
• Algorithmic Meta-theorems
• Approximating clique-width and branch-width
• Arboricity and bipartite subgraph listing algorithms
• Connectivity check in 3-connected planar graphs with obstacles
• Counting truth assignments of formulas of bounded tree-width or clique-width
• Deciding first-order properties of locally tree-decomposable structures
• Easy problems for tree-decomposable graphs
• Elements of finite model theory.
• Finding Branch-Decompositions and Rank-Decompositions
• First-order queries on structures of bounded degree are computable with constant delay
• From Tree-Width to Clique-Width: Excluding a Unit Interval Graph
• Generalized model-checking over locally tree-decomposable classes
• scientific article; zbMATH DE number 969067 (Why is no real title available?)
• scientific article; zbMATH DE number 2203240 (Why is no real title available?)
• Line graphs of bounded clique-width
• Linear time low tree-width partitions and algorithmic consequences
• Linear time solvable optimization problems on graphs of bounded clique-width
• Logic, graphs, and algorithms
• On powers of graphs of bounded NLC-width (clique-width)
• Query efficient implementation of graphs of bounded clique-width
• Recent developments on graphs of bounded clique-width
• Recognizability, hypergraph operations, and logical types
• Treewidth: Structure and Algorithms
• Upper bounds to the clique width of graphs

Cited in

(7)

• Efficient First-Order Model-Checking Using Short Labels
• scientific article; zbMATH DE number 2086422 (Why is no real title available?)
• On low rank-width colorings
• Fault-tolerant distance labeling for planar graphs
• Fault-tolerant distance labeling for planar graphs
• Implicit representation of relations
• Listing maximal H-free subgraphs

This page was built for publication: Compact labelings for efficient first-order model-checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q626458)