Author name cluster

Marco Roveri

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.

21 papers

2 author rows

AILAW Journal 2025 Journal Article

The compliance gap in data supply chains: contract specification languages and smart contracts as compliance technologies

Pablo Marcello Baquero
David Restrepo Amariles
Daniel Amyot
Amal Ahmed Anda
Mustafa Bayirli
Luigi Logrippo
Alberto Lopes
John Mylopoulos

Abstract This paper investigates the use of Contract Specification Languages (CSLs), smart contracts, and their associated software methods and tools for formally specifying, verifying, and monitoring contracts, as a means to improve compliance with data protection laws, by harnessing the back end of data supply chains. The privacy literature has focused predominantly on B2C relationships (front end data processing) to assess corporate compliance with data protection laws and has explored the use of technologies primarily as a means to empower data subjects vis-à-vis data processors. This article shifts the perspective. First, it shows that the effective implementation of data subjects’ rights hinges upon the capacity of data processors to monitor compliance in back-end processing, i. e. , the data supply chain. Second, it spells out the way CSLs and smart contracts can contribute to bridge the compliance gap in the data supply chain, which currently hinders data controllers from effectively monitoring the flow and use of data documents and practices across the networks of subcontractors. Indeed, while data is processed in an iterative and dynamic manner through a wide variety of means by actors within and across companies in the supply chain (e. g. , controller, processors, and sub-processors), the legal instruments used to ensure compliance are dispersed, static, convoluted and legalistic, ultimately lacking the capability to operationalize data protection across different management levels (legal, technical, business, etc.). This paper proposes methods for specifying and controlling obligations related to data processing and distributions by using CSLs and smart contracts, and the contribution these methods can make for monitoring compliance in the data supply chain. It briefly introduces the Symboleo CSL for the formal specification of contracts. It then offers a concrete case study testing the properties of the Symboleo in a dataset composed of contractual documents used in the data supply chain of a network of IT companies. The paper concludes with a discussion of the challenges laying ahead to narrow the compliance gap and highlights how the proposed methods can evolve to become effective compliance tools in data protection.

Details DOI

JAIR Journal 2024 Journal Article

Computing Unsatisfiable Cores for LTLf Specifications

Marco Roveri
Claudio Di Ciccio
Chiara Di Francescomarino
Chiara Ghidini

Linear-time temporal logic on finite traces (LTLf) is rapidly becoming a de-facto standard to produce specifications in many application domains (including planning, business process management, run-time monitoring, and reactive synthesis). Several studies have challenged the satisfiability problem thus far. In this paper, we focus instead on unsatisfiable LTLf specifications, with the objective of extracting the subset of formulae that cause inconsistencies within them, i.e., the unsatisfiable cores. We provide four algorithms to this end, which leverage the adaptation of a range of state-of-the-art algorithms to LTLf satisfiability checking. We implement those algorithms extending the respective implementations and carry out an experimental evaluation on a set of reference benchmarks, restricting to the unsatisfiable specifications. The results put in evidence that the different algorithms and tools exhibit complementary features determining their efficiency and efficacy. Indeed, our findings suggest exploring different strategies and algorithmic solutions for the extraction of unsatisfiable cores from LTLf specifications, thus confirming the challenging and multi-faceted nature of this problem.

PDF Details DOI

ICRA Conference 2024 Conference Paper

When Prolog Meets Generative Models: a New Approach for Managing Knowledge and Planning in Robotic Applications

Enrico Saccon
Ahmet Tikna
Davide De Martini
Edoardo Lamon
Luigi Palopoli 0002
Marco Roveri

In this paper, we propose a robot oriented knowledge representation system based on the use of the Prolog language. Our framework hinges on a special organisation of Knowledge Base (KB) that enables: 1) its efficient population from natural language texts using semi-automated procedures based on Large Language Models (LLMs); 2) the seamless generation of temporal parallel plans for multi-robot systems through a sequence of transformations; 3) the automated translation of the plan into an executable formalism. The framework is supported by a set of open source tools and its functionality is shown with a realistic application.

Details

IJCAI Conference 2022 Conference Paper

Real-Time BDI Agents: A Model and Its Implementation

Andrea Traldi
Francesco Bruschetti
Marco Robol
Marco Roveri
Paolo Giorgini

