The Temporal Logic Synthesis Format TLSF v1.2
arXiv:2303.03839
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.
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)