Do Your Best, but Don’t Take Too Many Chances: LTLf Synthesis of Minimal Best-Effort Strategies in FOND Domains

Inspired by Joker strategies in games on graphs, we introduce and study the synthesis problem of minimal best-effort strategies for goals expressed in Linear Temporal Logic on Finite Traces (LTLf), assuming that the agent operates in a Fully Observable Nondeterministic (FOND) domain. Minimal best-effort strategies always exist and guarantee that, when a winning strategy does not exist: (i) the agent does its best to achieve its goal; (ii) it relies the least on the environment's cooperation. We present a game-theoretic algorithm to synthesize minimal best-effort strategies and prove its correctness as well as its optimality (wrt computational complexity). We implemented the algorithm and performed an experimental analysis on scalable benchmarks. The empirical results show that the computation of minimal best-effort strategies is quite efficient: it only requires a small overhead compared to standard best-effort strategies.