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.
LTLf Synthesis Under Environment Specifications for Reachability and Safety Properties / Aminof, B.; De Giacomo, G.; Di Stasio, A.; Francon, H.; Rubin, S.; Zhu, S.. - 14282:(2023), pp. 263-279. (Intervento presentato al convegno European Conference on Multi-Agent Systems tenutosi a Naples; Italy) [10.1007/978-3-031-43264-4_17].
LTLf Synthesis Under Environment Specifications for Reachability and Safety Properties
Aminof B.
;De Giacomo G.
;Di Stasio A.
;Zhu S.
2023
Abstract
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.| File | Dimensione | Formato | |
|---|---|---|---|
|
Benjamin_LTLf-Synthesis-Under_2023.pdf
solo gestori archivio
Tipologia:
Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
420 kB
Formato
Adobe PDF
|
420 kB | Adobe PDF | Contatta l'autore |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
