The Temporal Logic Synthesis Format TLSF v1.2
Logic in Computer Science
2026-04-15 v3
Abstract
We present an extension of the Temporal Logic Synthesis Format (TLSF). TLSF builds on standard LTL, but additionally supports high-level constructs, such as sets and functions, as well as parameters that allow a specification to define a whole a family of problems. Our extension introduces operators and a new semantics option for LTLf, i.e., LTL on finite executions.
Keywords
Cite
@article{arxiv.2303.03839,
title = {The Temporal Logic Synthesis Format TLSF v1.2},
author = {Swen Jacobs and Guillermo A. Perez and Philipp Schlehuber-Caissier},
journal= {arXiv preprint arXiv:2303.03839},
year = {2026}
}
Comments
arXiv admin note: substantial text overlap with arXiv:1604.02284, arXiv:1601.05228; In this update we are clearer in the expectations concerning controllers synthesized for the competition (we want terminating ones and we want a live signal instead of termination signal)