# Finite LTL Synthesis with Environment Assumptions and Quality Measures

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 31 Aug 2018.

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

- [Compositional Automata Embeddings for Goal-Conditioned Reinforcement Learning](https://mlsanity.com/paper/2411.00205/) (2024)
- [Act for Your Duties but Maintain Your Rights](https://mlsanity.com/paper/2302.03384/) (2023)
- [L^*LM: Learning Automata from Examples using Natural Language Oracles](https://mlsanity.com/paper/2402.07051/) (2024)
- [LTLf Synthesis Under Environment Specifications for Reachability and Safety Properties](https://mlsanity.com/paper/2308.15184/) (2023)

## Abstract (arXiv)

In this paper, we investigate the problem of synthesizing strategies for linear temporal logic (LTL) specifications that are interpreted over finite traces -- a problem that is central to the automated construction of controllers, robot programs, and business processes. We study a natural variant of the finite LTL synthesis problem in which strategy guarantees are predicated on specified environment behavior. We further explore a quantitative extension of LTL that supports specification of quality measures, utilizing it to synthesize high-quality strategies. We propose new notions of optimality and associated algorithms that yield strategies that best satisfy specified quality measures. Our algorithms utilize an automata-game approach, positioning them well for future implementation via existing state-of-the-art techniques.