Luca Geatti

AIJ Journal 2026 Journal Article

An optimal pastification algorithm for LTL[X,F] and LTL[X,G]

• Alessandro Artale
• Luca Geatti
• Nicola Gigante
• Alessio Mansutti
• Andrea Mazzullo
• Angelo Montanari

AAAI Conference 2026 Conference Paper

Automata-less Monitoring via Trace-Checking

• Andrea Brunello
• Luca Geatti
• Angelo Montanari
• Nicola Saccomanno

In runtime verification, monitoring consists of analyzing the current execution of a system and determining, on the basis of the observed finite trace, whether all its possible continuations satisfy or violate a given specification. This is typically done by synthesizing a monitor–often a Deterministic Finite State Automaton (DFA)–from logical specifications expressed in Linear Temporal Logic (LTL) or in its finite-word variant (LTLf). Unfortunately, the size of the resulting DFA may incur a doubly exponential blow-up in the size of the formula. In this paper, we identify some conditions under which monitoring can be done without constructing such a DFA. We build on the notion of intentionally safe and cosafe formulas to show that monitoring of these formulas can be carried out through trace-checking, that is, by directly evaluating them on the current system trace, with a polynomial complexity in the size of both the trace and the formula. In addition, we investigate the complexity of recognizing intentionally safe and cosafe formulas for the safety and cosafety fragments of LTL and LTLf. As for LTLf, we show that all formulas in these fragments are intentionally safe and cosafe, thus removing the need for the check. As for LTL, we prove that the problem is in PSPACE, significantly improving over the EXPSPACE complexity of full LTL.

AAAI Conference 2026 Conference Paper

Do LLMs Really Struggle at NL-FOL Translation? Revealing Their Strengths via a Novel Benchmarking Strategy

• Andrea Brunello
• Luca Geatti
• Michele Mignani
• Angelo Montanari
• Nicola Saccomanno

Due to its expressiveness and unambiguous nature, First-Order Logic (FOL) is a powerful formalism for representing concepts expressed in natural language (NL). This is useful, e.g., for specifying and verifying desired system properties. While translating FOL into human-readable English is relatively straightforward, the inverse problem, converting NL to FOL (NL-FOL translation), has remained a longstanding challenge, for both humans and machines. Although the emergence of Large Language Models (LLMs) promised a breakthrough, recent literature provides contrasting results on their ability to perform NL-FOL translation. In this work, we provide a threefold contribution. First, we critically examine existing datasets and protocols for evaluating NL-FOL translation performance, revealing key limitations that may cause a misrepresentation of LLMs' actual capabilities. Second, to overcome these shortcomings, we propose a novel evaluation protocol explicitly designed to distinguish genuine semantic-level logical understanding from superficial pattern recognition, memorization, and dataset contamination. Third, using this new approach, we show that state-of-the-art, dialogue-oriented LLMs demonstrate strong NL-FOL translation skills and a genuine grasp of sentence-level logic, whereas embedding-centric models perform markedly worse.

AAAI Conference 2025 Conference Paper

First-Order Automata

• Luca Geatti
• Alessandro Gianola
• Nicola Gigante

First-order linear temporal logic (FOLTL) is a flexible and expressive formalism capable of naturally describing complex behaviors and properties. Although the logic is in general highly undecidable, the idea of using it as a specification language for the verification of complex infinite-state systems is appealing. However, a missing piece, which has proved to be an invaluable tool in dealing with other temporal logics, is an automaton model capable of capturing the logic. In this paper we address this issue, by defining and studying such a model, which we call first-order automaton. We define this very general class of automata, and the corresponding notion of regular first-order language (of finite words), showing their closure under most language-theoretic operations. We show how they can capture any FOLTL formula over finite words, over any signature and theory, and provide sufficient conditions for the semi-decidability of their non-emptiness problem. Then, to show the usefulness of the formalism, we prove the decidability of monodic FOLTL, a classic result known in the literature, with a simpler and direct proof.

ECAI Conference 2025 Conference Paper

Interpretable Early Failure Detection via Machine Learning and Trace Checking-Based Monitoring

• Andrea Brunello
• Luca Geatti
• Angelo Montanari
• Nicola Saccomanno

