Computing Adequately Permissive Assumptions for Synthesis

TL;DR

This paper introduces a polynomial-time algorithm for automatically computing environment assumptions in two-player games, ensuring system success, implementability, and permissiveness, with improvements over existing methods.

Contribution

It presents the first algorithm for computing sufficiently permissive environment assumptions in $\omega$-regular games, combining sufficiency, implementability, and permissiveness.

Findings

Algorithm runs faster than existing approaches.

Produces better assumptions both theoretically and empirically.

First to compute assumptions that are sufficient, implementable, and permissive for $\omega$-regular games.

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 $\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.