A Standard Grammar for Temporal Logics on Finite Traces
This work provides a standard grammar for temporal logics on finite traces, which is crucial for developers and researchers working with formal verification and synthesis tools to ensure interoperability.
This paper addresses the lack of a standard syntax for temporal logics on finite traces by proposing a unified grammar. It covers several formalisms including LTLf, LDLf, PLTLf, and PLDLf, aiming to improve interoperability among tools.
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).