Compact labelings for efficient first-order model-checking

DOI10.1007/S10878-009-9260-7zbMATH Open1237.90191arXiv0811.4713OpenAlexW2102621965MaRDI QIDQ626458FDOQ626458

Authors: Cyril Gavoille, Mamadou Moustapha Kanté, Bruno Courcelle 

Publication date: 18 February 2011

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

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.

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

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

zbMATH Keywords

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (6)

• On low rank-width colorings
• Fault-tolerant distance labeling for planar graphs
• Fault-tolerant distance labeling for planar graphs
• Efficient First-Order Model-Checking Using Short Labels
• Implicit representation of relations
• Title not available (Why is that?)

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)