Search Results

Documents authored by Geatti, Luca

Document
DOI: 10.4230/LIPIcs.STACS.2025.20
On Cascades of Reset Automata

Authors: Roberto Borelli, Luca Geatti, Marco Montali, and Angelo Montanari

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract
The Krohn-Rhodes decomposition theorem is a pivotal result in automata theory. It introduces the concept of cascade product, where two semiautomata, that is, automata devoid of initial and final states, are combined in a feed-forward fashion. The theorem states that any semiautomaton can be decomposed into a sequence of permutation-reset semiautomata. For the counter-free case, this decomposition consists entirely of reset components with two states each. This decomposition has significantly impacted recent research in various areas of computer science, including the identification of a class of transformer encoders equivalent to star-free languages and the conversion of Linear Temporal Logic formulas into past-only expressions (pastification). The paper revisits the cascade product in the context of reset automata, thus considering each component of the cascade as a language acceptor. First, we give regular expression counterparts of cascades of reset automata. We then establish several expressiveness results, identifying hierarchies of languages based on the restriction of the height (number of components) of the cascade or of the number of states in each level. We also show that any cascade of reset automata can be transformed, with a quadratic increase in height, into a cascade that only includes two-state components. Finally, we show that some fundamental operations on cascades, like intersection, union, negation, and concatenation with a symbol to the left, can be directly and efficiently computed by adding a two-state component.
Cite as

Roberto Borelli, Luca Geatti, Marco Montali, and Angelo Montanari. On Cascades of Reset Automata. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 20:1-20:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{borelli_et_al:LIPIcs.STACS.2025.20,
  author =	{Borelli, Roberto and Geatti, Luca and Montali, Marco and Montanari, Angelo},
  title =	{{On Cascades of Reset Automata}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{20:1--20:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.20},
  URN =		{urn:nbn:de:0030-drops-228453},
  doi =		{10.4230/LIPIcs.STACS.2025.20},
  annote =	{Keywords: Automata, Cascade products, Regular expressions, Krohn-Rhodes theory}
}
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