The BDI model proved to be effective for the developing of applications requiring high-levels of autonomy and to deal with the complexity and unpredictability of real-world scenarios. The model, however, has significant limitations in reacting and handling contingencies within the given real-time constraints. Without an explicit representation of time, existing real-time BDI implementations overlook the temporal implications during the agent’s decision process that may result in delays or unresponsiveness of the system when it gets overloaded. In this paper, we redefine the BDI agent control loop inspired by traditional and well establish algorithms for real-time systems to ensure a proper reaction of agents and their effective application in typical real-time domains. Our model proposes an effective real-time management of goals, plans, and actions with respect to time constraints and resources availability. We propose an implementation of the model for a resource-collection video-game and we validate the approach against a set of significant scenarios.

PDF Details DOI

SoCS Conference 2022 Conference Paper

Urban Traffic Control via Planning with Global State Constraints (Extended Abstract)

Franc Ivankovic
Mauro Vallati
Lukás Chrpa
Marco Roveri

Planning with global state constraints is an extension of classical planning such that some properties of each state are derived via a set of rules common to all states. This approach is important for the application of planning techniques in manipulating cyber-physical systems, and has been shown to be effective in practice. Urban Traffic Control (UTC) deals with the control and management of traffic in urban regions, and includes the optimisation of traffic signals configuration to minimise traffic congestion and travel delays. In this paper, we briefly introduce how to cast the UTC problem into the formalism of planning with global state constraints, and we perform a preliminary experimental evaluation considering significant scenarios taken from the literature, and a new one based on real-world data. The results show that the approach is feasible, and the quality of generated solutions has been confirmed in simulation using existing symbolic models.

Details

TIST Journal 2021 Journal Article

A Comprehensive Approach to On-board Autonomy Verification and Validation

Marco Bozzano
Alessandro Cimatti
Marco Roveri

Deep space missions are characterized by severely constrained communication links. To meet the needs of future missions and increase their scientific return, future space systems will require an increased level of autonomy on-board. In this work, we propose a comprehensive approach to on-board autonomy. We rely on model-based reasoning, and we consider many important (on-line and off-line) reasoning capabilities such as plan generation, validation, execution and monitoring, runtime diagnosis, and fault detection, identification, and recovery. The controlled platform is represented symbolically, and the reasoning capabilities are seen as symbolic manipulation of such formal model. We have developed a prototype of our framework, and we have integrated it within an on-board Autonomous Reasoning Engine. Finally, we have evaluated our approach on three case-studies inspired by real-world projects and characterized it in terms of reliability, availability, and performance.

Details DOI

I&C Journal 2020 Journal Article

SMT-based satisfiability of first-order LTL with event freezing functions and metric operators

Alessandro Cimatti
Alberto Griggio
Enrico Magnago
Marco Roveri
Stefano Tonetta

In this paper, we propose to extend First-Order Linear-time Temporal Logic with Past adding two operators “at next” and “at last”, which take in input a term and a formula and return the value of the term at the next state in the future or last state in the past in which the formula holds. The new logic, named LTL-EF, can be interpreted with different models of time (including discrete, dense, and super-dense time) and with different first-order theories (à la Satisfiability Modulo Theories (SMT)). We show that the “at next” and “at last” can encode (first-order) MTL 0, ∞ with counting. We provide rewriting procedures to reduce the satisfiability problem to the discrete-time case (to leverage on the mature state-of-the-art corresponding verification techniques) and to remove the extra functional symbols. We implemented these techniques in the nuXmv model checker enabling the analysis of LTL-EF and MTL 0, ∞ based on SMT-based model checking. We show the feasibility of the approach experimenting with several non-trivial valid and satisfiable formulas.

Details DOI

SAT Conference 2018 Conference Paper

Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization

Alessandro Cimatti
Alberto Griggio
Ahmed Irfan
Marco Roveri
Roberto Sebastiani

Abstract Incremental linearization is a conceptually simple, yet effective, technique that we have recently proposed for solving SMT problems over nonlinear real arithmetic constraints. In this paper, we show how the same approach can be applied successfully also to the harder case of nonlinear integer arithmetic problems. We describe in detail our implementation of the basic ideas inside the MathSAT SMT solver, and evaluate its effectiveness with an extensive experimental analysis over all nonlinear integer benchmarks in SMT-LIB. Our results show that MathSAT is very competitive with (and often outperforms) state-of-the-art SMT solvers based on alternative techniques.

Details

AIJ Journal 2018 Journal Article

Strong temporal planning with uncontrollable durations

Alessandro Cimatti
Minh Do
Andrea Micheli
Marco Roveri
David E. Smith

