# LTLf Synthesis Under Environment Specifications for Reachability and Safety Properties

arXiv: https://arxiv.org/abs/2308.15184 · HTML: https://mlsanity.com/paper/2308.15184/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 2 of its 32 references that are in the map.
- First posted on arXiv 29 Aug 2023.

## Builds on (most cited first, 2 of 2)

- [Planning and Synthesis Under Assumptions](https://mlsanity.com/paper/1807.06777/) (2018)
- [Finite LTL Synthesis with Environment Assumptions and Quality Measures](https://mlsanity.com/paper/1808.10831/) (2018)

## Built on by (most cited first, 1 of 1)

- [LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces](https://mlsanity.com/paper/2411.09366/) (2024)

## Abstract (arXiv)

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.