Synthesis from LTL with Reward Optimization in Sampled Oblivious Environments

TL;DR

This paper presents a method for synthesizing reactive systems that satisfy hard LTL constraints and optimize soft reward-based constraints in sampled, stochastic environments, using an SMT-based approach.

Contribution

It introduces a formal synthesis framework combining LTL constraints with reward optimization in sampled environments, proving NP-completeness and providing an SMT-based solution.

Findings

The synthesis problem is NP-complete.

The SMT-based approach effectively handles the combined constraints.

Case study demonstrates practical applicability.

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.