2026-07-21T19:26:05Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:19092 2024-03-06T11:03:10Z ddc:004 open_access

LTL over Finite Words Can Be Exponentially More Succinct Than Pure-Past LTL, and vice versa Artale, Alessandro Geatti, Luca Gigante, Nicola Mazzullo, Andrea Montanari, Angelo Temporal Logic Succinctness LTLf Finite Traces Pure past LTL Linear Temporal Logic over finite traces (LTL_𝖿) has proved itself to be an important and effective formalism in formal verification as well as in artificial intelligence. Pure past LTL_𝖿 (pLTL) is the logic obtained from LTL_𝖿 by replacing each (future) temporal operator by a corresponding past one, and is naturally interpreted at the end of a finite trace. It is known that each property definable in LTL_𝖿 is also definable in pLTL, and ǐceversa. However, despite being extensively used in practice, to the best of our knowledge, there is no systematic study of their succinctness. In this paper, we investigate the succinctness of LTL_𝖿 and pLTL. First, we prove that pLTL can be exponentially more succinct than LTL_𝖿 by showing that there exists a property definable with a pLTL formula of size n such that the size of all LTL_𝖿 formulas defining it is at least exponential in n. Then, we prove that LTL_𝖿 can be exponentially more succinct than pLTL as well. This result shows that, although being expressively equivalent, LTL_𝖿 and pLTL are incomparable when succinctness is concerned. In addition, we study the succinctness of Safety-LTL (the syntactic safety fragment of LTL over infinite traces) with respect to its canonical form G(pLTL), whose formulas are of the form G(α), G being the globally operator and α a pLTL formula. We prove that G(pLTL) can be exponentially more succinct than Safety-LTL, and that the same holds for the dual cosafety fragment. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alessandro Artale and Luca Geatti and Nicola Gigante and Andrea Mazzullo and Angelo Montanari 2023 Is Part Of LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TIME.2023.2 urn:nbn:de:0030-drops-190927 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.2 eng https://creativecommons.org/licenses/by/4.0/legalcode