# A High-Level LTL Synthesis Format: TLSF v1.1

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 8 Apr 2016.

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

- [Neural Circuit Synthesis from Specification Patterns](https://mlsanity.com/paper/2107.11864/) (2021)
- [SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning](https://mlsanity.com/paper/2501.17496/) (2025)
- [NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis](https://mlsanity.com/paper/2401.12131/) (2024)
- [SemML 2.0: Synthesizing Controllers for LTL](https://mlsanity.com/paper/2604.24102/) (2026)

## Abstract (arXiv)

We present the Temporal Logic Synthesis Format (TLSF), a high-level format to describe synthesis problems via Linear Temporal Logic (LTL). The format builds upon standard LTL, but additionally allows to use high-level constructs, such as sets and functions, to provide a compact and human-readable representation. Furthermore, the format allows to identify parameters of a specification such that a single description can be used to define a family of problems. Additionally, we present a tool to automatically translate the format into plain LTL, which then can be used for synthesis by a solver. The tool also allows to adjust parameters of the specification and to apply standard transformations on the resulting formula.