Abstract
Linear Temporal Logic over finite traces (LTLf) has proved itself to be an important and effective formalism in formal verification as well as in artificial intelligence. Pure past LTLf (pLTL) is the variant of LTLf featuring only past temporal modalities, and is naturally interpreted at the end of a finite trace. It is known that each property definable in LTLf is also definable in pLTL, and vice versa (they are expressively equivalent). The same goes for the safety and cosafety fragments of Linear Temporal Logic over infinite traces (LTL), when compared to G(pLTL) and F(pLTL) formulas, respectively, that is, pLTL formulas prefixed by a globally and an eventually modality. However, despite being extensively used in practice, to the best of our knowledge, there is no systematic study of their succinctness. Moreover, when considering (co)safety fragments of LTL devoid of binary temporal modalities, there are no known characterizations based on pLTL. In this paper, we investigate succinctness issues for LTLf and (co)safety fragments of LTL when compared with their pure past counterparts. First, we provide a pure past characterization of the (co)safety fragments of LTL devoid of binary temporal modalities. Then, we prove that the (co)safety fragments of LTL have pure past counterparts that can be exponentially more succinct. Finally, we show that the same holds for LTLf with respect to pLTL, and viceversa: LTLf and pLTL are incomparable when succinctness is concerned.