Compact Labelings For Efficient First-Order Model-Checking

Bruno Courcelle (1, 2) , Cyril Gavoille (1, 3) , Mamadou Moustapha Kanté (4)

1 LaBRI - Laboratoire Bordelais de Recherche en Informatique
2 IUF - Institut universitaire de France
3 CEPAGE - Algorithmics for computationally intensive applications over wide scale distributed platforms
4 LIMOS - Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes

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.

Mots clés: First-Order Logic; Labeling Scheme; Local Clique-Width; Local Tree-Width; Locally Bounded Clique-Width.; Locally Bounded Clique-Width

Domaines: Algorithme et structure de données [cs.DS]; Logique en informatique [cs.LO]

Bruno Courcelle, Cyril Gavoille, Mamadou Moustapha Kanté. Compact Labelings For Efficient First-Order Model-Checking. Journal of Combinatorial Optimization, 2011, 21 (1), pp.19--46. ⟨hal-00342668⟩