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

Swen Jacobs
(Saarland University)
Felix Klein
(Saarland University)
Sebastian Schirmer
(Saarland University)

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.

In Ruzica Piskac and Rayna Dimitrova: Proceedings Fifth Workshop on Synthesis (SYNT 2016), Toronto, Canada, July 17-18, 2016, Electronic Proceedings in Theoretical Computer Science 229, pp. 112–132.
Published: 22nd November 2016.

ArXived at: https://dx.doi.org/10.4204/EPTCS.229.10 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org