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综合问题。我们同时考虑代理任务与环境规约的这两类属性，提供了综合算法的完整图景。针对每种情况，我们设计了特定算法（在问题复杂度方面达到最优）并证明了其正确性。这些算法以不同方式组合了通用构建模块。其中部分情况已有文献研究，另一些情况则首次在此探讨。