Planning in real world domains often involves modeling and reasoning about the duration of actions. Temporal planning allows such modeling and reasoning by looking for plans that specify start and end time points for each action. In many practical cases, however, the duration of actions may be uncertain and not under the full control of the executor. For example, a navigation task may take more or less time, depending on external conditions such as terrain or weather. In this paper, we tackle the problem of strong temporal planning with uncontrollable action durations (STPUD). For actions with uncontrollable durations, the planner is only allowed to choose the start of the actions, while the end is chosen, within known bounds, by the environment. A solution plan must be robust with respect to all uncontrollable action durations, and must achieve the goal on all executions, despite the choices of the environment. We propose two complementary techniques. First, we discuss a dedicated planning method, that generalizes the state-space temporal planning framework, leveraging SMT-based techniques for temporal networks under uncertainty. Second, we present a compilation-based method, that reduces any STPUD problem to an ordinary temporal planning problem. Moreover, we investigate a set of sufficient conditions to simplify domains by removing some of the uncontrollability. We implemented both our approaches, and we experimentally evaluated our techniques on a large number of instances. Our results demonstrate the practical applicability of the two techniques, which show complementary behavior.

Details DOI

AAAI Conference 2017 Conference Paper

Validating Domains and Plans for Temporal Planning via Encoding into Infinite-State Linear Temporal Logic

Alessandro Cimatti
Andrea Micheli
Marco Roveri

Temporal planning is an active research area of Artiﬁcial Intelligence because of its many applications ranging from robotics to logistics and beyond. Traditionally, authors focused on the automatic synthesis of plans given a formal representation of the domain and of the problem. However, the effectiveness of such techniques is limited by the complexity of the modeling phase: it is hard to produce a correct model for the planning problem at hand. In this paper, we present a technique to simplify the creation of correct models by leveraging formal-veriﬁcation tools for automatic validation. We start by using the ANML language, a very expressive language for temporal planning problems that has been recently presented. We chose ANML because of its usability and readability. Then, we present a soundand-complete, formal encoding of the language into Linear Temporal Logic over predicates with inﬁnite-state variables. Thanks to this reduction, we enable the formal veriﬁcation of several relevant properties over the planning problem, providing useful feedback to the modeler.

PDF Details

AAAI Conference 2016 Conference Paper

Dynamic Controllability of Disjunctive Temporal Networks: Validation and Synthesis of Executable Strategies

Alessandro Cimatti
Andrea Micheli
Marco Roveri

The Temporal Network with Uncertainty (TNU) modeling framework is used to represent temporal knowledge in presence of qualitative temporal uncertainty. Dynamic Controllability (DC) is the problem of deciding the existence of a strategy for scheduling the controllable time points of the network observing past happenings only. In this paper, we address the DC problem for a very general class of TNU, namely Disjunctive Temporal Network with Uncertainty. We make the following contributions. First, we deﬁne strategies in the form of an executable language; second, we propose the ﬁrst decision procedure to check whether a given strategy is a solution for the DC problem; third we present an efﬁcient algorithm for strategy synthesis based on techniques derived from Timed Games and Satisﬁability Modulo Theory. The experimental evaluation shows that the approach is superior to the state-of-the-art.

PDF Details

AIJ Journal 2015 Journal Article

An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty

Alessandro Cimatti
Andrea Micheli
Marco Roveri

The framework of temporal problems with uncertainty (TPU) is useful to express temporal constraints over a set of activities subject to uncertain (and uncontrollable) duration. In this work, we focus on the most general class of TPU, namely disjunctive TPU (DTPU), and consider the case of weak controllability, that allows one to model problems arising in practical scenarios (e. g. on-line scheduling). We first tackle the decision problem, i. e. whether there exists a schedule of the activities that, depending on the uncertainty, satisfies all the constraints. We propose a logical approach, based on the reduction to a problem of Satisfiability Modulo Theories (SMT), in the theory of Linear Real Arithmetic with Quantifiers. This results in the first implemented solver for weak controllability of DTPUs. Then, we tackle the problem of synthesizing control strategies for scheduling the activities. We focus on strategies that are amenable for efficient execution. We prove that linear strategies are not always sufficient, even in the sub-case of simple TPU (STPU), while piecewise-linear strategies, that are multiple conditionally-applied linear strategies, are always sufficient. We present several algorithms for the synthesis of linear and piecewise-linear strategies, in case of STPU and of DTPU. All the algorithms are implemented on top of SMT solvers. We provide experimental evidence of the scalability of the proposed techniques, with dramatic speed-ups in strategy execution compared to on-line reasoning.

