Abstract

The following situation is typical of several tasks of model construction that arise, e.g., in connection with finite model properties and finite controllability: Given a finite set of local templates, together with specifications of required and permitted pairwise overlaps between them, the task is to find finite global realisations.

We approach this finite realisation task via a generic construction of reduced products with suitable groupoids. Due to strong acyclicity properties, these groupoids can serve as structural backbones in the construction of finite realisations, similar to the use of free groups in standard constructions of infinite realisations. The construction is sufficiently generic as to be compatible with symmetries of the specification while also allowing us to avoid incidental cycles of overlaps up to any specified finite length. The resulting finite realisations can be forced

—to realise symmetries built into the specification, and —to admit local homomorphisms into any (finite or infinite)

realisation and in particular into the canonical free realisation. As one consequence we obtain a new proof of the finite-model-assertion in a theorem of Herwig and Lascar, which allows us to lift local symmetries of finite structures to global symmetries within classes defined by forbidden homomorphisms. This in turn proves, e.g., finite controllability for UCQ vs. guarded specifications.