Compact Labelings For Efficient First-Order Model-Checking
Data Structures and Algorithms
2014-07-09 v2 Logic in Computer Science
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.
Cite
@article{arxiv.0811.4713,
title = {Compact Labelings For Efficient First-Order Model-Checking},
author = {Bruno Courcelle and Cyril Gavoille and Mamadou Moustapha Kanté},
journal= {arXiv preprint arXiv:0811.4713},
year = {2014}
}