The heterogeneity of tools that support temporal logic formulae poses several challenges in terms of interoperability. In particular, a standard syntax for temporal logic on finite traces, despite similar to the one for infinite traces, is currently missing. This document proposes a standard grammar for several temporal logic formalisms interpreted over finite traces, like Linear Temporal Logic (LTLf), Linear Dynamic Logic (LDLf), Pure-Past Linear Temporal Logic (PLTLf) and Pure-Past Linear Dynamic Logic (PLDLf).

翻译：支持时间逻辑公式的工具的异质性在互操作性方面构成若干挑战。 特别是,目前缺少关于有限痕迹的时间逻辑的标准语法,尽管与无限痕迹相似。 本文件提出了关于解释有限痕迹的一些时间逻辑形式主义的标准语法,如线性时空逻辑(LTLf)、线性动态逻辑(LDLf)、纯-帕斯特线性时空逻辑(PLTLf)和纯-帕斯特线性动态逻辑(PLDLf)。