Optimal LTLf Synthesis

• URL: http://arxiv.org/abs/2605.11544v1
• Date: Tue, 12 May 2026 05:17:10 GMT
• Title: Optimal LTLf Synthesis
• Abstract summary: We introduce optimalf synthesis, where the goal is to realise as many objectives as possible from a given specification.<n>We first consider max-guarantee synthesis, which commits to a maximal set of objectives that we can a priori guarantee to realise.<n>We then introduce maxobservation synthesis, which maximises a posteriori realised objectives that may be incomparable on different executions.
• Score: 6.527008293029305
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Position: It's Time to Optimize LLMs for Self-Consistency [50.68587056599734]
  Many important failures persist in language model pre- and post-training pipelines.<n>We argue that these failures arise from a modeling assumption permeating all aspects of the pipeline.<n>We propose self-consistency as a framework for understanding these failures.
  arXiv  Detail & Related papers  (2026-07-31T19:16:53Z)
• From Feasible to Practical: Pareto-Optimal Synthesis Planning [0.0]
  Current computer-aided synthesis planning methods often treat retrosynthesis as solved once a single feasible route is identified.<n>This view is misaligned with real-world practice, where chemists must balance competing objectives such as cost, sustainability, toxicity, and overall yield.<n>We introduce MORetro*, an algorithm that generates a Pareto front of routes to explicitly capture trade-offs among user-defined criteria.
  arXiv  Detail & Related papers  (2026-05-08T09:53:30Z)
• Multi-Property Synthesis [69.79949693440426]
  We study synthesis with multiple properties, where satisfying all properties may be impossible.<n>Instead of enumerating subsets of properties, we compute in one fixed-point computation the relation between product-game states and the goal sets that are realizable from them.
  arXiv  Detail & Related papers  (2026-01-15T18:18:33Z)
• Beyond Log Likelihood: Probability-Based Objectives for Supervised Fine-Tuning across the Model Capability Continuum [88.90314335542281]
  We study a family of probability-based objectives and characterize their effectiveness under different conditions.<n>We uncover a critical dimension that governs objective behavior: the model-capability continuum.<n>Our theoretical analysis further elucidates how objectives trade places across the continuum, providing a principled foundation for adapting objectives to model capability.
  arXiv  Detail & Related papers  (2025-10-01T05:17:47Z)
• Bounded Rationality for LLMs: Satisficing Alignment at Inference-Time [52.230936493691985]
  We propose SITAlign, an inference framework that addresses the multifaceted nature of alignment by maximizing a primary objective while satisfying threshold-based constraints on secondary criteria.<n>We provide theoretical insights by deriving sub-optimality bounds of our satisficing based inference alignment approach.
  arXiv  Detail & Related papers  (2025-05-29T17:56:05Z)
• LTLf Adaptive Synthesis for Multi-Tier Goals in Nondeterministic Domains [24.117872352200948]
  We study a variant of synthesisf synthesis that synthesizes adaptive strategies for achieving a multi-tier goal.<n>We provide a game-theoretic technique to compute adaptive strategies that is sound and complete.
  arXiv  Detail & Related papers  (2025-04-29T17:53:16Z)
• LTLf Best-Effort Synthesis in Nondeterministic Planning Domains [27.106071554421664]
  We study best-effort strategies (aka plans) in fully observable nondeterministic domains (FOND) We present a game-theoretic synthesis technique for synthesizing best-effort strategies that exploit the specificity of nondeterministic planning domains.
  arXiv  Detail & Related papers  (2023-08-29T10:10:41Z)
• ExeDec: Execution Decomposition for Compositional Generalization in Neural Program Synthesis [54.18659323181771]
  We characterize several different forms of compositional generalization that are desirable in program synthesis. We propose ExeDec, a novel decomposition-based strategy that predicts execution subgoals to solve problems step-by-step informed by program execution at each step.
  arXiv  Detail & Related papers  (2023-07-26T01:07:52Z)
• Opportunistic Qualitative Planning in Stochastic Systems with Incomplete Preferences over Reachability Objectives [24.11353445650682]
  Preferences play a key role in determining what goals/constraints to satisfy when not all constraints can be satisfied simultaneously. We present an algorithm to synthesize the SPI and SASI strategies that induce multiple sequential improvements.
  arXiv  Detail & Related papers  (2022-10-04T19:53:08Z)
• Are we Forgetting about Compositional Optimisers in Bayesian Optimisation? [66.39551991177542]
  This paper presents a sample methodology for global optimisation. Within this, a crucial performance-determiningtrivial is maximising the acquisition function. We highlight the empirical advantages of the approach to optimise functionation across 3958 individual experiments.
  arXiv  Detail & Related papers  (2020-12-15T12:18:38Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.