We study best-effort strategies (aka plans) in fully observable
nondeterministic domains (FOND) for goals expressed in Linear Temporal Logic on
Finite Traces (LTLf). The notion of best-effort strategy has been introduced to
also deal with the scenario when no agent strategy exists that fulfills the
goal against every possible nondeterministic environment reaction. Such
strategies fulfill the goal if possible, and do their best to do so otherwise.
We present a game-theoretic technique for synthesizing best-effort strategies
that exploit the specificity of nondeterministic planning domains. We formally
show its correctness and demonstrate its effectiveness experimentally,
exhibiting a much greater scalability with respect to a direct best-effort
synthesis approach based on re-expressing the planning domain as generic
environment specifications.

我们研究可在完全可观察、非确定性领域（FOND）中使用线性时态逻辑有限轨迹（LTLf）表示的目标的尽力策略（又称计划）。我们提出了一种基于博弈论的技术，用于合成利用非确定性规划领域特性的尽力策略。我们在形式上证明了其正确性，并在实验中展示了其有效性，相对于基于将规划领域重新表达为通用环境规范的直接尽力合成方法，其可扩展性大大提高。