Compact labelings for efficient first-order model-checking (Q626458)

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.