Monitoring is a runtime verification technique that allows one to check whether an ongoing computation of a system (partial trace) satisfies a given formula. It does not need a complete model of the system, but it typically requires the construction of a deterministic automaton doubly exponential in the size of the formula (in the worst case), which limits its practicality. In this paper, we show that, when considering finite, discrete traces, monitoring of pure past (co)safety fragments of Signal Temporal Logic (STL) can be reduced to trace checking, that is, evaluation of a formula over a trace, that can be performed in time polynomial in the size of the formula and the length of the trace. By exploiting such a result, we develop a GPU-accelerated framework for interpretable early failure detection based on vectorized trace checking, that employs genetic programming to learn temporal properties from historical trace data. The framework shows a 2–10% net improvement in key performance metrics compared to the state-of-the-art methods.

TIME Conference 2025 Conference Paper

Safety and Liveness on Finite Words

• Luca Geatti
• Stefano Pessotto
• Stefano Tonetta

The study of safety and liveness is crucial in the context of formal languages on infinite words, providing a fundamental classification of system properties. They have been studied extensively as fragments for regular languages and Linear Temporal Logic (LTL), both from the theoretical and practical point of view, especially in the context of model checking. In contrast, despite the growing interest in Linear Temporal Logic over finite traces (LTLf) as a specification formalism for finite-length executions, the notions of safety and liveness for finite words have remained largely unexplored. In this work, we address this gap by defining the safety and liveness fragments of languages on finite words, mirroring the definition used for infinite words. We show that safety languages are exactly those that are prefix-closed, from which a bounded model property for all safety languages follows. We also provide criteria for determining whether a given language belongs to the safety or liveness fragment and analyze the computational complexity of this classification problems. Moreover, we show that certain LTL formulas classified as safety or liveness over infinite words may not preserve this classification when interpreted over finite words, and ǐceversa. We further establish that the safety-liveness decomposition theorem - asserting that every ω-regular language can be expressed as the intersection of a safety language and a liveness language - also holds in the finite-word setting. Finally, we examine the implications of these results for the model checking problem in LTLf.

TCS Journal 2024 Journal Article

Cascade products and Wheeler automata

• Giovanna D'Agostino
• Luca Geatti
• Davide Martincigh
• Alberto Policriti

AAAI Conference 2024 Conference Paper

Foundations of Reactive Synthesis for Declarative Process Specifications

• Luca Geatti
• Marco Montali
• Andrey Rivkin

Given a specification of Linear-time Temporal Logic interpreted over finite traces (LTLf), the reactive synthesis problem asks to find a finitely-representable, terminating controller that reacts to the uncontrollable actions of an environment in order to enforce a desired system specification. In this paper we study, for the first time, the foundations of reactive synthesis for DECLARE, a well-established declarative, pattern-based business process modelling language grounded in LTLf. We provide a threefold contribution. First, we define a reactive synthesis problem for DECLARE. Second, we show how an arbitrary DECLARE specification can be polynomially encoded into an equivalent pure-past one in LTLf, and exploit this to define an EXPTIME algorithm for DECLARE synthesis. Third, we derive a symbolic version of this algorithm, by introducing a novel translation of pure-past temporal formulas into symbolic deterministic finite automata.

IJCAI Conference 2024 Conference Paper

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

• Andrea Brunello
• Luca Geatti
• Angelo Montanari
• Nicola Saccomanno

Monitoring is a runtime verification technique that can be used to check whether an execution of a system (trace) satisfies or not a given set of properties. Compared to other formal verification techniques, e. g. , model checking, one needs to specify the properties to be monitored, but a complete model of the system is no longer necessary. First, we introduce the pure past fragment of Signal Temporal Logic (ppSTL), and we use it to define the monitorable safety (G(ppSTL)) and cosafety (F(ppSTL)) fragments of STL, which properly extend the commonly-used bounded-future fragment. Then, we devise a multi-objective genetic programming algorithm to automatically extend the set of properties to monitor on the basis of the history of failure traces collected over time. The framework resulting from the integration of the monitor and the learning algorithm is then experimentally validated on various public datasets. The outcomes of the experimentation confirm the effectiveness of the proposed solution.

GandALF Workshop 2024 Workshop Paper

Synthesis of Timeline-Based Planning Strategies Avoiding Determinization

• Renato Acampora
• Dario Della Monica
• Luca Geatti
• Nicola Gigante
• Angelo Montanari
• Pietro Sala

