Search Results

Documents authored by Geatti, Luca

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
Extended Abstract
DOI: 10.4230/LIPIcs.TIME.2023.21
Torwards Infinite-State Verification and Planning with Linear Temporal Logic Modulo Theories (Extended Abstract)

Authors: Luca Geatti, Alessandro Gianola, and Nicola Gigante

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

Abstract
In this extended abstract, we discuss about Linear Temporal Logic Modulo Theories over finite traces (LTL_f^MT), a temporal logic that we recently introduced with the goal of providing an equilibrium between generality of the formalism and decidability of the logic. After recalling its distinguishing features, we discuss some future applications.
Cite as

Luca Geatti, Alessandro Gianola, and Nicola Gigante. Torwards Infinite-State Verification and Planning with Linear Temporal Logic Modulo Theories (Extended Abstract). In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 21:1-21:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{geatti_et_al:LIPIcs.TIME.2023.21,
  author =	{Geatti, Luca and Gianola, Alessandro and Gigante, Nicola},
  title =	{{Torwards Infinite-State Verification and Planning with Linear Temporal Logic Modulo Theories}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{21:1--21:3},
  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.21},
  URN =		{urn:nbn:de:0030-drops-191110},
  doi =		{10.4230/LIPIcs.TIME.2023.21},
  annote =	{Keywords: Linear Temporal Logic, Satisfiability Modulo Theories}
}
Document
Extended Abstract
DOI: 10.4230/LIPIcs.TIME.2023.22
Qualitative past Timeline-Based Games (Extended Abstract)

Authors: Renato Acampora, Luca Geatti, Nicola Gigante, and Angelo Montanari

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

Abstract
This extended abstract discusses timeline-based planning, a modeling approach that offers a unique way to model complex systems. Recently, the timeline-based planning framework has been extended to handle general nondeterminism in a game-theoretic setting, resulting in timeline-based games. In this context, the problem of establishing whether a timeline-based game admits a winning strategy and synthesizing such a strategy have been addressed. We propose exploring simpler yet expressive fragments of timeline-based games by leveraging results about the role of past operators in synthesis from temporal logic specifications. The qualitative fragment of timeline-based planning is a good starting point for this exploration. We suggest introducing syntactic restrictions on synchronization rules so that they only constrain the behavior of the system before the current time point, which is expected to lower the complexity of synthesizing timeline-based games to EXPTIME.
Cite as

Renato Acampora, Luca Geatti, Nicola Gigante, and Angelo Montanari. Qualitative past Timeline-Based Games (Extended Abstract). In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 22:1-22:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{acampora_et_al:LIPIcs.TIME.2023.22,
  author =	{Acampora, Renato and Geatti, Luca and Gigante, Nicola and Montanari, Angelo},
  title =	{{Qualitative past Timeline-Based Games}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{22:1--22:3},
  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.22},
  URN =		{urn:nbn:de:0030-drops-191125},
  doi =		{10.4230/LIPIcs.TIME.2023.22},
  annote =	{Keywords: Automata, Planning, Temporal Reasoning}
}
Document
DOI: 10.4230/LIPIcs.TIME.2021.8
Past Matters: Supporting LTL+Past in the BLACK Satisfiability Checker

Authors: Luca Geatti, Nicola Gigante, Angelo Montanari, and Gabriele Venturato

Published in: LIPIcs, Volume 206, 28th International Symposium on Temporal Representation and Reasoning (TIME 2021)

Abstract
LTL+Past is the extension of Linear Temporal Logic (LTL) supporting past temporal operators. The addition of the past does not add expressive power, but does increase the usability of the language both in formal verification and in artificial intelligence, e.g., in the context of multi-agent systems. In this paper, we add the support of past operators to BLACK, a satisfiability checker for LTL based on a SAT encoding of a tree-shaped tableau system. We implement two ways of supporting the past in the tool. The first one is an equisatisfiable translation that removes the past operators, obtaining a future-only formula that can be solved with the original LTL engine. The second one extends the SAT encoding of the underlying tableau to directly support the tableau rules that deal with past operators. We describe both approaches and experimentally compare the two between themselves and with the νXmv model checker, obtaining promising results.
Cite as

Luca Geatti, Nicola Gigante, Angelo Montanari, and Gabriele Venturato. Past Matters: Supporting LTL+Past in the BLACK Satisfiability Checker. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{geatti_et_al:LIPIcs.TIME.2021.8,
  author =	{Geatti, Luca and Gigante, Nicola and Montanari, Angelo and Venturato, Gabriele},
  title =	{{Past Matters: Supporting LTL+Past in the BLACK Satisfiability Checker}},
  booktitle =	{28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
  pages =	{8:1--8:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-206-8},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{206},
  editor =	{Combi, Carlo and Eder, Johann and Reynolds, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.8},
  URN =		{urn:nbn:de:0030-drops-147846},
  doi =		{10.4230/LIPIcs.TIME.2021.8},
  annote =	{Keywords: SAT, LTL, LTL+Past, Tableaux}
}
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