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

  • Jean-François Raskin,
  • Yun Chen Tsai

摘要

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.