Strategy synthesis typically follows an all-or-nothing paradigm, returning unrealisable whenever a specification cannot be guaranteed in an uncertain environment. In this paper, we introduce optimal LTLf synthesis, where the goal is to realise as many objectives as possible from a given specification consisting of multiple objectives, especially for the case that they are not all jointly realisable. We first consider max-guarantee synthesis, which commits to a maximal set of objectives that we can a priori guarantee to realise. We then introduce max-observation synthesis, which maximises a posteriori realised objectives that may be incomparable on different executions. Finally, we present incremental max-observation synthesis, which further improves strategies by exploiting opportunities for stronger guarantees when they arise during an execution. Experimental results show that different variations of optimal synthesis scale broadly equally well, solving a large fraction of the benchmark instances within the given timeout, demonstrating the practical feasibility of the approach.

翻译：策略综合通常遵循“全有或全无”范式，当规范无法在不确定环境中得到保证时，返回不可实现结果。本文引入最优LTLf综合，其目标是从包含多个目标的给定规范中尽可能多地实现目标，尤其适用于所有目标无法共同实现的情形。我们首先考虑最大保证综合，该方案承诺选择一组可先验保证实现的最大目标集。随后引入最大观测综合，旨在最大化后验可实现的目标，这些目标在不同执行轨迹上可能不可比较。最后，我们提出增量式最大观测综合，通过在执行过程中利用出现更强保证的时机进一步改进策略。实验结果表明，最优综合的不同变体扩展规模大致相当，能在给定超时时间内解决大部分基准测试实例，验证了该方法在实际中的可行性。