Synthesis from LTL with Reward Optimization in Sampled Oblivious Environments

2024/10/11 by Jean-François Raskin, Raskin, Jean-François, Yun Chen Tsai +1
Mathematics · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Numerical methods for differential equations

paper · pdf · doi:10.48550/arxiv.2410.08599

openalex publication_date 2024/10/11 · openalex created_date 2024/10/16 · openalex updated_date 2026/07/28

Abstract

This paper addresses the synthesis of reactive systems that enforce hard constraints while optimizing for quality-based soft constraints. We build on recent advancements in combining reactive synthesis with example-based guidance to handle both types of constraints in stochastic, oblivious environments accessible only through sampling. Our approach constructs examples that satisfy LTL-based hard constraints while maximizing expected rewards-representing the soft constraints-on samples drawn from the environment. We formally define this synthesis problem, prove it to be NP-complete, and propose an SMT-based solution, demonstrating its effectiveness with a case study.

Related

• High-Quality Synthesis Against Stochastic Environments
• Finite LTL Synthesis with Environment Assumptions and Quality Measures
• Synthesis from LTL Specifications with Mean-Payoff Objectives
• Synthesis from Satisficing and Temporal Goals
• Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis