Computing Adequately Permissive Assumptions for Synthesis

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 ω-regular winning condition Phi for the system player, we compute an ω-regular assumption Psi for the environment player, such that (i) every environment strategy compliant with Psi allows the system to fulfill Phi (sufficiency), (ii) Psi can be fulfilled by the environment for every strategy of the system (implementability), and (iii) Psi does not prevent any cooperative strategy choice (permissiveness). For parity games, which are canonical representations of ω-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 ω-regular games, we provide the first algorithm to compute sufficient and implementable environment assumptions that are also permissive.