Details DOI

I&C Journal 2015 Journal Article

HRELTL: A temporal logic for hybrid systems

Alessandro Cimatti
Marco Roveri
Stefano Tonetta

Hybrid traces are useful to describe behaviors of dynamic systems where continuous and discrete evolutions are combined. The ability to represent sets of traces by means of formulas in temporal logic has recently found important applications in various fields, such as requirements analysis, compositional verification, and contract-based design. In this paper we present HRELTL, a temporal logic to characterize hybrid traces. The logic is highly expressive: it allows the description of continuous behaviors, by expressing mathematical constraints over derivatives, and discrete behaviors, by constraining values of variables across instantaneous transitions. HRELTL combines the power of temporal operators and regular expressions, and enjoys important properties such as sampling invariance. We demonstrate that the satisfiability problem for a fragment of HRELTL allows for a satisfiability-preserving reduction to RELTL(RA), a logic over discrete traces with atoms in non-linear Real Arithmetic for which automated reasoning procedures are being developed.

Details DOI

AAAI Conference 2015 Conference Paper

Strong Temporal Planning with Uncontrollable Durations: A State-Space Approach

Alessandro Cimatti
Andrea Micheli
Marco Roveri

In many practical domains, planning systems are required to reason about durative actions. A common assumption in the literature is that the executor is allowed to decide the duration of each action. However, this assumption may be too restrictive for applications. In this paper, we tackle the problem of temporal planning with uncontrollable action durations. We show how to generate robust plans, that guarantee goal achievement despite the uncontrollability of the actual duration of the actions. We extend the state-space temporal planning framework, integrating recent techniques for solving temporal problems under uncertainty. We discuss different ways of lifting the total order plans generated by the heuristic search to partial order plans, showing (in)completeness results for each of them. We implemented our approach on top of COLIN, a stateof-the-art planner. An experimental evaluation over several benchmark problems shows the practical feasibility of the proposed approach.

PDF Details

TIME Conference 2014 Conference Paper

Sound and Complete Algorithms for Checking the Dynamic Controllability of Temporal Networks with Uncertainty, Disjunction and Observation

Alessandro Cimatti
Luke Hunsberger
Andrea Micheli
Roberto Posenato
Marco Roveri

Temporal networks are data structures for representing and reasoning about temporal constraints on activities. Many kinds of temporal networks have been defined in the literature, differing in their expressiveness. The simplest kinds of networks have polynomial algorithms for determining their consistency or controllability, but corresponding algorithms for more expressive networks (e. g. , Those that include observation nodes or disjunctive constraints) have so far been unavailable. However, recent work has introduced a new approach to such algorithms based on translating temporal networks into Timed Game Automata (TGAs) and then using off-the-shelf software to synthesize execution strategies -- or determine that none exist. So far, that approach has only been used on Simple Temporal Networks with Uncertainty, for which polynomial algorithms already exist. This paper extends the temporal-network-to-TGA approach to accommodate observation nodes and disjunctive constraints. Insodoing the paper presents, for the first time, sound and complete algorithms for checking the dynamic controllability of these more expressive networks. The translations also highlight the theoretical relationships between various kinds of temporal networks and the TGA model. The new algorithms have immediate applications in the workflow models being developed to automate business processes, including in the health-care domain.

Details

AAAI Conference 2014 Conference Paper

Using Timed Game Automata to Synthesize Execution Strategies for Simple Temporal Networks with Uncertainty

Alessandro Cimatti
Luke Hunsberger
Andrea Micheli
Marco Roveri

A Simple Temporal Network with Uncertainty (STNU) is a structure for representing and reasoning about temporal constraints in domains where some temporal durations are not controlled by the executor. The most important property of an STNU is whether it is dynamically controllable (DC); that is, whether there exists a strategy for executing the controllable time-points that guarantees that all constraints will be satisfied no matter how the uncontrollable durations turn out. This paper provides a novel mapping from STNUs to Timed Game Automata (TGAs) that: (1) explicates the deep theoretical relationships between STNUs and TGAs; and (2) enables the memoryless strategies generated from the TGA to be transformed into equivalent STNU execution strategies that reduce the real-time computational burden for the executor. The paper formally proves that the STNU-to-TGA encoding properly captures the execution semantics of STNUs.

PDF Details

AAAI Conference 2013 Conference Paper

Timelines with Temporal Uncertainty

