Symbolic ltl$$_f$$ Synthesis: A Unified Approach for Synthesizing Winning, Dominant, and Best-Effort Strategies

Abstract Synthesis typically focuses on finding strategies that win against all possible responses of the environment. When a winning strategy does not exist, the agent can either give up or do its best to achieve the goal. In this paper, we develop symbolic techniques to handle the latter case in the context of ltl $$_f$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mmultiscripts> <mml:mrow/> <mml:mi>f</mml:mi> <mml:mrow/> </mml:mmultiscripts> </mml:math> . Specifically, we consider winning , dominant , and best-effort strategies, which achieve the goal against all , the maximum subset, and a maximal subset of environment responses, respectively. While a unified game-theoretic technique that simultaneously solves the three synthesis problems exists, we present several symbolic refinements of such technique. Depending on key choices, such refinements behave in a radically different way. We provide an effective implementation of our symbolic techniques and show, by empirical evaluation, how they compare in practice. In particular, we show that one of them brings only a minor overhead compared to existing standard synthesis techniques for winning strategies.