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

Swen Jacobs, Felix Klein, Sebastian Schirmer
4/8/2016
cs.LO

Official code: reactive-systems/syfco (28 stars, MIT, last commit 2025-11-18).

Abstract

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.

View on arXivView PDF

Code Implementations(1)

reactive-systems/syfcoOfficial100%
MIT

Synthesis Format Conversion Tool

2815Shell, HaskellOct 27, 201511 months agoMIT

Similar Papers

The Extended HOA Format for Synthesis

82% match2019

FrAngel: Component-Based Synthesis with Control Structures

77% match1 repo262018

DART-Math: Difficulty-Aware Rejection Tuning for Mathematical Problem-Solving

77% match1 repo1202024

MathAgent: Adversarial Evolution of Constraint Graphs for Mathematical Reasoning Data Synthesis

76% match2026

Online Prompt Selection for Program Synthesis

76% match2025

Presburger Functional Synthesis: Complexity and Tractable Normal Forms

75% match2025

Cite this paper

@article{jacobs2016highlevel,
  title  = {A High-Level LTL Synthesis Format: TLSF v1.1},
  author = {Swen Jacobs and Felix Klein and Sebastian Schirmer},
  year   = {2016},
  eprint = {1604.02284},
  archivePrefix = {arXiv},
  url    = {https://arxiv.org/abs/1604.02284}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/1604.02284.svg)](https://codeofpaper.com/paper/1604.02284)

Discussion