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 $\omega$-regular winning condition $\Phi$ for the system player, we compute an $\omega$-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 $\omega$-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 $\omega$-regular games, we provide the first algorithm to compute sufficient and implementable environment assumptions that are also permissive.

翻译：我们解决了在双人回合制有限图博弈中自动计算一类新型环境假设的问题，这类假设刻画了系统玩家获胜所需环境提供的“充分合作”。给定系统玩家的$\omega$-正则获胜条件$\Phi$，我们为环境玩家计算出一个$\omega$-正则假设$\Psi$，使得：(i) 每个符合$\Psi$的环境策略都允许系统实现$\Phi$（充分性），(ii) 对于系统的任何策略，环境都能满足$\Psi$（可实现性），(iii) $\Psi$不会阻止任何合作性策略选择（容许性）。对于作为$\omega$-正则博弈典范表示的奇偶博弈，我们提出一种用于符号化计算充分容许性假设的多项式时间算法，并证明该算法在理论上和实验上均比现有方法运行更快且生成更优的假设。据我们所知，针对$\omega$-正则博弈，这是首个能够计算兼具充分性、可实现性与容许性的环境假设的算法。