cs.AIMay 12, 2026

Optimal LTLf Synthesis

Authors: Yujian CaoSven ScheweQiyi TangShufang Zhu

Organizations: University of Liverpool

Abstract

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.

Explore similar work

CardsList
  1. Symbolic Synthesis for LTLf+ Obligations

    Apr 20, 2026Giuseppe De Giacomo, Christian Hagemeier, Daniel Hausmann +1Linear Temporal LogicsConstraint-Aware Synthesis

  2. SemML 2.0: Synthesizing Controllers for LTL

    Apr 27, 2026Jan Křetínský, Tobias Meggendorfer, Maximilian ProkopLinear Temporal LogicsConstraint-Aware Synthesis