Author name cluster

Alessandro Gianola

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

10 papers

2 author rows

AAAI Conference 2026 Conference Paper

Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning

Pierriccardo Olivieri
Fausto Lasca
Alessandro Gianola
Matteo Papini

In this work, we propose a novel framework for the logical specification of non-Markovian rewards in Markov Decision Processes (MDPs) with large state spaces. Our approach leverages Linear Temporal Logic Modulo Theories over finite traces (LTLfMT), a more expressive extension of classical temporal logic in which predicates are first-order formulas of arbitrary first-order theories rather than simple Boolean variables. This enhanced expressiveness enables the specification of complex tasks over unstructured and heterogeneous data domains, promoting a unified and reusable framework that eliminates the need for manual predicate encoding. However, the increased expressive power of LTLfMT introduces additional theoretical and computational challenges compared to standard LTLf specifications. We address these challenges from a theoretical standpoint, identifying a fragment of LTLfMT that is tractable but sufficiently expressive for reward specification in an infinite-state-space context. From a practical perspective, we introduce a method based on reward machines and Hindsight Experience Replay (HER) to translate first-order logic specifications and address reward sparsity. We evaluate this approach to a continuous-control setting using Non-Linear Arithmetic Theory, showing that it enables natural specification of complex tasks. Experimental results show how a tailored implementation of HER is fundamental in solving tasks with complex goals.

PDF Details DOI

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.

PDF Details DOI

AAAI Conference 2024 Conference Paper

Linear-Time Verification of Data-Aware Processes Modulo Theories via Covers and Automata

Alessandro Gianola
Marco Montali
Sarah Winkler

The need to model and analyse dynamic systems operating over complex data is ubiquitous in AI and neighboring areas, in particular business process management. Analysing such data-aware systems is a notoriously difficult problem, as they are intrinsically infinite-state. Existing approaches work for specific datatypes, and/or limit themselves to the verification of safety properties. In this paper, we lift both such limitations, studying for the first time linear-time verification for so-called data-aware processes modulo theories (DMTs), from the foundational and practical point of view. The DMT model is very general, as it supports processes operating over variables that can store arbitrary types of data, ranging over infinite domains and equipped with domain-specific predicates. Specifically, we provide four contributions. First, we devise a semi-decision procedure for linear-time verification of DMTs, which works for a very large class of datatypes obeying to mild model-theoretic assumptions. The procedure relies on a unique combination of automata-theoretic and cover computation techniques to respectively deal with linear-time properties and datatypes. Second, we identify an abstract, semantic property that guarantees the existence of a faithful finite-state abstraction of the original system, and show that our method becomes a decision procedure in this case. Third, we identify concrete, checkable classes of systems that satisfy this property, generalising several results in the literature. Finally, we present an implementation and an experimental evaluation over a benchmark of real-world data-aware business processes.

PDF Details DOI

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.

Details

EAAI Journal 2023 Journal Article

Multi-perspective conformance checking of uncertain process traces: An SMT-based approach

Paolo Felli
Alessandro Gianola
Marco Montali
Andrey Rivkin
Sarah Winkler

Conformance checking, one of the central tasks in process mining, compares the expected behavior described by a reference process model to the actual behavior recorded in an event log, with the goal of detecting deviations. Traditionally, it is assumed that the log provides a faithful and complete digital footprint of reality. However, assuming perfect logs is often unrealistic: real-life logs typically suffer from data quality issues, exposing uncertainty in their events, timestamps, and data attributes. We attack this problem by introducing a comprehensive framework for multi-perspective conformance checking dealing with uncertainty along three perspectives: control-flow, time, and data. From the modeling point of view, we consider process models formalized as Petri nets operating over data variables, and event logs presenting uncertainty at the event- and attribute-level. We cast conformance checking as an alignment problem, extending the traditional notions of alignment and cost function to deal with uncertainty along the three aforementioned perspectives. From the operational point of view, we show how (optimal) alignments can be computed through well-established automated reasoning techniques from Satisfiability Modulo Theories (SMT). Specifically, we show how previous results on data-aware SMT-based conformance checking can be lifted to this more sophisticated setting, obtaining a flexible framework that can seamlessly handle different variants of the problem. We formally prove correctness of our approach and implement it in the conformance checker cocomot. Finally, we perform a thorough experimental evaluation on synthetic and real-life logs, demonstrating the overall promising performance of our framework.

Details DOI

IJCAI Conference 2023 Conference Paper

Safety Verification and Universal Invariants for Relational Action Bases

Silvio Ghilardi
Alessandro Gianola
Marco Montali
Andrey Rivkin

Modeling and verification of dynamic systems operating over a relational representation of states are increasingly investigated problems in AI, Business Process Management and Database Theory. To make these systems amenable to verification, the amount of information stored in each state needs to be bounded, or restrictions are imposed on the preconditions and effects of actions. We lift these restrictions by introducing the framework of Relational Action Bases (RABs), which generalizes existing frameworks and in which unbounded relational states are evolved through actions that can (1) quantify both existentially and universally over the data, and (2) use arithmetic constraints. We then study parameterized safety of RABs via (approximated) SMT-based backward search, singling out essential meta-properties of the resulting procedure, and showing how it can be realized by an off-the-shelf combination of existing verification modules of the state-of-the-art MCMT model checker. We demonstrate the effectiveness of this approach on a benchmark of data-aware business processes. Finally, we show how universal invariants can be exploited to make this procedure fully correct.

PDF Details DOI

AAAI Conference 2023 Conference Paper

SMT Safety Verification of Ontology-Based Processes

Diego Calvanese
Alessandro Gianola
Andrea Mazzullo
Marco Montali

In the context of verification of data-aware processes, a formal approach based on satisfiability modulo theories (SMT) has been considered to verify parameterised safety properties. This approach requires a combination of model-theoretic notions and algorithmic techniques based on backward reachability. We introduce here Ontology-Based Processes, which are a variant of one of the most investigated models in this spectrum, namely simple artifact systems (SASs), where, instead of managing a database, we operate over a description logic (DL) ontology. We prove that when the DL is expressed in (a slight extension of) RDFS, it enjoys suitable model-theoretic properties, and that by relying on such DL we can define Ontology-Based Processes to which backward reachability can still be applied. Relying on these results we are able to show that in this novel setting, verification of safety properties is decidable in PSPACE.

PDF Details DOI

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.

Details

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.

PDF Details DOI

AAAI Conference 2021 Conference Paper

SMT-based Safety Checking of Parameterized Multi-Agent Systems

Paolo Felli
Alessandro Gianola
Marco Montali

We study the problem of verifying whether a given parameterized multi-agent system (PMAS) is safe, namely whether none of its possible executions can lead to bad states. These are captured by a state formula existentially quantifying over agents. As the MAS is parameterized, it only describes the finite set of possible agent templates, while the actual number of concrete agent instances that will be present at runtime, for each template, is unbounded and cannot be foreseen. We solve this problem via infinite-state model checking based on satisfiability modulo theories (SMT), relying on the theory of array-based systems. We formally characterize the soundness, completeness and termination guarantees of our approach under specific assumptions. This gives us a technique that is implementable on top of third-party, SMT-based model checkers. Finally, we discuss how this approach lends itself to richer parameterized and data-aware MAS settings beyond the state-of-the-art solutions in the literature.

PDF Details