让无法全实现的复杂目标，优先达成最多可行部分。
Optimal LTLf Synthesis
- 按优先级最大化可保证达成的目标集合
- 后验优化策略，动态提升实际达成目标数
- 适合目标冲突、环境不确定的智能系统设计
传统策略合成采用全有或全无模式，一旦规范无法在不确定环境中被完全满足即判定为不可行。本文提出最优LTLf合成，旨在从包含多个目标的规范中尽可能实现更多目标，尤其适用于目标间无法全部共存的情况。首先提出最大保障合成，预先确定可确保实现的最大目标子集；接着引入最大观测合成，后验最大化不同执行路径中实际达成的目标数，即使目标间不可比较；最后提出增量式最大观测合成，利用执行过程中的新机会进一步强化保障能力。实验表明，不同变体在基准测试中均具有相似良好的可扩展性，多数实例在限定超时内求解成功，验证了该方法的实用性。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。