Computing Adequately Permissive Assumptions for Synthesis
Ashwani Anand, Kaushik Mallik, Satya Prakash Nayak, Anne-Kathrin Schmuck
TL;DR
This work tackles automatic synthesis under environment assumptions for two-player ω-regular games, introducing adequately permissive assumptions (APAs) that are simultaneously sufficient, implementable, and permissive. It proposes a unified, polynomial-time approach for parity games by composing three templates—safety, live-group, and co-liveness—decorated with frontier-based acceleration via the μ-calculus to compute the APA components. The main contribution is a formal, executable construction (Alg. parityAssump) that yields APAs for parity games with provable sufficiency, implementability, and permissiveness and is implemented in a C++ tool that outperforms prior methods on standard benchmarks and a 2-client arbiter scenario. This advances scalable, distributed, and correct-by-design synthesis by ensuring environment cooperation is expressed without unnecessarily restricting cooperative strategies.
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 $ω$-regular winning condition $Φ$ for the system player, we compute an $ω$-regular assumption $Ψ$ for the environment player, such that (i) every environment strategy compliant with $Ψ$ allows the system to fulfill $Φ$ (sufficiency), (ii) $Ψ$ can be fulfilled by the environment for every strategy of the system (implementability), and (iii) $Ψ$ 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.