University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Global Realisations of Local Specifications

Global Realisations of Local Specifications

Add to your list(s) Download to your calendar using vCal

  • UserMartin Otto, Technische Universit├Ąt Darmstadt, Germany World_link
  • ClockFriday 06 November 2015, 14:00-15:00
  • HouseFW26.

If you have a question about this talk, please contact Ohad Kammar.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity