Arrow Research search

Author name cluster

Fabio Patrizi

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.

51 papers
2 author rows

Possible papers

51

AAMAS Conference 2025 Conference Paper

Managing an Agent's Changing Intentions Using LTL f Synthesis

  • Giuseppe De Giacomo
  • Yves Lespérance
  • Gianmarco Parretti
  • Fabio Patrizi
  • Renzo Schram

Autonomous agents’ intentions (goals they are committed to) typically change as they operate. We develop a new model of intention change for such agents. We assume that the agent operates in a fully observable nondeterministic (fond) domain and uses Linear Temporal Logic over finite traces (ltl𝑓 ) to represent intentions. We exploit ltl𝑓 synthesis notions and techniques to generate strategies for the agent to satisfy its intentions and to revise them when the agent adopts new intentions or drops existing ones; this ensures that the agent’s intentions always remain realizable. We propose automata-based methods to efficiently manage ltl𝑓 intentions by exploiting auxiliary data structures built during synthesis. We implement a prototype and evaluate its effectiveness experimentally.

AAAI Conference 2024 Conference Paper

Mimicking Behaviors in Separated Domains (Abstract Reprint)

  • Giuseppe De Giacomo
  • Dror Fried
  • Fabio Patrizi
  • Shufang Zhu

Devising a strategy to make a system mimic behaviors from another system is a problem that naturally arises in many areas of Computer Science. In this work, we interpret this problem in the context of intelligent agents, from the perspective of LTLf, a formalism commonly used in AI for expressing finite-trace properties. Our model consists of two separated dynamic domains, D_A and D_B, and an LTLf specification that formalizes the notion of mimicking by mapping properties on behaviors (traces) of D_A into properties on behaviors of D_B. The goal is to synthesize a strategy that step-by-step maps every behavior of D_A into a behavior of D_B so that the specification is met. We consider several forms of mapping specifications, ranging from simple ones to full LTLf, and for each, we study synthesis algorithms and computational properties.

ECAI Conference 2024 Conference Paper

Monte Carlo Tree Search with State Merging for Reinforcement Learning in Regular Decision Processes

  • Gabriel Paludo Licks
  • Fabio Patrizi
  • Giuseppe De Giacomo

This paper introduces a novel algorithm for Reinforcement Learning (RL) in Regular Decision Processes (RDPs), a model of non-Markovian decision processes where dynamics and rewards depend on regular properties of the history. Our algorithm is inspired by Monte Carlo tree search (MCTS), yet it is improved with state merging capabilities. Performing merges allows us to evolve the tree model into a graph over time, as we periodically perform similarity tests borrowed from automata learning theory to learn states that are equivalent to one another. This results in improved efficiency and scalability over standard MCTS. We present empirical results that demonstrate orders of magnitude performance improvement over the state-of-the-art RL algorithms for RDPs.

TIST Journal 2023 Journal Article

Data-Aware Declarative Process Mining with SAT

  • Fabrizio Maria Maggi
  • Andrea Marrella
  • Fabio Patrizi
  • Vasyl Skydanienko

Process Mining is a family of techniques for analyzing business process execution data recorded in event logs. Process models can be obtained as output of automated process discovery techniques or can be used as input of techniques for conformance checking or model enhancement. In Declarative Process Mining, process models are represented as sets of temporal constraints (instead of procedural descriptions where all control-flow details are explicitly modeled). An open research direction in Declarative Process Mining is whether multi-perspective specifications can be supported, i.e., specifications that not only describe the process behavior from the control-flow point of view, but also from other perspectives like data or time. In this article, we address this question by considering SAT (Propositional Satisfiability Problem) as a solving technology for a number of classical problems in Declarative Process Mining, namely, log generation, conformance checking, and temporal query checking. To do so, we first express each problem as a suitable FO (First-Order) theory whose bounded models represent solutions to the problem, and then find a bounded model of such theory by compilation into SAT.

AAAI Conference 2023 Conference Paper

Exploiting Multiple Abstractions in Episodic RL via Reward Shaping

  • Roberto Cipollone
  • Giuseppe De Giacomo
  • Marco Favorito
  • Luca Iocchi
  • Fabio Patrizi

One major limitation to the applicability of Reinforcement Learning (RL) to many practical domains is the large number of samples required to learn an optimal policy. To address this problem and improve learning efficiency, we consider a linear hierarchy of abstraction layers of the Markov Decision Process (MDP) underlying the target domain. Each layer is an MDP representing a coarser model of the one immediately below in the hierarchy. In this work, we propose a novel form of Reward Shaping where the solution obtained at the abstract level is used to offer rewards to the more concrete MDP, in such a way that the abstract solution guides the learning in the more complex domain. In contrast with other works in Hierarchical RL, our technique has few requirements in the design of the abstract models and it is also tolerant to modeling errors, thus making the proposed approach practical. We formally analyze the relationship between the abstract models and the exploration heuristic induced in the lower-level domain. Moreover, we prove that the method guarantees optimal convergence and we demonstrate its effectiveness experimentally.

JAIR Journal 2023 Journal Article

Mimicking Behaviors in Separated Domains

  • Giuseppe De Giacomo
  • Dror Fried
  • Fabio Patrizi
  • Shufang Zhu

Devising a strategy to make a system mimic behaviors from another system is a problem that naturally arises in many areas of Computer Science. In this work, we interpret this problem in the context of intelligent agents, from the perspective of ltlf, a formalism commonly used in AI for expressing finite-trace properties. Our model consists of two separated dynamic domains, DA and DB, and an LTLf specification that formalizes the notion of mimicking by mapping properties on behaviors (traces) of DA into properties on behaviors of DB. The goal is to synthesize a strategy that step-by-step maps every behavior of DA into a behavior of DB so that the specification is met. We consider several forms of mapping specifications, ranging from simple ones to full LTLf, and for each, we study synthesis algorithms and computational properties.

AAAI Conference 2023 Conference Paper

Monitoring Arithmetic Temporal Properties on Finite Traces

  • Paolo Felli
  • Marco Montali
  • Fabio Patrizi
  • Sarah Winkler

We study monitoring of linear-time arithmetic properties against finite traces generated by an unknown dynamic system. The monitoring state is determined by considering at once the trace prefix seen so far, and all its possible finite-length, future continuations. This makes monitoring at least as hard as satisfiability and validity. Traces consist of finite sequences of assignments of a fixed set of variables to numerical values. Properties are specified in a logic we call ALTLf, combining LTLf (LTL on finite traces) with linear arithmetic constraints that may carry lookahead, i.e., variables may be compared over multiple instants of the trace. While the monitoring problem for this setting is undecidable in general, we show decidability for (a) properties without lookahead, and (b) properties with lookahead that satisfy the abstract, semantic condition of finite summary, studied before in the context of model checking. We then single out concrete, practically relevant classes of constraints guaranteeing finite summary. Feasibility is witnessed by a prototype implementation.

AIIM Journal 2023 Journal Article

Monitoring hybrid process specifications with conflict management: An automata-theoretic approach

  • Anti Alman
  • Fabrizio Maria Maggi
  • Marco Montali
  • Fabio Patrizi
  • Andrey Rivkin

Complexity of medical treatments can vary from prescribing medicine for a specific ailment to managing a complex set of simultaneous medical issues. In the latter case, doctors are assisted by clinical guidelines which outline standard medical procedures, tests, treatments, etc. To facilitate the use of such guidelines, they can be digitized as processes and adopted in complex process engines offering additional help to health providers such as decision support while monitoring active treatments so as to detect flaws in treatment procedures and suggest possible reactions on them. For example, a patient may present symptoms of multiple diseases simultaneously (requiring multiple clinical guidelines to be followed), while also being allergic to some often-used drugs (requiring additional constraints to be respected). This can easily lead to treating a patient based on a set of process specifications which are not fully compatible with each other. While a scenario like that commonly occurs in practice, research in that direction has thus far given little consideration to how to specify multiple clinical guidelines and how to automatically combine their specifications in the context of the monitoring task. In our previous work [2], we presented a conceptual framework for handling the above cases in the context of monitoring. In this paper, we present the algorithms necessary for implementing key components of this conceptual framework. More specifically, we provide formal languages for representing clinical guideline specifications and formalize a solution for monitoring the interplay of such specifications expressed as a combination of (data-aware) Petri nets and temporal logic rules. The proposed solution seamlessly handles combination of the input process specifications and provides both early conflict detection and decision support during process execution. We also discuss a proof-of-concept implementation of our approach and present the results of extensive scalability experiments.

ECAI Conference 2023 Conference Paper

Optimal Alignment of Temporal Knowledge Bases

  • Oliver Fernández Gil
  • Fabio Patrizi
  • Giuseppe Perelli
  • Anni-Yasmin Turhan

Answering temporal CQs over temporalized Description Logic knowledge bases (TKB) is a main technique to realize ontology-based situation recognition. In case the collected data in such a knowledge base is inaccurate, important query answers can be missed. In this paper we introduce the TKB Alignment problem, which computes a variant of the TKB that minimally changes the TKB, but entails the given temporal CQ and is in that sense (cost-) optimal. We investigate this problem for ALC TKBs and conjunctive queries with LTL operators and devise a solution technique to compute (cost-optimal) alignments of TKBs that extends techniques for the alignment problem for propositional LTL over finite traces.

ECAI Conference 2023 Conference Paper

Strategy Repair in Reachability Games

  • Pierre Gaillard
  • Fabio Patrizi
  • Giuseppe Perelli

We introduce Strategy Repair, the problem of finding a minimal amount of modifications to turn a strategy for a reachability game from losing into winning. The problem is relevant for a number of settings in Planning and Synthesis, where solutions essentially correspond to winning strategies in a suitably defined reachability game. We show, via reduction from Vertex Cover, that Strategy Repair is NP-complete and devise two algorithms, one optimal and exponential and one polynomial but sub-optimal, which we compare experimentally. The reported experimentation includes some heuristics for strategy modification, which proved crucial in dramatically improving performance.

AAAI Conference 2022 Conference Paper

ASP-Based Declarative Process Mining

  • Francesco Chiariello
  • Fabrizio Maria Maggi
  • Fabio Patrizi

We put forward Answer Set Programming (ASP) as a solution approach for three classical problems in Declarative Process Mining: Log Generation, Query Checking, and Conformance Checking. These problems correspond to different ways of analyzing business processes under execution, starting from sequences of recorded events, a. k. a. event logs. We tackle them in their data-aware variant, i. e. , by considering events that carry a payload (set of attribute-value pairs), in addition to the performed activity, specifying processes declaratively with an extension of linear-time temporal logic over finite traces (LTLf ). The data-aware setting is significantly more challenging than the control-flow one: Query Checking is still open, while the existing approaches for the other two problems do not scale well. The contributions of the work include an ASP encoding schema for the three problems, their solution, and experiments showing the feasibility of the approach.

PRL Workshop 2022 Workshop Paper

Exploiting Multiple Levels of Abstractions in Episodic RL via Reward Shaping

  • Roberto Cipollone
  • Giuseppe De Giacomo
  • Marco Favorito
  • Luca Iocchi
  • Fabio Patrizi

Reinforcement Learning (RL) agents have no model available to predict outcomes of their actions. While this allowed wide applicability of RL algorithms, this lack of knowledge also demands a significant number of interactions with the environment before an optimal policy can be estimated. Indeed, most of the successes of RL achieved in recent years come from the digital world (e. g. video games, simulated environments), where a large amount of samples can be easily generated. Still, even in these cases, such large number of samples might not be available, as the simulation costs may be very high. As a result, applications of RL in real environments, such as real robots, are still very rare. Many RL tasks are goal-oriented, in which a set of environment states are denoted as target configurations. Complex tasks induce sparse goals and, as a consequence, sparse rewards. This is known to be a challenging scenario for RL, which increases the requirements on the number of samples to collect. Unfortunately, sparse goal states are very common, as they may arise in simple tasks on large state spaces (such as reaching specific locations in a complex environment), or complex behaviours even in modest environments (such as the successful completion of a desired sequence (Brafman, De Giacomo, and Patrizi 2018; Icarte et al. 2018)). From Hierarchical RL approaches, it is known that abstractions play a fundamental role in subtask decomposition and efficient exploration. The technique proposed in this work allows to exploit abstractions of Markov Decision Processes (MDPs) to allow learning algorithms to effectively explore the ground1 environment, while guaranteeing optimal convergence. The abstraction of some ground MDP M is an MDP Mφ whose states represent sets of states of M. A simple example is that of an agent moving in a map. States of M could determine the agent’s position in terms of continuous coordinates, orientation, and other configurations. States of the abstraction Mφ, instead, may be coarser descriptions, for example, through discretization or by projecting out some state variables. Such compression corresponds, ultimately, to partitioning the concrete state-space and implicitly defines a mapping from concrete to abstract states. Importantly, action spaces of M and Mφ may differ, as each model would include the actions that are best appropriate for each representation. The core intuition is that, by first learning the optimal policy ρφ of the abstract MDP, we obtain a value estimate Vφ∗ which can be exploited to guide learning on the ground model M. Technically, we adopt a variant of Reward Shaping (RS), which is generated from Vφ∗, which offers rewards that are consistent with the correspondence between states at the ground and the abstract level. In this way, when learning in the concrete model M, the agent is biased to visit first states corresponding to the abstract ones preferred by ρφ, thus trying, in a sense, to replicate the behavior of ρφ at the ground level. For such exploration bias to be effective, it is essential that the transitions of Mφ are good proxies for the dynamics of M. We characterize this relation by identifying conditions under which the optimal policy of the ground MDP with computed rewards converges to a near-optimal exploration policy. We call such model the biased MDP. An important difference with respect to previous works is that, since the proposed approach focuses on the definition of a novel RS mechanism, it is very general and may be com- Copyright © 2022, Association for the Advancement of Artificial Intelligence (www. aaai. org). All rights reserved. 1 We follow the nomenclature from (Li, Walsh, and Littman 2006). One major limitation of Reinforcement Learning (RL) algorithms, which limits applicability in many practical domains, is the large amount of samples required to learn an optimal policy. To improve learning efficiency, we consider a hierarchy of abstraction layers, where the Markov Decision Process (MDP) underlying the target domain can be abstracted at multiple levels by other MDPs. Each abstract model in the hierarchy is a coarser representation of the next one below, which captures the relevant dynamics in finer resolution. This paper proposes a novel form of Reward Shaping defined in terms of the solution obtained in the abstract levels. Theoretical guarantees about optimality and experimental validation of learning efficiency are discussed in the paper. Our technique has minimum requirements in the design of abstract models and is also tolerant to modelling errors in abstractions, thus making the proposed method of practical interest.

AIJ Journal 2022 Journal Article

Situation calculus for controller synthesis in manufacturing systems with first-order state representation

  • Giuseppe De Giacomo
  • Paolo Felli
  • Brian Logan
  • Fabio Patrizi
  • Sebastian Sardiña

Manufacturing is transitioning from a mass production model to a service model in which facilities ‘bid’ to produce products. To decide whether to bid for a complex, previously unseen product, a facility must be able to synthesize, on the fly, a process plan controller that delegates abstract manufacturing tasks in a supplied process recipe to the available manufacturing resources. Often manufacturing processes depend on the data and objects (parts) they produce and consume. To formalize this aspect we need to adopt a first-order representation of the state of the processes. First-order representations of the state are commonly considered in reasoning about action in AI, and here we show that we can leverage the wide literature on the Situation Calculus and ConGolog programs to formalize this kind of manufacturing. With such a formalization available, we investigate how to synthesize process plan controllers in this first-order state setting. We also identify two important decidable cases—finite domains and bounded action theories—for which we provide techniques to actually synthesize the controller.

IJCAI Conference 2022 Conference Paper

Situation Calculus for Controller Synthesis in Manufacturing Systems with First-Order State Representation (Extended Abstract)

  • Giuseppe De Giacomo
  • Paolo Felli
  • Brian Logan
  • Fabio Patrizi
  • Sebastian Sardiña

Manufacturing is transitioning from a mass production model to a service model in which facilities `bid' for previously unseen products. To decide whether to bid for a previously unseen product, a facility must be able to synthesize, on the fly, a process plan controller that delegates abstract manufacturing tasks in a supplied process recipe to the available manufacturing resources. First-order representations of the state are commonly considered in reasoning about action in AI. Here we show that we can leverage the wide literature on the Situation Calculus automatically synthesize such controllers. We identify two important decidable cases---finite domains and bounded action theories---for which we provide practical synthesis techniques.

IJCAI Conference 2022 Conference Paper

Verification and Monitoring for First-Order LTL with Persistence-Preserving Quantification over Finite and Infinite Traces

  • Diego Calvanese
  • Giuseppe De Giacomo
  • Marco Montali
  • Fabio Patrizi

We address the problem of model checking first-order dynamic systems where new objects can be injected in the active domain during execution. Notable examples are systems induced by a first-order action theory, e. g. , expressed in the Situation Calculus. Recent results have shown that, under the state-boundedness assumption, such systems, in spite of having a first-order representation of the state, admit decidable model checking for full first-order mu-calculus. However, interestingly, model checking remains undecidable in the case of first-order LTL (LTL-FO). In this paper, we show that in LTL-FOp, which is the fragment of LTL-FO in which quantification is over objects that persist along traces, model checking state-bounded systems becomes decidable over finite and infinite traces. We then employ this result to show how to handle monitoring of LTL-FOp properties against a trace stemming from an unknown state-bounded dynamic system, simultaneously considering the finite trace up to the current point, and all its possibly infinite future continuations.

PRL Workshop 2021 Workshop Paper

Domain-independent reward machines for modular integration of planning and learning

  • Giuseppe De Giacomo
  • Marco Favorito
  • Luca Iocchi
  • Fabio Patrizi

Integrating planning and learning components has many advantages in practical applications, as it allows for combining the different benefits of the two approaches: prediction of future states from planning with adaptivity to current situations from learning. However, a problem with is approach is that the two components should share a common representation of the information about the environment (e. g. , states and actions). Previous work addresses this problem in the case where planning and learning are defined over different state variables, by defining a joint state space and a mapping between the two representations. In this paper, we present a method for integrating planning and reinforcement learning using a modular design where the two components can use their own representation formalism, without requiring an explicit mapping between them. More specifically, we introduce the concept of domain-independent reward machines, generated by a goal-oriented planning system and use them to drive a reinforcement learning agent to reach a goal state. Moreover, we show how to automatically generate and use sub task decomposition to speed up the reinforcement learning process.

KR Conference 2021 Conference Paper

Timed Trace Alignment with Metric Temporal Logic over Finite Traces

  • Giuseppe De Giacomo
  • Aniello Murano
  • Fabio Patrizi
  • Giuseppe Perelli

Trace Alignment is a prominent problem in Declarative Process Mining, which consists in identifying a minimal set of modifications that a log trace (produced by a system under execution) requires in order to be made compliant with a temporal specification. In its simplest form, log traces are sequences of events from a finite alphabet and specifications are written in DECLARE, a strict sublanguage of linear-time temporal logic over finite traces (LTLf ). The best approach for trace alignment has been developed in AI, using cost-optimal planning, and handles the whole LTLf. In this paper, we study the timed version of trace alignment, where events are paired with timestamps and specifications are provided in metric temporal logic over finite traces (MTLf ), essentially a superlanguage of LTLf. Due to the infiniteness of timestamps, this variant is substantially more challenging than the basic version, as the structures involved in the search are (uncountably) infinite-state, and calls for a more sophisticated machinery based on alternating (timed) automata, as opposed to the standard finite-state automata sufficient for the untimed version. The main contribution of the paper is a provably correct, effective technique for Timed Trace Alignment that takes advantage of results on MTLf decidability as well as on reachability for well-structured transition systems.

KR Conference 2020 Conference Paper

High-level Programming via Generalized Planning and LTL Synthesis

  • Blai Bonet
  • Giuseppe De Giacomo
  • Hector Geffner
  • Fabio Patrizi
  • Sasha Rubin

We look at program synthesis where the aim is to automatically synthesize a controller that operates on data structures and from which a concrete program can be easily derived. We do not aim at a fully-automatic process or tool that produces a program meeting a given specification of the program’s behaviour. Rather, we aim at the design of a clear and well-founded approach for supporting programmers at the design and implementation phases. Concretely, we first show that a program synthesis task can be modeled as a generalized planning problem. This is done at an abstraction level where the involved data structures are seen as black-boxes that can be interfaced with actions and observations, the first corresponding to the operations and the second to the queries provided by the data structure. The abstraction level is high enough to capture intuitive and common assumptions as well as general and simple strategies used by programmers, and yet it contains sufficient structure to support the automated generation of concrete solutions (in the form of controllers). From such controllers and the use of standard data structures, an actual program in a general language like C++ or Python can be easily obtained. Then, we discuss how the resulting generalized planning problem can be reduced to an LTL synthesis problem, thus making available any LTL synthesis engine for obtaining the controllers. We illustrate the effectiveness of the approach on a series of examples.

ICAPS Conference 2020 Conference Paper

Imitation Learning over Heterogeneous Agents with Restraining Bolts

  • Giuseppe De Giacomo
  • Marco Favorito
  • Luca Iocchi
  • Fabio Patrizi

A common problem in Reinforcement Learning (RL) is that the reward function is hard to express. This can be overcome by resorting to Inverse Reinforcement Learning (IRL), which consists in first obtaining a reward function from a set of execution traces generated by an expert agent, and then making the learning agent learn the expert's behavior –this is known as Imitation Learning (IL). Typical IRL solutions rely on a numerical representation of the reward function, which raises problems related to the adopted optimization procedures. We describe an IL method where the execution traces generated by the expert agent, possibly via planning, are used to produce a logical (as opposed to numerical) specification of the reward function, to be incorporated into a device known as Restraining Bolt (RB). The RB can be attached to the learning agent to drive the learning process and ultimately make it imitate the expert. We show that IL can be applied to heterogeneous agents, with the expert, the learner and the RB using different representations of the environment's actions and states, without specifying mappings among their representations.

AAAI Conference 2020 Conference Paper

Restraining Bolts for Reinforcement Learning Agents

  • Giuseppe De Giacomo
  • Luca Iocchi
  • Marco Favorito
  • Fabio Patrizi

In this work we have investigated the concept of “restraining bolt”, inspired by Science Fiction. We have two distinct sets of features extracted from the world, one by the agent and one by the authority imposing some restraining specifications on the behaviour of the agent (the “restraining bolt”). The two sets of features and, hence the model of the world attainable from them, are apparently unrelated since of interest to independent parties. However they both account for (aspects of) the same world. We have considered the case in which the agent is a reinforcement learning agent on a set of low-level (subsymbolic) features, while the restraining bolt is specified logically using linear time logic on finite traces LTLf /LDLf over a set of high-level symbolic features. We show formally, and illustrate with examples, that, under general circumstances, the agent can learn while shaping its goals to suitably conform (as much as possible) to the restraining bolt specifications. 1

KR Conference 2020 Conference Paper

Temporal Logic Monitoring Rewards via Transducers

  • Giuseppe De Giacomo
  • Marco Favorito
  • Luca Iocchi
  • Fabio Patrizi
  • Alessandro Ronca

In Markov Decision Processes (MDPs), rewards are assigned according to a function of the last state and action. This is often limiting, when the considered domain is not naturally Markovian, but becomes so after careful engineering of extended state space. The extended states record information from the past that is sufficient to assign rewards by looking just at the last state and action. Non-Markovian Reward Decision Processes (NRMDPs) extend MDPs by allowing for non-Markovian rewards, which depend on the history of states and actions. Non-Markovian rewards can be specified in temporal logics on finite traces such as LTLf/LDLf, with the great advantage of a higher abstraction and succinctness; they can then be automatically compiled into an MDP with an extended state space. We contribute to the techniques to handle temporal rewards and to the solutions to engineer them. We first present an approach to compiling temporal rewards which merges the formula automata into a single transducer, sometimes saving up to an exponential number of states. We then define monitoring rewards, which add a further level of abstraction to temporal rewards by adopting the four-valued conditions of runtime monitoring; we argue that our compilation technique allows for an efficient handling of monitoring rewards. Finally, we discuss application to reinforcement learning.

ICAPS Conference 2019 Conference Paper

Foundations for Restraining Bolts: Reinforcement Learning with LTLf/LDLf Restraining Specifications

  • Giuseppe De Giacomo
  • Luca Iocchi
  • Marco Favorito
  • Fabio Patrizi

In this work we investigate on the concept of “restraining bolt”, envisioned in Science Fiction. Specifically we introduce a novel problem in AI. We have two distinct sets of features extracted from the world, one by the agent and one by the authority imposing restraining specifications (the “restraining bolt”). The two sets are apparently unrelated since of interest to independent parties, however they both account for (aspects of) the same world. We consider the case in which the agent is a reinforcement learning agent on the first set of features, while the restraining bolt is specified logically using linear time logic on finite traces LTLf/LDLf over the second set of features. We show formally, and illustrate with examples, that, under general circumstances, the agent can learn while shaping its goals to suitably conform (as much as possible) to the restraining bolt specifications.

I&C Journal 2018 Journal Article

First-order μ-calculus over generic transition systems and applications to the situation calculus

  • Diego Calvanese
  • Giuseppe De Giacomo
  • Marco Montali
  • Fabio Patrizi

We consider μ L, μ L a, and μ L p, three variants of the first-order μ-calculus studied in verification of data-aware processes, that differ in the form of quantification on objects across states. Each of these three logics has a distinct notion of bisimulation. We show that the three notions collapse for generic dynamic systems, which include all state-based systems specified using a logical formalism, e. g. , the situation calculus. Hence, for such systems, μ L, μ L a, and μ L p have the same expressive power. We also show that, when the dynamic system stores only a bounded number of objects in each state (e. g. , for bounded situation calculus action theories), a finite abstraction can be constructed that is faithful for μ L (the most general variant), yielding decidability of verification. This contrasts with the undecidability for first-order ltl, and notably implies that first-order ltl cannot be captured by μ L.

AAAI Conference 2018 Conference Paper

LTLf/LDLf Non-Markovian Rewards

  • Ronen Brafman
  • Giuseppe De Giacomo
  • Fabio Patrizi

In Markov Decision Processes (MDPs), the reward obtained in a state is Markovian, i. e. , depends on the last state and action. This dependency makes it difficult to reward more interesting long-term behaviors, such as always closing a door after it has been opened, or providing coffee only following a request. Extending MDPs to handle non-Markovian reward functions was the subject of two previous lines of work. Both use LTL variants to specify the reward function and then compile the new model back into a Markovian model. Building on recent progress in temporal logics over finite traces, we adopt LDLf for specifying non-Markovian rewards and provide an elegant automata construction for building a Markovian model, which extends that of previous work and offers strong minimality and compositionality guarantees.

AAAI Conference 2017 Conference Paper

On the Disruptive Effectiveness of Automated Planning for LTL f -Based Trace Alignment

  • Giuseppe De Giacomo
  • Fabrizio Maria Maggi
  • Andrea Marrella
  • Fabio Patrizi

One major task in business process management is that of aligning real process execution traces to a process model by (minimally) introducing and eliminating steps. Here, we look at declarative process specifications expressed in Linear Temporal Logic on finite traces (LTLf ). We provide a sound and complete technique to synthesize the alignment instructions relying on finite automata theoretic manipulations. Such a technique can be effectively implemented by using planning technology. Notably, the resulting planning-based alignment system significantly outperforms all current state-of-the-art ad-hoc alignment systems. We report an in-depth experimental study that supports this claim.

AIJ Journal 2016 Journal Article

Agent planning programs

  • Giuseppe De Giacomo
  • Alfonso Emilio Gerevini
  • Fabio Patrizi
  • Alessandro Saetti
  • Sebastian Sardina

This work proposes a novel high-level paradigm, agent planning programs, for modeling agents behavior, which suitably mixes automated planning with agent-oriented programming. Agent planning programs are finite-state programs, possibly containing loops, whose atomic instructions consist of a guard, a maintenance goal, and an achievement goal, which act as precondition-invariance-postcondition assertions in program specification. Such programs are to be executed in possibly nondeterministic planning domains and their execution requires generating plans that meet the goals specified in the atomic instructions, while respecting the program control flow. In this paper, we define the problem of automatically synthesizing the required plans to execute an agent planning program, propose a solution technique based on model checking of two-player game structures, and use it to characterize the worst-case computational complexity of the problem as EXPTIME-complete. Then, we consider the case of deterministic domains and propose a different technique to solve agent planning programs, which is based on iteratively solving classical planning problems and on exploiting goal preferences and plan adaptation methods. Finally, we study the effectiveness of this approach for deterministic domains through an experimental analysis on well-known planning domains.

AIJ Journal 2016 Journal Article

Bounded situation calculus action theories

  • Giuseppe De Giacomo
  • Yves Lespérance
  • Fabio Patrizi

In this paper, 1 we investigate bounded action theories in the situation calculus. A bounded action theory is one which entails that, in every situation, the number of object tuples in the extension of fluents is bounded by a given constant, although such extensions are in general different across the infinitely many situations. We argue that such theories are common in applications, either because facts do not persist indefinitely or because the agent eventually forgets some facts, as new ones are learned. We discuss various classes of bounded action theories. Then we show that verification of a powerful first-order variant of the μ-calculus is decidable for such theories. Notably, this variant supports a controlled form of quantification across situations. We also show that through verification, we can actually check whether an arbitrary action theory maintains boundedness.

KR Conference 2016 Conference Paper

On First-Order Mu-Calculus over Situation Calculus Action Theories

  • Diego Calvanese
  • Giuseppe De Giacomo
  • Marco Montali
  • Fabio Patrizi

These results are concerned with verification logics that In this paper we study verification of situation calculus action theories against first-order μ-calculus with quantification across situations. Specifically, we consider μLa and μLp, the two variants of μ-calculus introduced in the literature for verification of data-aware processes. The former requires that quantification ranges over objects in the current active domain, while the latter additionally requires that objects assigned to variables persist across situations. Each of these two logics has a distinct corresponding notion of bisimulation. In spite of the differences we show that the two notions of bisimulation collapse for dynamic systems that are generic, which include all those systems specified through a situation calculus action theory. Then, by exploiting this result, we show that for bounded situation calculus action theories, μLa and μLp have exactly the same expressive power. Finally, we prove decidability of verification of μLa properties over bounded action theories, using finite faithful abstractions. Differently from the μLp case, these abstractions must depend on the number of quantified variables in the μLa formula.

IJCAI Conference 2016 Conference Paper

Plan Synthesis for Knowledge and Action Bases

  • Diego Calvanese
  • Marco Montali
  • Fabio Patrizi
  • Michele Stawowy

We study plan synthesis for a variant of Knowledge and Action Bases (KABs), a rich, dynamic framework, where states are description logic (DL) knowledge bases (KBs) whose extensional part is manipulated by actions that possibly introduce new objects from an infinite domain. We show that plan existence over KABs is undecidable even under severe restrictions. We then focus on state-bounded KABs, a class for which plan existence is decidable, and provide sound and complete plan synthesis algorithms, which combine techniques based on standard planning, DL query answering, and finite-state abstraction. All results hold for any DL with decidable query answering. We finally show that for lightweight DLs, plan synthesis can be compiled into standard ADL planning.

AAAI Conference 2016 Conference Paper

Verifying ConGolog Programs on Bounded Situation Calculus Theories

  • Giuseppe De Giacomo
  • Yves Lespérance
  • Fabio Patrizi
  • Sebastian Sardina

We address verification of high-level programs over situation calculus action theories that have an infinite object domain, but bounded fluent extensions in each situation. We show that verification of μ-calculus temporal properties against ConGolog programs over such bounded theories is decidable in general. To do this, we reformulate the transition semantics of ConGolog to keep the bindings of “pick variables” into a separate variable environment whose size is naturally bounded by the number of variables. We also show that for situation-determined ConGolog programs, we can compile away the program into the action theory itself without loss of generality. This can also be done for arbitrary programs, but only to check certain properties, such as if a situation is the result of a program execution, not for μ-calculus verification.

IJCAI Conference 2015 Conference Paper

Description Logic Based Dynamic Systems: Modeling, Verification, and Synthesis

  • Diego Calvanese
  • Giuseppe De Giacomo
  • Marco Montali
  • Fabio Patrizi

In this paper, we overview the recently introduced general framework of Description Logic Based Dynamic Systems, which leverages Levesque’s functional approach to model systems that evolve the extensional part of a description logic knowledge base by means of actions. This framework is parametric w. r. t. the adopted description logic and the progression mechanism. In this setting, we discuss verification and adversarial synthesis for specifications expressed in a variant of first-order µ-calculus, with a controlled form of quantification across successive states and present key decidability results under the natural assumption of state-boundedness.

KR Conference 2014 Short Paper

Action Theories over Generalized Databases with Equality Constraints

  • Fabio Patrizi
  • Stavros Vassos

BATs with generalized fluent databases In this work we study action theories of the situation calculus such that the initial KB is a generalized database with equality constraints (GFDBs). We show that GFDBs characterize the class of definitional KBs and that they are closed under progression. We also show that, under conditions, generalized projection queries can be decided based on an induced transition system and evaluation of local conditions over states. The situation calculus as presented by Reiter (2001) is a three-sorted first-order language with equality (and some limited second-order features). The sorts are used to distinguish between actions, situations, and objects. A situation represents a world history as a sequence of actions. S0 is used to denote the initial situation where no actions have occurred. Sequences of actions are built using the function symbol do, such that do(a, s) denotes the successor situation resulting from performing action a in situation s. A (relational) fluent is a predicate whose last argument is a situation, whose value can change from situation to situation. We also assume a finite number of fluent and action symbols, F and A, and an infinite number of constants C. Reiter (2001) investigates the case where the initial knowledge base V (KB) is a definitional theory characterized as follows: Fi ∈F ∀x~i. F (~xi, S0) ≡ φi (~xi), where φi (~xi), called the definition for Fi, is an unrestricted first-order formula mentioning no situations. Definitional KBs express complete information for fluents under the assumption of the unique-name axioms for constants captured in a set E. For example the following axiom states that there are exactly two atoms true for In(x1, x2, S0), namely In(box, it1, S0) and In(box, it2, S0):

JELIA Conference 2014 Conference Paper

Action Theories over Generalized Databases with Equality Constraints

  • Fabio Patrizi
  • Stavros Vassos

Abstract In this work we focus on situation calculus action theories over generalized databases with equality constraints, here called GFDBs, which are able to finitely represent complete information over a possibly infinite number of objects. We contribute with the following: i) we show that GFDBs characterize the class of definitional KBs and that they are closed under progression; ii) we show that temporal projection queries are decidable for theories with an initial KB expressed as a GFDB, which we call GFDB-BATs; iii) we extend the notion of boundedness to allow for infinite objects in the extensions of fluents and prove that a wide class of generalized projection queries is decidable for GFDB-BAT under a restriction we call C-boundedness; iv) we show that checking whether C-boundedness holds for a given bound is decidable. The proposed action theories are to date the most expressive ones for which there are decidable methods for computing both progression and generalized projection.

ICAPS Conference 2014 Conference Paper

Building Virtual Behaviors from Partially Controllable Available Behaviors in Nondeterministic Environments

  • Giuseppe De Giacomo
  • Fabio Patrizi
  • Sebastian Sardiña

The composition problem involves how to coordinate a set of available modules (e. g. , concrete devices installed in a smart house, such as video cameras, lights, blinds, etc.) so as to implement a desired but non-existent target complex component (e. g. , a complex entertainment house system). This paper summarizes the results in (De Giacomo, Patrizi, and Sardina 2013), by formally defining the problem within an AI context, characterizing its complexity, and identifying effective techniques to solve it. Related results are also briefly discussed.

ECAI Conference 2014 Conference Paper

LTL Verification of Online Executions with Sensing in Bounded Situation Calculus

  • Giuseppe De Giacomo
  • Yves Lespérance
  • Fabio Patrizi
  • Stavros Vassos

We look at agents reasoning about actions from a first-person perspective. The agent has a representation of world as situation calculus action theory. It can perform sensing actions to acquire information. The agent acts "online", i. e. , it performs an action only if it is certain that the action can be executed, and collects sensing results from the actual world. When the agent reasons about its future actions, it indeed considers that it is acting online; however only possible sensing values are available. The kind of reasoning about actions we consider for the agent is verifying a first-order (FO) variant (without quantification across situations) of linear time temporal logic (LTL). We mainly focus on bounded action theories, where the number of facts that are true in any situation is bounded. The main results of this paper are: (i) possible sensing values can be based on consistency if the initial situation description is FO; (ii) for bounded action theories, progression over histories that include sensing results is always FO; (iii) for bounded theories, verifying our FO LTL against online executions with sensing is decidable.

IJCAI Conference 2013 Conference Paper

A Classification of First-Order Progressable Action Theories in Situation Calculus

  • Stavros Vassos
  • Fabio Patrizi

Projection in the situation calculus refers to answering queries about the future evolutions of the modeled domain, while progression refers to updating the logical representation of the initial state so that it reflects the changes due to an executed action. In the general case projection is not decidable and progression may require second-order logic. In this paper we focus on a recent result about the decidability of projection and use it to drive results for the problem of progression. In particular we contribute with the following: (i) a major result showing that for a large class of intuitive action theories with bounded unknowns a first-order progression always exists and can be computed; (ii) a comprehensive classification of the known classes that can be progressed in first-order; (iii) a novel account of nondeterministic actions in the situation calculus.

AIJ Journal 2013 Journal Article

Automatic behavior composition synthesis

  • Giuseppe De Giacomo
  • Fabio Patrizi
  • Sebastian Sardiña

The behavior composition problem amounts to realizing a virtual desired module (e. g. , a surveillance agent system) by suitably coordinating (and re-purposing) the execution of a set of available modules (e. g. , a video camera, vacuum cleaner, a robot, etc.). In particular, we investigate techniques to synthesize a controller implementing a fully controllable target behavior by suitably coordinating available partially controllable behaviors that are to execute within a shared, fully observable, but partially predictable (i. e. , non-deterministic), environment. Both behaviors and environment are represented as arbitrary finite state transition systems. The technique we propose is directly based on the idea that the controller job is to coordinate the concurrent execution of the available behaviors so as to “mimic” the target behavior. To this end, we exploit a variant of the formal notion of simulation to formally capture the notion of “mimicking”, and we show that the technique proposed is sound and complete, optimal with respect to computational complexity, and robust for different kind of system failures. In addition, we demonstrate that the technique is well suited for highly efficient implementation based on synthesis by model checking technologies, by relating the problem to that of finding a winning strategy in a special safety game and explaining how to actually solve it using an existing verification tool.

IJCAI Conference 2013 Conference Paper

Bounded Epistemic Situation Calculus Theories

  • Giuseppe De Giacomo
  • Yves Lespérance
  • Fabio Patrizi

We define the class of e-bounded theories in the epistemic situation calculus, where the number of fluent atoms that the agent thinks may be true is bounded by a constant. Such theories can still have an infinite domain and an infinite set of states. We show that for them verification of an expressive class of first-order µ-calculus temporal epistemic properties is decidable. We also show that if the agent’s knowledge in the initial situation is ebounded and the objective part of an action theory maintains boundedness, then the entire epistemic theory is e-bounded.

IJCAI Conference 2013 Conference Paper

Fair LTL Synthesis for Non-Deterministic Systems Using Strong Cyclic Planners

  • Fabio Patrizi
  • Nir Lipovetzky
  • Hector Geffner

We consider the problem of planning in environments where the state is fully observable, actions have non-deterministic effects, and plans must generate infinite state trajectories for achieving a large class of LTL goals. More formally, we focus on the control synthesis problem under the assumption that the LTL formula to be realized can be mapped into a deterministic Büchi automaton. We show that by assuming that action non-determinism is fair, namely that infinite executions of a nondeterministic action in the same state yield each possible successor state an infinite number of times, the (fair) synthesis problem can be reduced to a standard strong cyclic planning task over reachability goals. Since strong cyclic planners are built on top of efficient classical planners, the transformation reduces the non-deterministic, fully observable, temporally extended planning task into the solution of classical planning problems. A number of experiments are reported showing the potential benefits of this approach to synthesis in comparison with state-of-the-art symbolic methods.

KR Conference 2012 Conference Paper

An Abstraction Technique for the Verification of Artifact-Centric Systems

  • Francesco Belardinelli
  • Alessio Lomuscio
  • Fabio Patrizi

on which services operate. This emphasis on data makes the automata-based formalisms commonly used to model services generally insufficient: one really requires to account for the evolution of the first-order schemas representing the underlying databases. While this makes the resulting verification problem for artifact systems undecidable, partial solutions have been put forward (Deutsch et al. 2009; Belardinelli, Lomuscio, and Patrizi 2011b; 2011a). These techniques enable the verification of basic temporal properties of the artifact system when analysed under a number of conditions. While these results are valuable, they concern the verification of properties of the artifact system per se and do not address the need of modelling and verifying the actions and information properties of the services acting on or through the artifact system. But if artifact systems are to be deployed in a range of information services as their proponents recommend, it is paramount we can model what actions specific participants are allowed and not allowed to make, what knowledge they can and cannot derive in a system run, what system state they can achieve in coordination with their peers, etc. In other words, we need to verify the epistemic properties of a multi-agent system in which artifacts are present, and not just the evolution of the artifacts themselves. In this paper we set about to explore the verification problem for artifact-centric multi-agent systems, i. e., systems of agents interacting through artifact systems, by means of a knowledge-based perspective. We operate in a first-order setting with knowledge and branching time (FO-CTLK). We first remark that the general problem is undecidable and then proceed to give abstraction results that enable us, in a large class of cases of practical interest, to be able to analyse the model checking of finite approximations rather than the plain infinite model with unbounded database schemas. We stress the fact that all results are obtained for the full firstorder temporal epistemic logic FO-CTLK with identity. So, we assume no restriction on the specification language. The rest of the paper is as follows. In Section 2 we identify the problem, give a general semantics for artifact-centric multi-agent systems (AC-MAS), as well as comment on the undecidability of the model checking problem in the general case. In Section 3 we explore abstraction results that enable us to translate the problem to the model checking of finite We explore the paradigm of artifact-centric systems from a knowledge-based perspective. We provide a semantics based on interpreted-systems to interpret a first-order temporalepistemic language with identity in a multi-agent setting. We consider the model checking problem for this language and provide abstraction results. We isolate a natural subclass of artifact-systems for which the model checking problem is decidable. We give an upper bound on the complexity of the model checking problem.

KR Conference 2012 Conference Paper

Bounded Situation Calculus Action Theories and Decidable Verification

  • Giuseppe De Giacomo
  • Yves Lespérance
  • Fabio Patrizi

Here, we present an important new result on decidability of the situation calculus, showing that verification of bounded action theories is decidable. Bounded action theories are basic action theories (Reiter 2001), where it is entailed that in all situations, the number of ground fluent atoms is bounded. In such theories, the object domain remains nonetheless infinite, as is the domain of situations. But why should we believe that practical domains conform to this boundedness assumption? While it is often assumed that the law of inertia applies and that ground fluent atoms persist indefinitely in the absence of actions that affect them, we all know that pretty much everything eventually decays and changes. We may not even know how the change may happen, but nevertheless know that it will. Another line of argument for boundedness is epistemic. Agents remember facts that they use and periodically try to confirm them, often by sensing. A fact that never gets used is eventually forgotten. If a fact can never be confirmed, it may be given up as too uncertain. Given this, it seems plausible that an agent’s knowledge would always remain bounded. While these philosophical arguments are interesting and relate to some deep questions about knowledge representation, one may take a more pragmatic stance, and this is what we do here. We identify some interesting classes of bounded action theories and show how they can model typical example domains. We also show how we can transform arbitrary basic action theories into bounded action theories, either by blocking actions that would exceed the bound, or by having persistence (frame axioms) apply only for a bounded number of steps. The main result of the paper is that verification of an expressive class of first-order (FO) µ-calculus temporal properties in bounded action theories is in fact decidable. This means that we can check whether a system or process specified over such a theory satisfies some specification even if we have an infinite domain and an infinite set of situations or states. In a nutshell, we prove our results by focussing on the active domain of situations, i. e., the set of objects for which some atomic fluent hold; we know that the set of such active objects is bounded. We show that essentially we can abstract situations whose active domains are isomorphic into a single state, and thus, by suitably abstracting also actions, we can obtain an abstract finite transition system that satisfies exactly the same formulas of our variant of the µ-calculus. We define a notion of bounded action theory in the situation calculus, where the theory entails that in all situations, the number of ground fluent atoms is bounded by a constant. Such theories can still have an infinite domain and an infinite set of states. We argue that such theories are fairly common in applications, either because facts do not persist indefinitely or because one eventually forgets some facts, as one learns new ones. We discuss various ways of obtaining bounded action theories. The main result of the paper is that verification of an expressive class of first-order µ-calculus temporal properties in such theories is in fact decidable.

IJCAI Conference 2011 Conference Paper

A Computationally-Grounded Semantics for Artifact-Centric Systems and Abstraction Results

  • Francesco Belardinelli
  • Alessio Lomuscio
  • Fabio Patrizi

We present a formal investigation of artifact-based systems, a relatively novel framework in service oriented computing, aimed at laying the foundations for verifying these systems through model checking. We present an infinite-state, computationally grounded semantics for these systems that allows us to reason about temporal-epistemic specifications. We present abstraction techniques for the semantics that guarantee transfer of satisfaction from the abstract system to the concrete one.

ICAPS Conference 2011 Conference Paper

An Effective Approach to Realizing Planning Programs

  • Alfonso Emilio Gerevini
  • Fabio Patrizi
  • Alessandro Saetti

Planning programs are loose, high-level, declarative representations of the behavior of agents acting in a domain and following a path of goals to achieve. Such programs are specified through transition systems that can include cycles and decisions to make at certain points. We investigate a new effective approach for solving the problem of realizing a planning program, i. e. , informally, for finding and combining a collection of plans that guarantee the planning program executability. We focus on deterministic domains and propose a general algorithm that solves the problem exploiting a planning technique handling goal constraints and preferences. A preliminary experimental analysis indicates that our approach dramatically outperforms the existing method based on formal verification and synthesis techniques.

IJCAI Conference 2011 Conference Paper

Computing Infinite Plans for LTL Goals Using a Classical Planner

  • Fabio Patrizi
  • Nir Lipovetzky
  • Giuseppe De Giacomo
  • Hector Geffner

Classical planning has been notably successful in synthesizing finite plans to achieve states where propositional goals hold. In the last few years, classical planning has also been extended to incorporate temporally extended goals, expressed in temporal logics such as LTL, to impose restrictions on the state sequences generated by finite plans. In this work, we take the next step and consider the computation of infinite plans for achieving arbitrary LTL goals. We show that infinite plans can also be obtained efficiently by calling a classical planner once over a classical planning encoding that represents and extends the composition of the planning domain and the Buchi automaton representing the goal. This compilation scheme has been implemented and a number of experiments are reported.

AAMAS Conference 2010 Conference Paper

Agent Programming via Planning Programs

  • Guiseppe De Giacomo
  • Fabio Patrizi
  • Sebastian Sardina

We imagine high-level "planning" programs as programs built from achievement and maintenance goals. Their execution requires the ability to meet such goals while respecting program's control flow. The question then is: can we always guarantee the execution of such programs? In this paper, we define the novel planning-programming problem formally, and propose a technique to actually generate a solution by appealing to recent results in LTL-based synthesis of reactive systems.

KR Conference 2010 Conference Paper

Generalized planning with loops under strong fairness constraints

  • Giuseppe De Giacomo
  • Fabio Patrizi
  • Sebastian Sardina

We consider a generalized form of planning, possibly involving loops, that arises in nondeterministic domains when explicit strong fairness constraints are asserted over the planning domain. Such constraints allow us to specify the necessity of occurrence of selected effects of nondeterministic actions over domain’s runs. Also they are particularly meaningful from the technical point of view because they exhibit the expressiveness advantage of LTL over CTL in verification. We show that planning for reachability and maintenance goals is EXPTIME-complete in this setting, that is, it has the same complexity as conditional planning in nondeterministic domains (without strong fairness constraints). We also show that within the EXPTIME bound one can solve the more general problems of realizing agent planning programs as well as composition-based planning in the presence of strong fairness constraints.

AAAI Conference 2010 Conference Paper

Two-Player Game Structures for Generalized Planning and Agent Composition

  • Giuseppe De Giacomo
  • Paolo Felli
  • Fabio Patrizi
  • Sebastian Sardina

In this paper, we review a series of agent behavior synthesis problems under full observability and nondeterminism (partial controllability), ranging from conditional planning, to recently introduced agent planning programs, and to sophisticated forms of agent behavior compositions, and show that all of them can be solved by model checking two-player game structures. These structures are akin to transition systems/Kripke structures, usually adopted in model checking, except that they distinguish (and hence allow to separately quantify) between the actions/moves of two antagonistic players. We show that using them we can implement solvers for several agent behavior synthesis problems.

ICAPS Conference 2009 Conference Paper

Composition of Partially Observable Services Exporting their Behaviour

  • Giuseppe De Giacomo
  • Riccardo De Masellis
  • Fabio Patrizi

In this paper we look at the problem of composing services that export their behavior in terms of a transition system, characterizing the choices of actions given to a client at each point in time. The composition consists of synthesizing an orchestrator that coordinates the available services so as to mimic the desired target service asked by the client. Specifically, in this paper we study the "conformant form" of the problem, where available services are partially controllable and partially observable, and hence, the orchestrator has to make its decisions exploiting the observations made so far only. We give a sound and complete procedure to synthesize the orchestrator in such case, and characterize the computational complexity of the problem. The procedure is based on working with belief (or knowledge) states, a standard technique to tackle conformant planning. Moreover we show that, although in general unavoidable, the powerset construction at the base of the belief state approach can be delegated to the symbolic manipulations of the game-structure model checking tool (TLV), which can be used to efficiently implement the orchestrator synthesis procedure.

KR Conference 2008 Conference Paper

Behavior Composition in the Presence of Failure

  • Sebastian Sardina
  • Fabio Patrizi
  • Giuseppe De Giacomo

In this paper we articulate theoretical bases for robust behavior composition of multiple modules (e. g., agents, devices, etc.) by relying on the formal notion of simulation. Specifically, we consider the problem of synthesizing a fully controllable target behavior from a library of available partially controllable behaviors that are to execute within a shared, fully observable, but partially predictable environment. Both behaviors and environment are represented as finite state transition systems. While previous solutions to this problem assumed full reliability, here we consider unforeseen potential failures, such as a module, or the environment, unexpectedly changes it state; or a module becomes temporarily unavailable or drops out permanently, etc. Based on the notion of simulation, we propose an alternative synthesis approach and show how to refine the solution in hand, either on-the-fly or parsimoniously, so as to cope with failures. Interestingly, it turns out that the proposed simulation-based technique is computationally an improvement over previously known methods which assumed full-reliability.

ECAI Conference 2006 Conference Paper

Evaluating ASP and Commercial Solvers on the CSPLib

  • Marco Cadoli
  • Toni Mancini
  • Davide Micaletto
  • Fabio Patrizi

This paper deals with three solvers for combinatorial problems: the commercial state-of-the-art solver Ilog OPL, and the research ASP systems DLV and SMODELS. The first goal of this research is to evaluate the relative performance of such systems, using a reproducible and extensible experimental methodology. In particular, we consider a third-party problem library, i. e. , the CSPLib, and uniform rules for modelling and selecting instances. The second goal is to analyze the effects of a popular reformulation technique, i. e. , symmetry breaking, and the impact of other modelling aspects, like global constraints and auxiliary predicates. Results show that there is not a single solver winning on all problems, and that reformulation is almost always beneficial: symmetry-breaking may be a good choice, but its complexity has to be carefully chosen, by taking into account also the particular solver used. Global constraints often, but not always, help OPL, and the addition of auxiliary predicates is usually worth, especially when dealing with ASP solvers. Moreover, interesting synergies among the various modelling techniques exist.

v2026.09.13