Talks:

We embed the framework of infinite two-player turn-based games played on graphs with safety objectives in an epistemic temporal logic. This embedding is made possible thanks to two intermediate embeddings: the first is from infinite games with safety objectives to supervisory control theory and the second is from supervisory control theory to epistemic temporal logic. Thereby, we are able to determine whether a player has a winning strategy from a given state, and in that case we can elicit and synthesize all his winning strategies. The originality of our results stems from the fact that they are all formulated in terms of model checking problems in our epistemic temporal logic. Our reformulation of infinite game theory and supervisory control theory in epistemic temporal logic highlights their main underlying intuitions in terms of formal expressions involving the modalities of action, time and knowledge.

We propose strategic games wherein the strategies consist of players asking each other questions and answering those questions. We study simplifications of such games wherein two players simultaneously ask each other a question that the opponent is then obliged to answer. The motivation for our research is to model conversation including the dynamics of questions and answers, to provide new links between game theory and dynamic logics of information, and to exploit the dynamic/strategic structure that, we think, lies implicitly inside epistemic models for epistemic languages, and to make that structure an explicit subject of logical study. Our main contributions are: the notion of a two-person question-answer game with information goals, the existence and computation of equilibria for these games, the correspondence with Bayesian games and their equilibria, and a connection between logic and game theory namely the existence of equilibria for positive goal formulae.

This work is joint with Thomas Agotnes, Johan van Benthem and Stefan Minica.

The main aim of the epistemic foundation program of game theory is to characterise, for any game, the behaviour of rational players who know the structure of the game, players' preferences, and can reason about each others' rationality as well as reasoning abilities. Over the years, many proposals have been put forward to describe what 'mutual recognition of rationality' means. In this talk we would focus on two such proposals for dynamic games, viz. common strong belief in rationality (Battigalli and Siniscalchi, 2002) and common belief in future rationality (Perea, 2013), the corresponding recursive procedures, viz. iterated conditional dominance procedure and backward dominance procedure, respectively, and compare the outcome sets for these two procedures. Comparing these sets is far from trivial as these are distinct iterative heuristics of strategy sieving whose technical definitions do not directly disclose their epistemic motivations. This calls for exposing the axiomatic assumptions underlying the concepts in a way which will enable an explicit comparison between them. If time permits, we would present ongoing work on building up such axiom systems.

The distributed synthesis problem asks for a coordinated strategy in a multi-agent setting where each agent has only partial information about the other agents actions/states and the agents coordinate their play to win against moves of a distinguished player (called Nature). For three or more agents (including Nature) this problem is known to be undecidable even for simple objectives. We show that under the guarantee of recurrent 'certainty' for agents such games can be decided for observable winning conditions. Additionally we show that there is an efficient way of testing this property given an arbitrary game graph. We also show the same results under the guarantee of another property called 'recurrent hierarchicity'.

A general concept of uniform strategies has recently been proposed as a relevant notion in game theory for computer science, which subsumes various notions from the literature. It relies on properties involving sets of plays in two-player turn-based arenas equipped with arbitrary binary relations between plays; these properties are expressed in a language based on CTL* with a quantifier over related plays. There are two semantics for our quantifier, a strict one and a full one, that we study separately. Regarding the strict semantics, the existence of a uniform strategy is undecidable for rational binary relations, but introducing jumping tree automata and restricting to recognizable relations allows us to establish a 2-Exptime-complete complexity - and still capture a class of two-player imperfect-information games with epistemic temporal objectives. Regarding the full semantics, relying on information set automata we establish that the existence of a uniform strategy is decidable for rational relations and we provide a nonelementary synthesis procedure. We also exhibit an essentially optimal subclass of rational relations for which the problem becomes 2-Exptime-complete. Considering rich classes of relations makes the theory of uniform strategies powerful: it directly entails various results in logics of knowledge and time, some of them already known, and others new.

We study infinite two-player games on at most countable alphabets. We first investigate the scenario where one of the players is unsure about the set of moves available to the other player. In particular, the set of moves of the other player is a strict superset of what she assumes it to be. We explore what happens to sets in various levels of the Borel hierarchy under such a situation. We show that the sets at every alternate level of the hierarchy jump to the next higher level. We then look at what happens to the various Borel sets under homomorphisms and inverse homomorphisms. We show that depending on the nature of the homomorphism, a Borel set can either stay at the same level in the hierarchy or undergo jumps similar to the ones under uncertain moves. Finally, we introduce a fragment of the logic $L_{\omega_1\omega}$ which we call $L^*_{\omega_1\omega}$ and which we show can define the countable levels of the Borel hierarchy. We also show that an increase in the alternation depth of the operators of the $L^*_{\omega_1\omega}$ formula result in a strict increase in their expressive power.

This work is joint with Nicholas Asher.

We present a new logic RoCTL* to model robustness in concurrent systems. RoCTL* extends CTL* with the addition of Obligatory and Robustly operators, which quantify over failure-free paths and paths with one more failure respectively. We present a number of examples of problems to which RoCTL* can be applied. The core result of this talk is to show that RoCTL* is expressively equivalent to CTL* but is non-elementarily more succinct. We present a translation from RoCTL* into CTL* that preserves truth but may result in non-elementary growth in the length of the translated formula as each nested Robustly operator may result in an extra exponential blow-up. However, we show that this translation is optimal in the sense that any equivalence preserving translation will require an extra exponential growth per nested Robustly. We also compare RoCTL* to Quantified CTL* (QCTL*) and hybrid logics.

This is joint work with John C. McCabe-Dansted, Tim French and Mark Reynolds, University of Western Australia.

Notions of strategy dominance and iterated elimination of dominated strategies are central for study of rationality and equilibria in games. These notions can be extended to infinite games on graphs, but there are many challenges since the set of strategies is infinite and may lead to infinite dominance chains. Imperfect information results in infinite epistemic structures, complicating construction of Harsanyi-style type spaces. The talk is a brief tour through the challenging terrain.

Multi-pushdown systems are formal systems used to model concurrent programs. Without any restrictions, such systems are Turing powerful . Various decidable subclasses of Multi-pushdown systems have been well studied in literature. We will look at decidability and complexity bounds of parity games on structures of some well known subclasses.

The class of weakly acyclic games capture many applications in selfish routing and network connection framework. Intuitively, weakly acyclic games are games in which the natural update dynamics (like the best response update) does not enter into an inescapable cycle. The existence of pure Nash equilibrium is therefore guaranteed in weakly acyclic games. We argue that it is useful to classify weakly acyclic games using the concept of a scheduler. We also show some results relating weakly acyclic games to the notion of strategic dominance.

Sponsors.

The Institute of Mathematical Sciences (IMSc)	INRIA, Rennes

Organizer