# Symbolic LTLf Synthesis

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

## Key facts

- Cited by 21 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 23 May 2017.

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

- [ShieldAgent: Shielding Agents via Verifiable Safety Policy Reasoning](https://mlsanity.com/paper/2503.22738/) (2025)
- [LTLDoG: Satisfying Temporally-Extended Symbolic Constraints for Safe Diffusion-based Planning](https://mlsanity.com/paper/2405.04235/) (2024)
- [Learning Interpretable Temporal Properties from Positive Examples Only](https://mlsanity.com/paper/2209.02650/) (2022)
- [Embedding Symbolic Temporal Knowledge into Deep Sequential Models](https://mlsanity.com/paper/2101.11981/) (2021)
- [Specification-Driven Video Search via Foundation Models and Formal Verification](https://mlsanity.com/paper/2309.10171/) (2023)
- [Neuro-Symbolic Predictive Process Monitoring](https://mlsanity.com/paper/2509.00834/) (2025)
- [Forward LTLf Synthesis: DPLL At Work](https://mlsanity.com/paper/2302.13825/) (2023)
- [Automaton Distillation: Neuro-Symbolic Transfer Learning for Deep Reinforcement Learning](https://mlsanity.com/paper/2310.19137/) (2023)
- [Model Checking Strategies from Synthesis Over Finite Traces](https://mlsanity.com/paper/2305.08319/) (2023)
- [Act for Your Duties but Maintain Your Rights](https://mlsanity.com/paper/2302.03384/) (2023)
- [Optimal Control of Logically Constrained Partially Observable and Multi-Agent Markov Decision Processes](https://mlsanity.com/paper/2305.14736/) (2023)
- [Reinforcement Learning with Temporal-Logic-Based Causal Diagrams](https://mlsanity.com/paper/2306.13732/) (2023)
- [LTLf Best-Effort Synthesis in Nondeterministic Planning Domains](https://mlsanity.com/paper/2308.15188/) (2023)
- [LTLf Synthesis on First-Order Agent Programs in Nondeterministic Environments](https://mlsanity.com/paper/2410.00726/) (2024)
- [Mimicking Behaviors in Separated Domains](https://mlsanity.com/paper/2205.09201/) (2022)
- [Symbolic LTLf Best-Effort Synthesis](https://mlsanity.com/paper/2308.15178/) (2023)
- [On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts](https://mlsanity.com/paper/2408.07324/) (2024)
- [LTLf Synthesis Under Unreliable Input](https://mlsanity.com/paper/2412.14728/) (2024)
- [A Compositional Framework for On-the-Fly LTLf Synthesis](https://mlsanity.com/paper/2508.04116/) (2025)
- [Multi-Property Synthesis](https://mlsanity.com/paper/2601.10651/) (2026)
- [DeepDFA: Injecting Temporal Logic in Deep Learning for Sequential Subsymbolic Applications](https://mlsanity.com/paper/2602.03486/) (2026)

## Abstract (arXiv)

LTLf synthesis is the process of finding a strategy that satisfies a linear temporal specification over finite traces. An existing solution to this problem relies on a reduction to a DFA game. In this paper, we propose a symbolic framework for LTLf synthesis based on this technique, by performing the computation over a representation of the DFA as a boolean formula rather than as an explicit graph. This approach enables strategy generation by utilizing the mechanism of boolean synthesis. We implement this symbolic synthesis method in a tool called Syft, and demonstrate by experiments on scalable benchmarks that the symbolic approach scales better than the explicit one.