Search Results

Documents authored by Artale, Alessandro

Document
DOI: 10.4230/LIPIcs.TIME.2023.2
LTL over Finite Words Can Be Exponentially More Succinct Than Pure-Past LTL, and vice versa

Authors: Alessandro Artale, Luca Geatti, Nicola Gigante, Andrea Mazzullo, and Angelo Montanari

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

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.
Cite as

Alessandro Artale, Luca Geatti, Nicola Gigante, Andrea Mazzullo, and Angelo Montanari. LTL over Finite Words Can Be Exponentially More Succinct Than Pure-Past LTL, and vice versa. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.TIME.2023.2},
  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}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.TIME.2017.1
Ontology-Mediated Query Answering over Temporal Data: A Survey (Invited Talk)

Authors: Alessandro Artale, Roman Kontchakov, Alisa Kovtunova, Vladislav Ryzhikov, Frank Wolter, and Michael Zakharyaschev

Published in: LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)

Abstract
We discuss the use of various temporal knowledge representation formalisms for ontology-mediated query answering over temporal data. In particular, we analyse ontology and query languages based on the linear temporal logic LTL, the multi-dimensional Halpern-Shoham interval temporal logic HS_n, as well as the metric temporal logic MTL. Our main focus is on the data complexity of answering temporal ontology-mediated queries and their rewritability into standard first-order and datalog queries.
Cite as

Alessandro Artale, Roman Kontchakov, Alisa Kovtunova, Vladislav Ryzhikov, Frank Wolter, and Michael Zakharyaschev. Ontology-Mediated Query Answering over Temporal Data: A Survey (Invited Talk). In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 1:1-1:37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{artale_et_al:LIPIcs.TIME.2017.1,
  author =	{Artale, Alessandro and Kontchakov, Roman and Kovtunova, Alisa and Ryzhikov, Vladislav and Wolter, Frank and Zakharyaschev, Michael},
  title =	{{Ontology-Mediated Query Answering over Temporal Data: A Survey}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{1:1--1:37},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-052-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{90},
  editor =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.1},
  URN =		{urn:nbn:de:0030-drops-79338},
  doi =		{10.4230/LIPIcs.TIME.2017.1},
  annote =	{Keywords: Description Logic, Temporal Logic, Ontology Mediated Query Answering, Data Complexity}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact