Concerning model checking, our method uses a different technique than the
previous ones. There are several characterizations of classes having bounded
expansion [1]}. Among them we find characterizations via
“low tree depth coloring” and “transitive fraternal augmentations”. The
previous methods were based on the low tree depth coloring characterization
while ours is based on transitive fraternal augmentations. We show that it is
enough to consider quantifier-free queries in a given normal form. The normal
form is at the core of our algorithms for constant delay enumeration and for
counting the number of solutions. As for the previous proofs, we exhibit a
quantifier elimination method, also based on our normal form. Our quantifier
elimination method results in a quantifier-free query but over a recoloring
of a functional representation of a “fraternal and transitive augmentation”
of the initial structure.
