This week I’m attending ATVA’14. On Monday we started with a series of tutorial talks, the first one by Krishnendu Chatterjee. Once available I’ll update the post with a link to the slides.
Krishnendu started of by introducing two-player games in general, using three motivating examples:
- Concurrency synthesis, e.g. synthesising locks in concurrent programs, where the objective is the have maximal performance without introducing data races.
- Incompatible synthesis, i.e. synthesising a program satisfying a set of Boolean objectives that cannot all be satisfied at the same time. The objective is then, e.g., to satisfy as many of them as possible.
- Quantitative simulation, which is useful in the case that programs cannot simulate each other exactly, now the problem is to match steps as closely as possible.
In the first part of the talk Krishnendu very clearly introduced quantitative games, in particular mean-payoff games (objectives about long-run averages), as well as lim-inf and lim-sup objectives. Mean pay-off games are two-player games in which the edges carry some (possibly negative) integer weight. The game is played by two players, player 1 and player 2, and the objective for player 1 is to make sure that the long run average of these weights exceeds a certain threshold. He explained the consequences of the choice for memoryless and finite- and infinite-memory strategies in this setting: mean-payoff games are memoryless determined, so having finite or infinite memory does not change the expressive power. Deciding whether player 1 has a winning strategy is in NP and co-NP.
The second part of the tutorial focused on generalising the ideas in mean-payoff games to the multidimensional setting. This means that instead of satisfying a single mean-payoff objective, multiple objectives have to be satisfied. There are multiple reward functions on the edges, and player 1 wins if all mean-payoff objectives are satisfied. He studies the impact of this w.r.t. different problems. It turns out that:
- infinite memory strategies are more powerful than finite memory strategies, which in turn are more powerful than memoryless strategies.
- determining winning in the setting with finite memories is co-NP complete.
In the process, he shows an algorithm that uses a linear programming approach to compute flows in strongly connected components in the game graph (to encode the mean payoff objective), and proofs some properties using the principle of edge induction. Both approaches are somewhat of a recurring theme, that you should check out! (I will add some reference later)
In the third part of his talk, he generalises the above ideas to Markov Decision Processes; here the algorithmic approach does not use SCCs, but instead work on maximal end components.
During his talk, Krishnendu introduces several open problems. One of which is to determine whether deciding winning in multi-dimensional mean-payoff games with finite memory is polynomial time computable.