1 Search Results for "Venturato, Gabriele"

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-dev.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}
}
  • Refine by Author
  • 1 Geatti, Luca
  • 1 Gigante, Nicola
  • 1 Montanari, Angelo
  • 1 Venturato, Gabriele

  • Refine by Classification
  • 1 Theory of computation → Modal and temporal logics

  • Refine by Keyword
  • 1 LTL
  • 1 LTL+Past
  • 1 SAT
  • 1 Tableaux

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2021

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 Imprint Privacy Contact