mlsanityData to 14 Oct 2026

Symbolic LTLf Synthesis

arXiv 1705.08426 ↗First posted 23 May 2017cs.LO cs.AIcited by 21

Not on the map. Why?

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.

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

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2021: 1; 2022: 2; 2023: 9; 2024: 4; 2025: 3; 2026: 2.

21 papers.

Sort:

By area:

  1. 2025ShieldAgent: Shielding Agents via Verifiable Safety Policy Reasoningcited by 151
  2. 2024LTLDoG: Satisfying Temporally-Extended Symbolic Constraints for Safe Diffusion-based Planningcited by 16
  3. 2022Learning Interpretable Temporal Properties from Positive Examples Onlycited by 12
  4. 2021Embedding Symbolic Temporal Knowledge into Deep Sequential Modelscited by 11
  5. 2023Specification-Driven Video Search via Foundation Models and Formal Verificationcited by 10
  6. 2025Neuro-Symbolic Predictive Process Monitoringcited by 7
  7. 2023Forward LTLf Synthesis: DPLL At Workcited by 4
  8. 2023Automaton Distillation: Neuro-Symbolic Transfer Learning for Deep Reinforcement Learningcited by 4
  9. 2023Model Checking Strategies from Synthesis Over Finite Tracescited by 3
  10. 2023Act for Your Duties but Maintain Your Rightscited by 2
  11. 2023Optimal Control of Logically Constrained Partially Observable and Multi-Agent Markov Decision Processescited by 2
  12. 2023Reinforcement Learning with Temporal-Logic-Based Causal Diagramscited by 2
9 more
  1. 2023LTLf Best-Effort Synthesis in Nondeterministic Planning Domainscited by 2
  2. 2024LTLf Synthesis on First-Order Agent Programs in Nondeterministic Environmentscited by 1
  3. 2022Mimicking Behaviors in Separated Domainscited by 0
  4. 2023Symbolic LTLf Best-Effort Synthesiscited by 0
  5. 2024On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Countscited by 0
  6. 2024LTLf Synthesis Under Unreliable Inputcited by 0
  7. 2025A Compositional Framework for On-the-Fly LTLf Synthesiscited by 0
  8. 2026Multi-Property Synthesiscited by 0
  9. 2026DeepDFA: Injecting Temporal Logic in Deep Learning for Sequential Subsymbolic Applicationscited by 0