3 Search Results for "Gianola, Alessandro"

Document
Short Paper
DOI: 10.4230/LIPIcs.ITP.2025.37
LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean (Short Paper)

Authors: Eric Vin, Kyle A. Miller, and Daniel J. Fremont

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
We propose LeanLTL, a unifying framework for linear temporal logics in Lean 4. LeanLTL supports reasoning about traces that represent either infinite or finite linear time. The library allows traditional LTL syntax to be combined with arbitrary Lean expressions, making it straightforward to define properties involving numerical or other types. We prove that standard flavors of LTL can be embedded in our framework. The library also provides automation for reasoning about LeanLTL formulas in a way that facilitates using Lean’s existing tactics. Finally, we provide examples illustrating the utility of the library in reasoning about systems that come from applications.
Cite as

Eric Vin, Kyle A. Miller, and Daniel J. Fremont. LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean (Short Paper). In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 37:1-37:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vin_et_al:LIPIcs.ITP.2025.37,
  author =	{Vin, Eric and Miller, Kyle A. and Fremont, Daniel J.},
  title =	{{LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{37:1--37:9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.37},
  URN =		{urn:nbn:de:0030-drops-246356},
  doi =		{10.4230/LIPIcs.ITP.2025.37},
  annote =	{Keywords: Linear Temporal Logic, Interactive Theorem Proving, Lean 4}
}
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
DOI: 10.4230/LIPIcs.CALCO.2017.2
Cospan/Span(Graph): an Algebra for Open, Reconfigurable Automata Networks

Authors: Alessandro Gianola, Stefano Kasangian, and Nicoletta Sabadini

Published in: LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

Abstract
Span(Graph) was introduced by Katis, Sabadini and Walters as a categorical algebra of automata with interfaces, with main operation being communicating-parallel composition. Additional operations provide also a calculus of connectors or wires among components. A system so described has two aspects: an informal network geometry arising from the algebraic expression, and a space of states and transition given by its evaluation in Span(Graph). So, Span(Graph) yields purely compositional, hierarchical descriptions of networks with a fixed topology . The dual algebra Cospan(Graph) allows to describe also the sequential behaviour of systems. Both algebras, of spans and of cospans, are symmetrical monoidal categories with commutative separable algebra structures on the objects. Hence, the combined algebra CospanSpan(Graph) can be interpreted as a general algebra for reconfigurable/hierarchical networks, generalizing the usual Kleene's algebra for classical automata. We present some examples of systems described in this setting.
Cite as

Alessandro Gianola, Stefano Kasangian, and Nicoletta Sabadini. Cospan/Span(Graph): an Algebra for Open, Reconfigurable Automata Networks. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 2:1-2:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{gianola_et_al:LIPIcs.CALCO.2017.2,
  author =	{Gianola, Alessandro and Kasangian, Stefano and Sabadini, Nicoletta},
  title =	{{Cospan/Span(Graph): an Algebra for Open, Reconfigurable Automata Networks}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{2:1--2:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-033-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{72},
  editor =	{Bonchi, Filippo and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.2},
  URN =		{urn:nbn:de:0030-drops-80535},
  doi =		{10.4230/LIPIcs.CALCO.2017.2},
  annote =	{Keywords: Categories, Automata, Composition, Networks}
}
  • Refine by Type
  • 3 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2023
  • 1 2017

  • Refine by Author
  • 2 Gianola, Alessandro
  • 1 Fremont, Daniel J.
  • 1 Geatti, Luca
  • 1 Gigante, Nicola
  • 1 Kasangian, Stefano
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Logic and verification
  • 1 Theory of computation → Modal and temporal logics
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 2 Linear Temporal Logic
  • 1 Automata
  • 1 Categories
  • 1 Composition
  • 1 Interactive Theorem Proving
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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