LTLf Synthesis Under Environment Specifications for Reachability and Safety Properties
Logic in Computer Science
2023-08-30 v1 Artificial Intelligence
Formal Languages and Automata Theory
Systems and Control
Systems and Control
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.
Keywords
Cite
@article{arxiv.2308.15184,
title = {LTLf Synthesis Under Environment Specifications for Reachability and Safety Properties},
author = {Benjamin Aminof and Giuseppe De Giacomo and Antonio Di Stasio and Hugo Francon and Sasha Rubin and Shufang Zhu},
journal= {arXiv preprint arXiv:2308.15184},
year = {2023}
}
Comments
To appear at EUMAS2023