Efficient First-Order Model-Checking Using Short Labels

We prove that there exists an O(log(n))-labeling scheme for every first-order formula with free set variables in every class of graphs that is nicely locally cwd-decomposable, which contains in particular, the nicely locally treedecomposable classes. For every class of bounded expansion we prove that every bounded formula has an O(log(n))-labeling scheme. We also prove that, for fixed k, every quantifier-free formula has an O(log(n))-labeling scheme in graphs of arboricity at most k. Some of these results are extended to counting queries.

• Type: Conference
• Year: 2008
• Where: FAW
• Authors: Bruno Courcelle, Cyril Gavoille, Mamadou Moustapha Kanté
• Keywords: Algorithms, FAW 2008, First-order Formula, Free Set Variables, Treedecomposable Classes