Compact Labelings For Efficient First-Order Model-Checking

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 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. We also consider such labelings for bounded first-order formulas on graph classes of bounded expansion. Some of these results are extended to counting queries. Key words: First-Order Logic; Labeling Scheme; Local Clique-Width; Local Tree-Width; Locally Bounded Clique-Width.

• Type: Journal
• Year: 2008
• Where: CORR
• Authors: Bruno Courcelle, Cyril Gavoille, Mamadou Moustapha Kanté
• Keywords: CORR 2008, Education, First-order Formulas, Free Set Variables, Logarithmic Length