License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TIME.2023.2
URN: urn:nbn:de:0030-drops-190927
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/19092/
Artale, Alessandro ;
Geatti, Luca ;
Gigante, Nicola ;
Mazzullo, Andrea ;
Montanari, Angelo
LTL over Finite Words Can Be Exponentially More Succinct Than Pure-Past LTL, and vice versa
Abstract
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.
BibTeX - Entry
@InProceedings{artale_et_al:LIPIcs.TIME.2023.2,
author = {Artale, Alessandro and Geatti, Luca and Gigante, Nicola and Mazzullo, Andrea and Montanari, Angelo},
title = {{LTL over Finite Words Can Be Exponentially More Succinct Than Pure-Past LTL, and vice versa}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {2:1--2:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/19092},
URN = {urn:nbn:de:0030-drops-190927},
doi = {10.4230/LIPIcs.TIME.2023.2},
annote = {Keywords: Temporal Logic, Succinctness, LTLf, Finite Traces, Pure past LTL}
}
|
Keywords: |
|
Temporal Logic, Succinctness, LTLf, Finite Traces, Pure past LTL |
|
Collection: |
|
30th International Symposium on Temporal Representation and Reasoning (TIME 2023) |
|
Issue Date: |
|
2023 |
|
Date of publication: |
|
18.09.2023 |
