Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Synthesis from LTL with Reward Optimization in Sampled Oblivious Environments

Jean-François Raskin, Yun Chen Tsai

TL;DR

This paper addresses the synthesis of reactive systems that enforce hard constraints while optimizing for quality-based soft constraints in stochastic, oblivious environments accessible only through sampling, and proposes an SMT-based solution.

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.

Synthesis from LTL with Reward Optimization in Sampled Oblivious Environments

TL;DR

This paper addresses the synthesis of reactive systems that enforce hard constraints while optimizing for quality-based soft constraints in stochastic, oblivious environments accessible only through sampling, and proposes an SMT-based solution.

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.

Paper Structure

This paper contains 20 sections, 5 theorems, 23 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Related works
  3. Structure of the paper
  4. Preliminaries
  5. LTL and the realizability problem
  6. Realizability game
  7. Automata-based approach to realizablility
  8. Pre-Mealy, Mealy and reward machines
  9. Sample trees
  10. Partial strategy and expected reward
  11. The problem and its algorithm
  12. Computing the partial strategy
  13. Hardness
  14. SMT based solution
  15. Solving the Optimality
  16. ...and 5 more sections

Key Result

theorem 1

The realizability problem for LTL is 2ExpTime-C.

Figures (5)

  • Figure 1: illustration of the automata
  • Figure 2: An example of sample tree.
  • Figure 3: The reward machine is designed to penalize false warning signals in hindsight.
  • Figure 4: The Markov Chain for modelling the environment
  • Figure 5: The completed Mealy machine

Theorems & Definitions (6)

  • theorem 1
  • theorem 2
  • theorem 3
  • theorem 4
  • definition 1
  • lemma 1