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.

翻译：本文提出了时序逻辑综合格式（TLSF）的扩展版本。TLSF基于标准线性时序逻辑（LTL），同时额外支持集合与函数等高级结构，以及允许规范定义完整问题族的参数机制。本次扩展引入了新运算符，并为有限执行路径上的线性时序逻辑（LTLf）提供了新的语义选项。