Luca Geatti

Stefano Pessotto

Stefano Tonetta

Proceedings of the 32nd International Symposium on Temporal Representation and Reasoning, 2025

On Cascades of Reset Automata.

[BibT_eX]

[DOI]

Proceedings of the 42nd International Symposium on Theoretical Aspects of Computer Science, 2025

First-Order Automata.

[BibT_eX]

[DOI]

Proceedings of the AAAI-25, Sponsored by the Association for the Advancement of Artificial Intelligence, February 25, 2025

2024

Extended bounded response LTL: a new safety fragment for efficient reactive synthesis.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., December, 2024

SAT Meets Tableaux for Linear Temporal Logic Satisfiability.

[BibT_eX]

[DOI]

J. Autom. Reason., June, 2024

Cascade products and Wheeler automata.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2024

Controller Synthesis for Timeline-based Games.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2024

Synthesis of Timeline-Based Planning Strategies Avoiding Determinization.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Fifteenth International Symposium on Games, 2024

A General Automata Model for First-Order Temporal Logics (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2024

Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems (extended version).

[BibT_eX]

[DOI]

Alessio Mansutti

CoRR, 2024

Evaluating LLMs Capabilities at Natural Language to Logic Translation: A Preliminary Investigation.

[BibT_eX]

[DOI]

Proceedings of the Short Paper Proceedings of the 6th International Workshop on Artificial Intelligence and Formal Verification, 2024

Learning What to Monitor: Using Machine Learning to Improve past STL Monitoring.

[BibT_eX]

[DOI]

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, 2024

Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems.

[BibT_eX]

[DOI]

Alessio Mansutti

Proceedings of the Foundations of Software Science and Computation Structures, 2024

SMT-Based Symbolic Model-Checking for Operator Precedence Languages.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 36th International Conference, 2024

Foundations of Reactive Synthesis for Declarative Process Specifications.

[BibT_eX]

[DOI]

Marco Montali

Andrey Rivkin

Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence, 2024

2023

A first-order logic characterization of safety and co-safety languages.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2023

GR(1) is equivalent to R(1).

[BibT_eX]

[DOI]

Inf. Process. Lett., 2023

Decidable Fragments of LTLf Modulo Theories (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2023

Torwards Infinite-State Verification and Planning with Linear Temporal Logic Modulo Theories (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the 30th International Symposium on Temporal Representation and Reasoning, 2023

LTL over Finite Words Can Be Exponentially More Succinct Than Pure-Past LTL, and vice versa.

[BibT_eX]

[DOI]

Proceedings of the 30th International Symposium on Temporal Representation and Reasoning, 2023

Qualitative past Timeline-Based Games (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the 30th International Symposium on Temporal Representation and Reasoning, 2023

Towards Machine Learning Enhanced LTL Monitoring.

[BibT_eX]

[DOI]

Nicola Saccomanno

Proceedings of the Short Paper Proceedings of the 5th Workshop on Artificial Intelligence and Formal Verification, 2023

A Landscape of First-Order Linear Temporal Logics in Infinite-State Verification and Temporal Ontologies.

[BibT_eX]

[DOI]

Proceedings of the Short Paper Proceedings of the 5th Workshop on Artificial Intelligence and Formal Verification, 2023

A Singly Exponential Transformation of LTL[X, F] into Pure Past LTL.

[BibT_eX]

[DOI]

Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning, 2023

A Linear-size Cascade Decomposition for Wheeler Automata.

[BibT_eX]

[DOI]

Proceedings of the 24th Italian Conference on Theoretical Computer Science, 2023

Decidable Fragments of LTL<sub>f</sub> Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the ECAI 2023 - 26th European Conference on Artificial Intelligence, September 30 - October 4, 2023, Kraków, Poland, 2023

Foundations of Collaborative sfDECLARE.

[BibT_eX]

[DOI]

Marco Montali

Andrey Rivkin

Proceedings of the Business Process Management Forum, 2023

Complexity of Safety and coSafety Fragments of Linear Temporal Logic.

[BibT_eX]

[DOI]

Proceedings of the Thirty-Seventh AAAI Conference on Artificial Intelligence, 2023

2022

Reactive Synthesis for DECLARE via symbolic automata.

[BibT_eX]

[DOI]

Marco Montali

Andrey Rivkin

CoRR, 2022

Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2022

Linear Temporal Logic Modulo Theories over Finite Traces.

[BibT_eX]

[DOI]

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, 2022

A first-order logic characterisation of safety and co-safety languages.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2022

2021

One-pass and tree-shaped tableau systems for TPTL and TPTL<sub>b</sub>+Past.

[BibT_eX]

[DOI]

Inf. Comput., 2021

Expressiveness of Extended Bounded Response LTL.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 12th International Symposium on Games, 2021

Past Matters: Supporting LTL+Past in the BLACK Satisfiability Checker.

[BibT_eX]

[DOI]

Proceedings of the 28th International Symposium on Temporal Representation and Reasoning, 2021

Fairness, Assumptions, and Guarantees for Extended Bounded Response LTL+P Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods - 19th International Conference, 2021

BLACK: A Fast, Flexible and Reliable LTL Satisfiability Checker.

[BibT_eX]

[DOI]

Proceedings of the 3rd Workshop on Artificial Intelligence and Formal Verification, 2021

2020

Safe Decomposition of Startup Requirements: Verification and Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

Reactive Synthesis from Extended Bounded Response LTL Specifications.

[BibT_eX]

[DOI]

Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

2019

A SAT-Based Encoding of the One-Pass and Tree-Shaped Tableau System for LTL.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2019

An Abstract Distributed Middleware for Transactions over Heterogeneous Stores.

[BibT_eX]

[DOI]