# LTLf Synthesis with Fairness and Stability Assumptions

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Dec 2019.

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

- [Act for Your Duties but Maintain Your Rights](https://mlsanity.com/paper/2302.03384/) (2023)
- [Emerson-Lei and Manna-Pnueli Games for LTLf+ and PPLTL+ Synthesis](https://mlsanity.com/paper/2508.14725/) (2025)
- [LTLf Adaptive Synthesis for Multi-Tier Goals in Nondeterministic Domains](https://mlsanity.com/paper/2504.20983/) (2025)
- [Symbolic LTLf Best-Effort Synthesis](https://mlsanity.com/paper/2308.15178/) (2023)
- [Incremental LTLf Synthesis](https://mlsanity.com/paper/2603.01201/) (2026)

## Abstract (arXiv)

In synthesis, assumptions are constraints on the environment that rule out certain environment behaviors. A key observation here is that even if we consider systems with LTLf goals on finite traces, environment assumptions need to be expressed over infinite traces, since accomplishing the agent goals may require an unbounded number of environment action. To solve synthesis with respect to finite-trace LTLf goals under infinite-trace assumptions, we could reduce the problem to LTL synthesis. Unfortunately, while synthesis in LTLf and in LTL have the same worst-case complexity (both 2EXPTIME-complete), the algorithms available for LTL synthesis are much more difficult in practice than those for LTLf synthesis. In this work we show that in interesting cases we can avoid such a detour to LTL synthesis and keep the simplicity of LTLf synthesis. Specifically, we develop a BDD-based fixpoint-based technique for handling basic forms of fairness and of stability assumptions. We show, empirically, that this technique performs much better than standard LTL synthesis.