Algorithmic Model Theory

Finite Model Theory of Guarded Logics

The generalised tree-model property of the guarded fragment [G99] explains some of the good algorithmic model-theoretic properties of the guarded fragment and some of its extensions. In light of the above, this crucial feature of guarded logics should be called acyclic model property, because a guarded tree-unfolding always yields a guarded bisimilar model whose hypergraph of guarded sets is acyclic.

The obvious analogy here is that with the tree model property of basic modal logic: bisimilar tree unfoldings yielding models based on acyclic graphs (i.e., actual trees rather than tree-like relational structures, or acyclic graphs rather than acyclic hypergraphs). This analogy does not carry over easily to the finite model theory of modal and guarded logics, though: while basic modal logic even has the finite tree-model property, for the guarded fragment there cannot be any straightforward finite model analogue of its acyclic model property (see here).


Characterisation theorem (fmt)

Finite cover constructions and the analysis of guarded bisimulation and first-order Ehrenfeucht–Fraisse games have confirmed the long-standing conjecture that the guarded fragment GF is expressively complete for the class of all first-order properties of finite structures that are compatible with guarded bisimulation equivalence [O10] (the fmt analogue of the Andreka–van Benthem–Nemeti charaterisation).

Finite model properties and small models

An elegant proof of the finite model property for the guarded fragment GF in [G99] was extended to the clique guarded fragment CGF in [HO03] using conformal finite hypergraph covers; the same argument proved the Hrushovski–Herwig–Lascar style extension property for partial automorphisms (EPPA) for the class of conformal finite relational structures and, e.g., for the class of Ck-free graphs.

Substantial extensions of the finite model property for GF were achieved in [BGO10] and [O10]. The weakly acyclic covers in [BGO10] show that GF has the finite model property also in restriction to any class defined in terms of forbidden homomorphic images of finitely many configurations – and thus shows that conjunctive queries are finitely controllable in the presence of guarded constraints. The acyclic covers of [O10] show that GF even has the finite model property in restriction to any class defined in terms of finitely many forbidden cyclic configurations. This is a strong results for the finite model theory of GF since infinite fully acyclic models can always be obtained by the abovementioned acyclic model property. Other key results of [BGO10] provide rather tight, feasible bounds on the size of small models for GF and CGF.

Descriptive complexity

A polynomial time canonisation procedure for finite relational structures up to guarded bisimulation equivalence in [BGO10] implies that there is a logic for the class of all guarded bisimulation closed PTime properties of finite structures, a positive solution to the fundamental problem of capturing Ptime in the guarded world.


[G99] E. Grädel. On the restraining power of guards. Journal of Symbolic Logic, vol. 64, pp. 1719–1742, 1999. 

[O10]M. Otto.Highly acyclic groups, hypergraph covers and the guarded fragment, preprint, 2010, 42 pages. Journal version of LICS 2010 paper, invited for JACM, December 2010. Abstract

[HO03] I. Hodkinson and M. Otto, Finite Conformal Hypergraph Covers and Gaifman Cliques in Finite Structures,
Bulletin of Symbolic Logic, volume 9, 2003, pp. 387-405.
Abstract BibTeX entry

[BGO10] V. Barany, G. Gottlob and M. Otto. Querying the Guarded Fragment, Proceedings of Logic in Computer Science, LICS 2010
Abstract BibTeX entry


A A A | Print Print | Impressum Legal note | Contact Contact
    zum Seitenanfangzum Seitenanfang