Synthesis from LTL with Reward Optimization in Sampled Oblivious Environments
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866912069060657152 |
|---|---|
| author | Raskin, Jean-François Tsai, Yun Chen |
| author_facet | Raskin, Jean-François Tsai, Yun Chen |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_08599 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Synthesis from LTL with Reward Optimization in Sampled Oblivious Environments Raskin, Jean-François Tsai, Yun Chen Formal Languages and Automata Theory 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. |
| title | Synthesis from LTL with Reward Optimization in Sampled Oblivious Environments |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2410.08599 |