Erich Grädel

Talk on 26/5/15, 11h00: Infinite games on graphs

Infinite games where two (or more) players take turns to move a token through a
directed graph, thus tracing out an infinite path, have numerous applications
in different branches of mathematics and computer science. In the classical
format of such games, the possible moves of the players are given by the edges
of the graph; in each move a player takes the token from its current position
along an edge to a next position. In Banach-Mazur games the players instead
select in each move a path of arbitrary finite length rather than just an edge.
In both cases the outcome of a play is an infinite path and the objectives of
the players are given by properties of infinite paths.

Fundamental mathematical questions about such games, such as the
synthesis and optimization of good strategies, or the computation of winning regions
or equilibria are closely related to questions concerning the design and verification
of non-terminating systems and the evaluation of logical specifications.

In the survey we shall, in particular, discuss determinacy issues
via several different notions of "simple" strategies for games
on graphs, such as positional strategies, finite-memory strategies, move-counting or
length-counting strategies, and strategies with a memory based on finite
appearance records (FAR). We shall see that Banach-Mazur games often admit
stronger determinacy results than classical graph games and more efficient algorithmic
solutions. For instance, all Banach-Mazur games with omega-regular winning
conditions are positionally determined.

Talk on 27/5/15, 11h00: Logic and Games for Dependence and Independence

There have been a number of proposals for incorporating the concepts
of dependence or independence into mathematical logic. Classical
variants include Henkin quantifiers and independence friendly logics;
a more modern approach, triggered by Väänänen’s dependence logic,
treats notions of dependence and independence as atomic properties and
not as annotations of quantifiers, and has motivated the construction
and analysis of a large variety of logics based on different notions
of dependence and independence, many of which have close connections
to dependency concepts from database theory.

The key difference to classical logical formalisms is that dependence
and independence manifest themselves not for a single assignment,
mapping variables to elements of a structure, but only for a set of
such assignments. Accordingly, model-theoretic semantics for logics of
dependence and independence refer to structures together with a set of
assignments (called a team) and thus differ substantially from the
Tarski-style semantics of first-order logic, second-order logic and
similar formalisms.

We shall describe different logics of dependence an independence and
examine their expressive power.  We design model-checking games for
logics with team semantics in a general and systematic way in terms of
second-order reachability games. A number of examples are provided
that show how logics with team semantics express familiar
combinatorial problems in a somewhat unexpected way. Based on our
games, we provide a complexity analysis of logics with teams
semantics.

We shall also discuss the recently discovered connections between
logics with team semantics and fixed-point logics, and analyze these
connections in game-theoretic terms.