Alessandro Cimatti
Andrea Micheli
Marco Roveri

Timelines are a formalism to model planning domains where the temporal aspects are predominant, and have been used in many real-world applications. Despite their practical success, a major limitation is the inability to model temporal uncertainty, i. e. the fact that the plan executor cannot decide the actual duration of some activities. In this paper we make two key contributions. First, we propose a comprehensive, semantically well founded framework that (conservatively) extends with temporal uncertainty the state of the art timeline approach. Second, we focus on the problem of producing time-triggered plans that are robust with respect to temporal uncertainty, under a bounded horizon. In this setting, we present the first complete algorithm, and we show how it can be made practical by leveraging the power of Satisfiability Modulo Theories.

PDF Details

AAAI Conference 2012 Conference Paper

Solving Temporal Problems Using SMT: Weak Controllability

Alessandro Cimatti
Andrea Micheli
Marco Roveri

Temporal problems with uncertainty are a well established formalism to model time constraints of a system interacting with an uncertain environment. Several works have addressed the definition and the solving of controllability problems, and three degrees of controllability have been proposed: weak, strong, and dynamic. In this work we focus on weak controllability: we address both the decision and the strategy extraction problems. Extracting a strategy means finding a function from assignments to uncontrollable time points to assignments to controllable time points that fulfills all the temporal constraints. We address the two problems in the satisfiability modulo theory framework. We provide a clean and complete formalization of the problems, and we propose novel techniques to extract strategies. We also provide experimental evidence of the scalability and efficiency of the proposed techniques.

PDF Details

IJCAI Conference 2011 Conference Paper

A Comprehensive Approach to On-Board Autonomy Verification and Validation

Marco Bozzano
Alessandro Cimatti
Marco Roveri
Andrei Tchaltsev

Deep space missions are characterized by severely constrained communication links. To meet the needs of future missions and increase their scientific return, future space systems will require an increased level of autonomy on-board. In this work, we propose a comprehensive approach to on-board autonomy relying on model-based reasoning, and encompassing many important reasoning capabilities such as plan generation, validation, execution and monitoring, FDIR, and run-time diagnosis. The controlled platform is represented symbolically, and the reasoning capabilities are seen as symbolic manipulation of such formal model. We have developed a prototype of our framework, implemented within an on-board Autonomous Reasoning Engine. We have evaluated our approach on two case-studies inspired by real-world, ongoing projects, and characterized it in terms of reliability, availability and performance.

PDF Details DOI

AIJ Journal 2006 Journal Article

Strong planning under partial observability

Piergiorgio Bertoli
Alessandro Cimatti
Marco Roveri
Paolo Traverso

Rarely planning domains are fully observable. For this reason, the ability to deal with partial observability is one of the most important challenges in planning. In this paper, we tackle the problem of strong planning under partial observability in nondeterministic domains: find a conditional plan that will result in a successful state, regardless of multiple initial states, nondeterministic action effects, and partial observability. We make the following contributions. First, we formally define the problem of strong planning within a general framework for modeling partially observable planning domains. Second, we propose an effective planning algorithm, based on and-or search in the space of beliefs. We prove that our algorithm always terminates, and is correct and complete. In order to achieve additional effectiveness, we leverage on a symbolic, bdd-based representation for the domain, and propose several search strategies. We provide a thorough experimental evaluation of our approach, based on a wide selection of benchmarks. We compare the performance of the proposed search strategies, and identify a uniform winner that combines heuristic distance measures with mechanisms that reduce runtime uncertainty. Then, we compare our planner mbp with other state-of-the art-systems. mbp is able to outperform its competitor systems, often by orders of magnitude.

Details DOI

ICAPS Conference 1998 Conference Paper

Strong Planning in Non-Deterministic Domains Via Model Checking

Alessandro Cimatti
Marco Roveri
Paolo Traverso

Most real world domains are non-deterministic: the state of the world can be incompletely known, the effect of actions can not be completely foreseen, and the environment can change in unpredictable ways. Automatic plan formation in non-deterministic domains is, however, still an open problem. In this paper we show how to do strong planning in non-deterministic domains, i.e. finding automatically plans which are guaranteed to achieve the goal regardless of non-determinism. We define a notion of planning solution which is guaranteed to achieve the goal independently of non-determinism, a notion of plan including conditionals and iterations, and an automatic decision procedure for strong planning based on model checking techniques. The procedure is correct, complete and returns optimal plans. The work has been implemented in MBP, a planner based on model checking techniques.

Details