LTLf synthesis under environment specifications for reachability and safety properties
In this paper, we study LTLf synthesis under environment specifications for arbitrary reachability and safety properties. We consider both kinds of properties for both agent tasks and environment specifications, providing a complete landscape of synthesis algorithms. For each case, we devise a speci...
| Main Authors: | , , , , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Springer
2023
|
| _version_ | 1797112453584125952 |
|---|---|
| author | Aminof, B De Giacomo, G Di Stasio, A Francon, H Rubin, S Zhu, S |
| author_facet | Aminof, B De Giacomo, G Di Stasio, A Francon, H Rubin, S Zhu, S |
| author_sort | Aminof, B |
| collection | OXFORD |
| description | In this paper, we study LTLf synthesis under environment specifications for arbitrary reachability and safety properties. We consider both kinds of properties for both agent tasks and environment specifications, providing a complete landscape of synthesis algorithms. For each case, we devise a specific algorithm (optimal wrt complexity of the problem) and prove its correctness. The algorithms combine common building blocks in different ways. While some cases are already studied in literature others are studied here for the first time. |
| first_indexed | 2024-03-07T08:24:29Z |
| format | Conference item |
| id | oxford-uuid:4eb4cea0-0b33-4b60-a023-d20916782dfa |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T08:24:29Z |
| publishDate | 2023 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:4eb4cea0-0b33-4b60-a023-d20916782dfa2024-02-12T14:56:27ZLTLf synthesis under environment specifications for reachability and safety propertiesConference itemhttp://purl.org/coar/resource_type/c_5794uuid:4eb4cea0-0b33-4b60-a023-d20916782dfaEnglishSymplectic ElementsSpringer2023Aminof, BDe Giacomo, GDi Stasio, AFrancon, HRubin, SZhu, SIn this paper, we study LTLf synthesis under environment specifications for arbitrary reachability and safety properties. We consider both kinds of properties for both agent tasks and environment specifications, providing a complete landscape of synthesis algorithms. For each case, we devise a specific algorithm (optimal wrt complexity of the problem) and prove its correctness. The algorithms combine common building blocks in different ways. While some cases are already studied in literature others are studied here for the first time. |
| spellingShingle | Aminof, B De Giacomo, G Di Stasio, A Francon, H Rubin, S Zhu, S LTLf synthesis under environment specifications for reachability and safety properties |
| title | LTLf synthesis under environment specifications for reachability and safety properties |
| title_full | LTLf synthesis under environment specifications for reachability and safety properties |
| title_fullStr | LTLf synthesis under environment specifications for reachability and safety properties |
| title_full_unstemmed | LTLf synthesis under environment specifications for reachability and safety properties |
| title_short | LTLf synthesis under environment specifications for reachability and safety properties |
| title_sort | ltlf synthesis under environment specifications for reachability and safety properties |
| work_keys_str_mv | AT aminofb ltlfsynthesisunderenvironmentspecificationsforreachabilityandsafetyproperties AT degiacomog ltlfsynthesisunderenvironmentspecificationsforreachabilityandsafetyproperties AT distasioa ltlfsynthesisunderenvironmentspecificationsforreachabilityandsafetyproperties AT franconh ltlfsynthesisunderenvironmentspecificationsforreachabilityandsafetyproperties AT rubins ltlfsynthesisunderenvironmentspecificationsforreachabilityandsafetyproperties AT zhus ltlfsynthesisunderenvironmentspecificationsforreachabilityandsafetyproperties |