Abstract: We solve the problem of automatically computing a new class of environment assumptions in two-player turn-based finite graph games which characterize an "adequate cooperation" needed from the environment to allow the system player to win. Given an o-regular winning condition F for the system player, we compute an o-regular assumption Ps for the environment player, such that (i) every environment strategy compliant with Ps allows the system to fulfill F (sufficiency), (ii) Ps can be fulfilled by the environment for every strategy of the system (implementability), and (iii) Ps does not prevent any cooperative strategy choice (permissiveness).
For parity games, which are canonical representations of o-regular games, we present a polynomial-time algorithm for the symbolic computation of adequately permissive assumptions and show that our algorithm runs faster and produces better assumptions than existing approaches--both theoretically and empirically. To the best of our knowledge, for o-regular games, we provide the first algorithm to compute sufficient and implementable environment assumptions that are also permissive.
In the second part of the talk, we apply the lessons learned to strategies computation, and negotiations between multiple agents. This is joint work with Kaushik Mallik, Satya Prakash Nayak, and Anne-Kathrin Schmuck.
Bio: Ashwani Anand is a 3rd year PhD student at the Max Planck Institute for Software Systems, Germany, advised by Rupak Majumdar and Anne-Kathrin Schmuck. His research focuses on the verification and synthesis of distributed systems.