In this talk we shall describe recent work at Oxford, developing a structural understanding of bisimulation games for various guarded fragments of first order logic. Intuitively, these guarded logics are wide generalisations of conventional modal logics, gaining superior expressive power, whilst retaining attractive computational characteristics. Our eventual aim is to identify the structural reasons why these logics have such desirable computational and model theoretic properties.

Our analysis builds upon the earlier work of Abramsky, Dawar, Wang and Shah exhibiting an exciting connection between two apparently disparate fields:

* The study of the power of computational methods, as typified by finite model theory and descriptive complexity
* The investigation of the structure of computational phenomena, characteristic of program semantics and particularly categorical methods

The divide is bridged by a novel comonadic perspective on model comparison games such as the pebbling and Ehrenfeuct-Fraisse games. The framework also has quantitative aspects, via natural gradings that capture resource theoretic aspects on the phenomena involved. It is these techniques that we aim extend to the guarded setting in our new work.

The talk will aim to be reasonably self contained. We shall provide an introduction to the comonadic approach to model comparison games, and background on the various logical fragments of interest.

This is work in progress, jointly with Samson Abramsky, Tom Paine, and Nihil Shah at Oxford

Hella's k-pebble n-bijective is a long-studied generalisation of the k-pebble bijection game. While the latter captures equivalence of relational structures up to k-variable first-order logic extendended with fixed-point and counting quantifiers, Hella's game (for n>1) captures equivalence in the much more powerful extension of FO with all n-ary generalised quantifiers. In this talk, I'll present a new contruction that Anuj Dawar and I have been working on which extends Abramsky, Dawar and Wang's pebbling comonad to deal with generalised quantifiers.       

This talk will be about ongoing work on a subcomonad of the pebbling comonad. This subcomona captures a restriction of k-variable logic that imposes a restriction on conjunctions in a formula. In analogy with the characterization of tree-width as the coalgebra number, I will show that this subcomonad characterizes path-width. As a bonus, I will discuss ongoing work on clique-width and other graph parameters.

Traditionally, in categorical logic, first-order quantifiers are encoded as adjoints to the inclusion maps of the algebra of formulas in n free variables into the algebra of formulas in n+1 free variables. Hence, quantifiers correspond to a property of the inclusion maps. We depart from this standpoint and propose viewing quantification as a "construction". We discuss how, from this perspective, quantification can be dually understood as a space-of-measures construction. To illustrate these ideas, we draw from recent results obtained in collaboration with Mai Gehrke and Daniela Petrisan where the viewpoint of quantifiers as measures has been successfully applied in logic on words and finite model theory.

The talk is divided into two parts, one presented by Tomas Jakl and the other by Luca Reggio.

I'd like to present some very early ideas being developed with Adam Ó Conghaile and Sasha Huriot on extensions of concurrent games which it's intended will help unify game theoretic, algebraic and resource considerations.

In this talk I will discuss the finite rank fragments of the pebbling comonad introduced by Abrasmsky, Dawar and Wang. These can be used analogously to the ‘n-cores’ used in the proof of Rossmans equirank homomorphism preservation theorem, with an aim to also preserve the number of variables used in a formula. I will give a proof of some simple cases and indicate what would be needed to prove the full result.