# 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.