Qualitative timeline-based planning models domains as sets of independent, but interacting, components whose behaviors over time, the timelines, are governed by sets of qualitative temporal constraints (ordering relations), called synchronization rules. Its plan-existence problem has been shown to be PSPACE-complete; in particular, PSPACE-membership has been proved via reduction to the nonemptiness problem for nondeterministic finite automata. However, nondeterministic automata cannot be directly used to synthesize planning strategies as a costly determinization step is needed. In this paper, we identify a large fragment of qualitative timeline-based planning whose plan-existence problem can be directly mapped into the nonemptiness problem of deterministic finite automata, which can then be exploited to synthesize strategies. In addition, we identify a maximal subset of Allen's relations that fits into such a deterministic fragment.

KR Conference 2023 Conference Paper

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

• Alessandro Artale
• Luca Geatti
• Nicola Gigante
• Andrea Mazzullo
• Angelo Montanari

Confronting the past can be hard. This is true even in Linear Temporal Logic (LTL), interpreted on either infinite or finite traces, when faced with the problem of transforming a temporally future formula into an equivalent one that contains past temporal modalities only. To our knowledge, the best among the available pastification procedures for full LTL, as well as for expressive enough fragments of it (that is, containing at least one temporal modality other than tomorrow), are triply exponential in the size of the input. In this paper, we focus on the fragment of LTL that features the tomorrow and eventually modalities, and provide a singly exponential pastification algorithm for it. The transformation is based on a normalisation procedure that requires a non-trivial complexity analysis, and on the subsequent generation of a pure past formula from suitably-defined dependency tree structures. Moreover, leveraging its purely syntactic nature, we present an implementation of our procedure in a temporal satisfiability checking tool that deals with both future and past modalities.

AAAI Conference 2023 Conference Paper

Complexity of Safety and coSafety Fragments of Linear Temporal Logic

• Alessandro Artale
• Luca Geatti
• Nicola Gigante
• Andrea Mazzullo
• Angelo Montanari

Linear Temporal Logic (LTL) is the de-facto standard temporal logic for system specification, whose foundational properties have been studied for over five decades. Safety and cosafety properties of LTL define notable fragments of LTL, where a prefix of a trace suffices to establish whether a formula is true or not over that trace. In this paper, we study the complexity of the problems of satisfiability, validity, and realizability over infinite and finite traces for the safety and cosafety fragments of LTL. As for satisfiability and validity over infinite traces, we prove that the majority of the fragments have the same complexity as full LTL, that is, they are PSPACE-complete. The picture is radically different for realizability: we find fragments with the same expressive power whose complexity varies from 2EXPTIME-complete (as full LTL) to EXPTIME-complete. Notably, for all cosafety fragments, the complexity of the three problems does not change passing from infinite to finite traces, while for all safety fragments the complexity of satisfiability (resp., realizability) over finite traces drops to NP-complete (resp., Πᴾ₂- complete).

ECAI Conference 2023 Conference Paper

Decidable Fragments of LTL f Modulo Theories

• Luca Geatti
• Alessandro Gianola
• Nicola Gigante
• Sarah Winkler

We study Linear Temporal Logic Modulo Theories over Finite Traces (LTLMTf), a recently introduced extension of LTL over finite traces (LTLf) where propositions are replaced by first-order formulas and where first-order variables referring to different time points can be compared. In general, LTLMTf was shown to be semi-decidable for any decidable first-order theory (e. g. , linear arithmetics), with a tableau-based semi-decision procedure. In this paper we present a sound and complete pruning rule for the LTLMTf tableau. We show that for any LTLMTf formula that satisfies an abstract, semantic condition, that we call finite memory, the tableau augmented with the new rule is also guaranteed to terminate. Last but not least, this technique allows us to establish novel decidability results for the satisfiability of several fragments of LTLMTf, as well as to give new decidability proofs for classes that are already known.

TIME Conference 2023 Conference Paper

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

• Alessandro Artale
• Luca Geatti
• Nicola Gigante
• Andrea Mazzullo
• Angelo Montanari

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.

TIME Conference 2023 Conference Paper

Qualitative past Timeline-Based Games (Extended Abstract)

• Renato Acampora
• Luca Geatti
• Nicola Gigante
• Angelo Montanari

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.

TIME Conference 2023 Conference Paper

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

• Luca Geatti
• Alessandro Gianola
• Nicola Gigante

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.

GandALF Workshop 2022 Workshop Paper

Controller Synthesis for Timeline-based Games

• Renato Acampora
• Luca Geatti
• Nicola Gigante
• Angelo Montanari
• Valentino Picotti

