ltl Synthesis Under Environment Specifications for Reachability and Safety Properties
Aminof, B., De Giacomo, G., Di Stasio, A. 
ORCID: 0000-0001-5475-2978 , Francon, H., Rubin, S. & Zhu, S. (2025).
ltl Synthesis Under Environment Specifications for Reachability and Safety Properties.
Information and Computation, 303,
article number 105255.
doi: 10.1016/j.ic.2024.105255
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.
| Publication Type: | Article |
|---|---|
| Additional Information: | This is an open access article distributed under the terms of the Creative Commons CC-BY license, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited. |
| Subjects: | Q Science > QA Mathematics > QA75 Electronic computers. Computer science |
| Departments: | School of Science & Technology School of Science & Technology > Computer Science |
| SWORD Depositor: |
Available under License Creative Commons Attribution.
Download (504kB) | Preview
Export
Downloads
Downloads per month over past year
Metadata
MetadataActions (login required)
Admin Login