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$-正则游戏的典型表示形式，我们提出了一个多项式时间算法，用于符号计算足够宽容的假设，展示了我们的算法在理论和实践中运行速度更快，生成的假设更好。据我们所知，我们提供了第一个算法来计算充分和可实现的环境假设，同时保持宽容。