In the timeline-based approach to planning, originally born in the space sector, the evolution over time of a set of state variables (the timelines) is governed by a set of temporal constraints. Traditional timeline-based planning systems excel at the integration of planning with execution by handling temporal uncertainty. In order to handle general nondeterminism as well, the concept of timeline-based games has been recently introduced. It has been proved that finding whether a winning strategy exists for such games is 2EXPTIME-complete. However, a concrete approach to synthesize controllers implementing such strategies is missing. This paper fills this gap, outlining an approach to controller synthesis for timeline-based games.

IJCAI Conference 2022 Conference Paper

Linear Temporal Logic Modulo Theories over Finite Traces

• Luca Geatti
• Alessandro Gianola
• Nicola Gigante

This paper studies Linear Temporal Logic over Finite Traces (LTLf) where proposition letters are replaced with first-order formulas interpreted over arbitrary theories, in the spirit of Satisfiability Modulo Theories. The resulting logic, called LTLf Modulo Theories (LTLfMT), is semi-decidable. Nevertheless, its high expressiveness comes useful in a number of use cases, such as model-checking of data-aware processes and data-aware planning. Despite the general undecidability of these problems, being able to solve satisfiable instances is a compromise worth studying. After motivating and describing such use cases, we provide a sound and complete semi-decision procedure for LTLfMT based on the SMT encoding of a one-pass tree-shaped tableau system. The algorithm is implemented in the BLACK satisfiability checking tool, and an experimental evaluation shows the feasibility of the approach on novel benchmarks.

GandALF Workshop 2021 Workshop Paper

Expressiveness of Extended Bounded Response LTL

• Alessandro Cimatti
• Luca Geatti
• Nicola Gigante
• Angelo Montanari
• Stefano Tonetta

Extended Bounded Response LTL with Past (LTLEBR+P) is a safety fragment of Linear Temporal Logic with Past (LTL+P) that has been recently introduced in the context of reactive synthesis. The strength of LTLEBR+P is a fully symbolic compilation of formulas into symbolic deterministic automata. Its syntax is organized in four levels. The first three levels feature (a particular combination of) future temporal modalities, the last one admits only past temporal operators. At the base of such a structuring there are algorithmic motivations: each level corresponds to a step of the algorithm for the automaton construction. The complex syntax of LTLEBR+P made it difficult to precisely characterize its expressive power, and to compare it with other LTL+P safety fragments. In this paper, we first prove that LTLEBR+P is expressively complete with respect to the safety fragment of LTL+P, that is, any safety language definable in LTL+P can be formalized in LTLEBR+P, and vice versa. From this, it follows that LTLEBR+P and Safety-LTL are expressively equivalent. Then, we show that past modalities play an essential role in LTLEBR+P: we prove that the future fragment of LTLEBR+P is strictly less expressive than full LTLEBR+P.

TIME Conference 2021 Conference Paper

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

• Luca Geatti
• Nicola Gigante
• Angelo Montanari
• Gabriele Venturato

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.

GandALF Workshop 2018 Workshop Paper

One-Pass and Tree-Shaped Tableau Systems for TPTL and TPTLb+Past

• Luca Geatti
• Nicola Gigante
• Angelo Montanari
• Mark Reynolds

In this paper, we propose a novel one-pass and tree-shaped tableau method for Timed Propositional Temporal Logic and for a bounded variant of its extension with past operators. Timed Propositional Temporal Logic (TPTL) is a real-time temporal logic, with an EXPSPACE-complete satisfiability problem, which has been successfully applied to the verification of real-time systems. In contrast to LTL, adding past operators to TPTL makes the satisfiability problem for the resulting logic (TPTL+P) non-elementary. In this paper, we devise a one-pass and tree-shaped tableau for both TPTL and bounded TPTL+P (TPTLb+P), a syntactic restriction introduced to encode timeline-based planning problems, which recovers the EXPSPACE-complete complexity. The tableau systems for TPTL and TPTLb+P are presented in a unified way, being very similar to each other, providing a common skeleton that is then specialised to each logic. In doing that, we characterise the semantics of TPTLb+P in terms of a purely syntactic fragment of TPTL+P, giving a translation that embeds the former into the latter. Soundness and completeness of the system are proved fully. In particular, we give a greatly simplified model-theoretic completeness proof, which sidesteps the complex combinatorial argument used by known proofs for the one-pass and tree-shaped tableau systems for LTL and LTL+P.