Invited Speakers


Krishnendu Chatterjee (IST Austria)

Breaking the O(n*m) Barrier for Büchi Games and Probabilistic Verification.

Turn-based Büchi games and maximal end-component decomposition are two classic graph theoretic problems that are core algorithmic problems in synthesis and verification of probabilistic systems. Moreover, many other problems on graph games reduce to them, and as an example we will first describe how analysis of reachability objectives in concurrent games reduces to Büchi games. We will present recent results that break the O(n*m) barrier for Büchi games, and show how the same techniques break the barrier for maximal end-component decomposition.


Alessio R. Lomuscio (Imperial College London)

Model Checking Systems against Epistemic Specifications.

Twenty years after the publication of the influential article "Model checking vs theorem proving: a manifesto" by Halpern and Vardi, the area of model checking systems against agent-based specifications is flourishing. In this talk I will present some of the approaches I have developed with collaborators. I will begin by discussing BDD-based model checking for epistemic logic combined with ATL operators and then move to abstraction techniques including symmetry reduction. I will then highlight how, in our experience, bounded model checking can also successfully be used in this context, particularly in combination with BDDs, and how synthesis problems can be formulated and solved in an epistemic setting. The talk will include examples in the context of security protocols and a brief demo of MCMAS, an open-source model checker implementing some of these techniques.


Jean-Francois Raskin (Université Libre de Bruxelles)

Looking at Mean-Payoff and Total-Payoff through Windows.

We consider two-player games played on weighted directed graphs with mean-payoff and total-payoff objectives, which are two classical quantitative objectives. While for single dimensional objectives all results for mean-payoff and total-payoff coincide, we show that in contrast to multi-dimensional mean-payoff games that are known to be coNP-complete, multi-dimensional total-payoff games are undecidable. We introduce conservative approximations of these objectives, where the payoff is considered over a local finite window sliding along a play, instead of the whole play. For single dimension, we show that (i) if the window size is polynomial, then the problem can be solved in polynomial time, and (ii) the existence of a bounded window can be decided in NP and in coNP, and is at least as hard as solving mean-payoff games. For multiple dimensions, we show that (i) the problem with fixed window size is ExpTime-complete, and (ii) there is no primitive-recursive algorithm to decide the existence of a bounded window.


Michael Wooldridge (University of Oxford)

Bad Equilibria (and what to do about them).

In economics, an equilibrium is a steady-state situation, which obtains because no participant has any rational incentive to deviate from it. Equilibrium concepts are arguably the most important and widely used analytical weapons in the game theory arsenal. The concept of Nash equilibrium in particular has found a huge range of applications, in areas as diverse and seemingly unrelated as biology and moral philosophy. However, there remain fundamental problems associated with Nash equilibria and their application. First, there may be multiple Nash equilibria, in which case, how should we choose between them? Second, some equilibria may be undesirable, in which case, how can we avoid them? In this presentation, I will introduce work that we have done addressing these problems from a computational/AI perspective. Assuming no prior knowledge of game theory or economic solution concepts, I will discuss various ways in which we can try to engineer a game so that desirable equilibria result, or else engineer out undesirable equilibria. In particular, I will consider thee possible devices for the management of equilibria: taxation, communication, and law-making. While all of these devices are regularly used in human societies, in this work, we consider these as computational problems.