Arrow Research search

Author name cluster

Giuseppe De Giacomo

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.

164 papers
2 author rows

Possible papers

164

AAAI Conference 2026 Conference Paper

Best-Effort Policies for Robust Markov Decision Processes

  • Alessandro Abate
  • Thom Badings
  • Giuseppe De Giacomo
  • Francesco Fabiano

We study the common generalization of Markov decision processes (MDPs) with sets of transition probabilities, known as robust MDPs (RMDPs). A standard goal in RMDPs is to compute a policy that maximizes the expected return under an adversarial choice of the transition probabilities. If the uncertainty in the probabilities is independent between the states, known as s-rectangularity, such optimal robust policies can be computed efficiently using robust value iteration. However, there might still be multiple optimal robust policies, which, while equivalent with respect to the worst-case, reflect different expected returns under non-adversarial choices of the transition probabilities. Hence, we propose a refined policy selection criterion for RMDPs, drawing inspiration from the notions of dominance and best-effort in game theory. Instead of seeking a policy that only maximizes the worst-case expected return, we additionally require the policy to achieve a maximal expected return under different (i.e., not fully adversarial) transition probabilities. We call such a policy an optimal robust best-effort (ORBE) policy. We prove that ORBE policies always exist, characterize their structure, and present an algorithm to compute them with a manageable overhead over standard robust value iteration. ORBE policies offer a principled tie-breaker among optimal robust policies. Numerical experiments show the feasibility of our approach.

AAAI Conference 2026 Conference Paper

Good-for-MDP State Reduction for Stochastic LTL Planning

  • Christoph Weinhuber
  • Giuseppe De Giacomo
  • Yong Li
  • Sven Schewe
  • Qiyi Tang

We study stochastic planning problems in Markov Decision Processes (MDPs) with goals specified in Linear Temporal Logic (LTL). The state-of-the-art approach transforms LTL formulas into good-for-MDP (GFM) automata, which feature a restricted form of nondeterminism. These automata are then composed with the MDP, allowing the agent to resolve the nondeterminism during policy synthesis. A major factor affecting the scalability of this approach is the size of the generated automata. In this paper, we propose a novel GFM state-space reduction technique that significantly reduces the number of automata states. Our method employs a sophisticated chain of transformations, leveraging recent advances in good-for-games minimisation developed for adversarial settings. In addition to our theoretical contributions, we present empirical results demonstrating the practical effectiveness of our state-reduction technique. Furthermore, we introduce a direct construction method for formulas of the form GFφ, where φ is a co-safety formula. This construction is provably single-exponential in the worst case, in contrast to the general doubly-exponential complexity. Our experiments confirm the scalability advantages of this specialised construction.

KER Journal 2026 Journal Article

Stochastic service composition for ʟᴛʟ<sub><b><i>f</i></b></sub> reachability and safety tasks

  • Giuseppe De Giacomo
  • Marco Favorito
  • Luciana Silo

Service composition à la Roman model consists of realizing a virtual service by suitably orchestrating a set of already available services. In this paper, we consider a variant where available services are stochastic systems, and the target specification is goal-oriented and specified in Linear Temporal Logic on finite traces (ʟᴛʟf). In this setting, we are interested in synthesizing a controller (policy) that maximizes the probability of satisfying the temporal logic objective (either reachability or safety) while minimizing the expected cost of using the available services. To do so, we combine techniques from ʟᴛʟf synthesis, service composition à la Roman Model, and bi-objective lexicographic optimization on Markov Decision Processes (MDPs). This framework has several interesting applications, including Smart Manufacturing and Digital Twins.

AAAI Conference 2026 Conference Paper

Strategic Reasoning over Golog Programs in the Nondeterministic Situation Calculus

  • Giuseppe De Giacomo
  • Yves Lesperance
  • Matteo Mancanelli

We investigate the problem of synthesizing strategies that guarantee the successful execution of a high-level nondeterministic agent program in Golog within a nondeterministic first-order basic action theory, considering the environment as adversarial. Our approach constructs a symbolic program graph that captures the control flow independently of the domain, enabling strategy synthesis through the cross product of the program graph with the domain model. We formally relate graph-based transitions to standard Golog semantics and provide a synthesis procedure that is sound though incomplete (in general, the problem is undecidable, given that we have a first-order representation of the state). We also extend the framework to handle the case where the environment's possible behaviors are specified by a Golog program.

JAAMAS Journal 2025 Journal Article

Behavioral QLTL

  • Giuseppe De Giacomo
  • Giuseppe Perelli

Abstract This paper introduces Behavioral QLTL, a “behavioral” variant of Linear Temporal Logic ( ltl ) with second-order quantifiers. Behavioral qltl is characterized by the fact that the functions that assign the truth value of the quantified propositions along the trace can only depend on the past. In other words, such functions must be “processes” (Abadi et al. , Realizable and Unrealizable Specifications of Reactive Systems, 1989 ). This gives the logic a strategic flavor that we usually associate with planning. Indeed we show that temporally extended planning in nondeterministic domains and ltl synthesis are expressed in Behavioral qltl through formulas with a simple quantification alternation. As such alternation increases, we get to forms of planning/synthesis in which contingent and conformant planning aspects get mixed. We study this logic from the computational point of view and compare it to the original qltl (with non-behavioral semantics) and simpler forms of behavioral semantics.

ECAI Conference 2025 Conference Paper

Do Your Best, but Don't Take Too Many Chances: LTL f Synthesis of Minimal Best-Effort Strategies in FOND Domains

  • Giuseppe De Giacomo
  • Gianmarco Parretti
  • Elisa Santini

Inspired by Joker strategies in games on graphs, we introduce and study the synthesis problem of minimal best-effort strategies for goals expressed in Linear Temporal Logic on Finite Traces (LTLf), assuming that the agent operates in a Fully Observable Nondeterministic (FOND) domain. Minimal best-effort strategies always exist and guarantee that, when a winning strategy does not exist: (i) the agent does its best to achieve its goal; (ii) it relies the least on the environment’s cooperation. We present a game-theoretic algorithm to synthesize minimal best-effort strategies and prove its correctness as well as its optimality (wrt computational complexity). We implemented the algorithm and performed an experimental analysis on scalable benchmarks. The empirical results show that the computation of minimal best-effort strategies is quite efficient: it only requires a small overhead compared to standard best-effort strategies.

KR Conference 2025 Conference Paper

Emerson-Lei and Manna-Pnueli Games for LTLf+ and PPLTL+ Synthesis

  • Daniel Hausmann
  • Shufang Zhu
  • Gianmarco Parretti
  • Christoph Weinhuber
  • Giuseppe De Giacomo
  • Nir Piterman

Recently, the Manna-Pnueli Hierarchy has been used to define the temporal logics LTLf+ and PPLTL+, which allow to use finite-trace LTLf/PPLTL techniques in infinite-trace settings while achieving the expressiveness of full LTL. In this paper, we present the first actual solvers for reactive synthesis in these logics. These are based on games on graphs that leverage DFA-based techniques from LTLf/PPLTL to construct the game arena. We start with a symbolic solver based on Emerson-Lei games, which reduces lower-class properties (guarantee, safety) to higher ones (recurrence, persistence) before solving the game. We then introduce Manna-Pnueli games, which natively embed Manna-Pnueli objectives into the arena. These games are solved by composing solutions to a DAG of simpler Emerson-Lei games, resulting in a provably more efficient approach. We implemented the solvers and practically evaluated their performance on a range of representative formulas. The results show that Manna-Pnueli games often offer significant advantages, though not universally, indicating that combining both approaches could further enhance practical performance.

KR Conference 2025 Conference Paper

LTL Synthesis Under Multi-Agent Environment Assumptions

  • Benjamin Aminof
  • Giuseppe De Giacomo
  • Giuseppe Perelli
  • Sasha Rubin

We investigate LTL synthesis under structured assumptions about the environment. In our setting, the environment is viewed by the protagonist as a collection of peer agents acting together in a shared world. In contrast to the symmetrical frameworks typically studied in multi-agent systems, we take a strikingly asymmetric first-person perspective in which the protagonist ascribes a specification to each of its peer agents and the world, capturing its understanding of their possible strategies. We show that in this setting, LTL synthesis has the same computational complexity as standard LTL synthesis, i. e. , 2EXPTIME-complete. We establish this via a sophisticated, yet fully implementable, argument that builds on the notion of traces compatible with strategies: we use the fact that if the basic specification of the world and of each agent is given in LTL then the sets of traces compatible with the strategies describing the behaviors of the agents are omega-regular. This enables the use of word-automata rather than the more complicated tree-automata.

AAAI Conference 2025 Conference Paper

LTLf Synthesis Under Unreliable Input

  • Christian Hagemeier
  • Giuseppe De Giacomo
  • Moshe Y. Vardi

We study the problem of realizing strategies for an LTLf goal specification while ensuring that at least an LTLf backup specification is satisfied in case of unreliability of certain input variables. We formally define the problem and characterize its worst-case complexity as 2EXPTIME-complete, like standard LTLf synthesis. Then we devise three different solution techniques: one based on direct automata manipulation, which is 2EXPTIME, one disregarding unreliable input variables by adopting a belief construction, which is 3EXPTIME, and one leveraging second-order quantified LTLf (QLTLf), which is 2EXPTIME and allows for a direct encoding into monadic second-order logic, which in turn is worst-case nonelementary. We prove their correctness and evaluate them against each other empirically. Interestingly, theoretical worst-case bounds do not translate into observed performance; the MSO technique performs best, followed by belief construction and direct automata manipulation. As a byproduct of our study, we provide a general synthesis procedure for arbitrary QLTLf specifications.

IJCAI Conference 2025 Conference Paper

LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces

  • Benjamin Aminof
  • Giuseppe De Giacomo
  • Sasha Rubin
  • Moshe Y. Vardi

We study two logics, LTLf+ and PPLTL+, to express properties of infinite traces, that are based on the linear-time temporal logics LTLf and PPLTL on finite traces. LTLf+/PPLTL+ use levels of Manna and Pnueli’s LTL safety-progress hierarchy, and thus have the same expressive power as LTL. However, they also retain a crucial characteristic of reactive synthesis for the base logics: the game arena for strategy extraction can be derived from deterministic finite automata (DFA). Consequently, these logics circumvent the notorious difficulties associated with determinizing infinite trace automata, typical of LTL synthesis. We present optimal DFA-based technique for solving reactive synthesis for LTLf+ and PPLTL+. Additionally, we adapt these algorithms to optimally solve satisfiability and model-checking for these two logics.

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.

TIME Conference 2025 Conference Paper

PDDL to DFA: A Symbolic Transformation for Effective Reasoning

  • Giuseppe De Giacomo
  • Antonio Di Stasio 0001
  • Gianmarco Parretti

ltl_f reactive synthesis under environment specifications, which concerns the automated generation of strategies enforcing logical specifications, has emerged as a powerful technique for developing autonomous AI systems. It shares many similarities with Fully Observable Nondeterministic (fond) planning. In particular, nondeterministic domains can be expressed as ltl_f environment specifications. However, this is not needed since nondeterministic domains can be transformed into deterministic finite-state automata (dfa) to be used directly in the synthesis process. In this paper, we present a practical symbolic technique for translating domains expressed in Planning Domain Definition Language (pddl) into dfas. The technique allows for the integration of the planning domain, reduced to dfa in a symbolic form, into current symbolic ltl_f synthesis tools. We implemented our technique in a new tool, pddl2dfa, and applied it to solve fond planning by using state-of-the-art reactive synthesis techniques in a tool called syft4fond. Our empirical results confirm the effectiveness of our approach.

IJCAI Conference 2025 Conference Paper

Responsibility Anticipation and Attribution in LTLf

  • Giuseppe De Giacomo
  • Emiliano Lorini
  • Timothy Parker
  • Gianmarco Parretti

Responsibility is one of the key notions in machine ethics and in the area of autonomous systems. It is a multi-faceted notion involving counterfactual reasoning about actions and strategies. In this paper, we study different variants of responsibility for LTLf outcomes based on strategic reasoning. We show a connection with notions in reactive synthesis, including the synthesis of winning, dominant, and best-effort strategies. This connection provides a strong computational grounding of responsibility, allowing us to characterize the worst-case computa- tional complexity and devise sound, complete, and optimal algorithms for anticipating and attributing responsibility.

AAAI Conference 2025 Conference Paper

Situation Calculus Temporally Lifted Abstractions for Generalized Planning

  • Giuseppe De Giacomo
  • Yves Lespérance
  • Matteo Mancanelli

We present a new formal framework for generalized planning (GP) based on the situation calculus extended with LTL constraints. The GP problem is specified by a first-order basic action theory whose models are the problem instances. This low-level theory is then abstracted into a high-level propositional nondeterministic basic action theory with a single model. A refinement mapping relates the two theories. LTL formulas are used to specify the temporally extended goals as well as assumed trace constraints. If all LTL trace constraints hold at the low level and the high-level model can simulate all the low-level models with respect to the mapping, we say that we have a temporally lifted abstraction. We prove that if we have such an abstraction and the agent has a strategy to achieve a LTL goal under some trace constraints at the abstract level, then there exists a refinement of the strategy to achieve the refinement of the goal at the concrete level. We use LTL synthesis to generate the strategy at the abstract level. We illustrate our approach by synthesizing a program that solves a data structure manipulation problem.

IJCAI Conference 2025 Conference Paper

Solving MDPs with LTLf+ and PPLTL+ Temporal Objectives

  • Giuseppe De Giacomo
  • Yong Li
  • Sven Schewe
  • Christoph Weinhuber
  • Pian Yu

The temporal logics LTLf+ and PPLTL+ have recently been introduced to express objectives over infinite traces. These logics are appealing because they match the expressive power of LTL on infinite traces while enabling efficient DFA-based techniques, which have been crucial to the scalability of reactive synthesis and adversarial planning in LTLf and PPLTL over finite traces. In this paper, we demonstrate that these logics are also highly effective in the context of MDPs. Introducing a technique tailored for probabilistic systems, we leverage the benefits of efficient DFA-based methods and compositionality. This approach is simpler than its nonprobabilistic counterparts in reactive synthesis and adversarial planning, as it accommodates a controlled form of nondeterminism ("good for MDPs") in the automata when transitioning from finite to infinite traces. Notably, by exploiting compositionality, our solution is both implementation-friendly and well-suited for straightforward symbolic implementations.

AAAI Conference 2024 Conference Paper

Abstraction of Situation Calculus Concurrent Game Structures

  • Yves Lesperance
  • Giuseppe De Giacomo
  • Maryam Rostamigiv
  • Shakil M. Khan

We present a general framework for abstracting agent behavior in multi-agent synchronous games in the situation calculus, which provides a first-order representation of the state and allows us to model how plays depend on the data and objects involved. We represent such games as action theories of a special form called situation calculus synchronous game structures (SCSGSs), in which we have a single action "tick" whose effects depend on the combination of moves selected by the players. In our framework, one specifies both an abstract SCSGS and a concrete SCSGS, as well as a refinement mapping that specifies how each abstract move is implemented by a Golog program defined over the concrete SCSGS. We define notions of sound and complete abstraction with respect to a mapping over such SCSGS. To express strategic properties on the abstract and concrete games we adopt a first-order variant of alternating-time mu-calculus mu-ATL-FO. We show that we can exploit abstraction in verifying mu-ATL-FO properties of SCSGSs under the assumption that agents can always execute abstract moves to completion even if not fully controlling their outcomes.

IJCAI Conference 2024 Conference Paper

Effective Approach to LTLf Best-Effort Synthesis in Multi-Tier Environments

  • Benjamin Aminof
  • Giuseppe De Giacomo
  • Gianmarco Parretti
  • Sasha Rubin

We consider an agent acting in a complex environment modeled through a multi-tiered specification, in which each tier adds nondeterminism in the environment response to the agent actions. In this setting, we devise an effective approach to best-effort synthesis, i. e. , synthesizing agent strategies that win against a maximal set of possible environment responses in each tier. We do this in a setting where both the multi-tier environment and agent goal are specified in the linear temporal logic on finite traces (LTLf). While theoretical solution techniques based on automata on infinite trees have been developed previously, we completely side-step them here and focus on a DFA-based game-theoretic technique, which can be effectively implemented symbolically. Specifically, we present a provably correct algorithm that is based on solving separately DFA-based games for each tier and then combining the obtained solutions on-the-fly. This algorithm is linear, as opposed to being exponential, in the number of tiers and thus, it can graciously handle multi-tier environments formed of several tiers.

IJCAI Conference 2024 Conference Paper

Lifted Planning: Recent Advances in Planning Using First-Order Representations

  • Augusto B. Corrêa
  • Giuseppe De Giacomo

Lifted planning is usually defined as planning directly over a first-order representation. From the mid-1990s until the late 2010s, lifted planning was sidelined, as most of the state-of-the-art planners first ground the task and then solve it using a propositional representation. Moreover, it was unclear whether lifted planners could scale. But as planning problems become harder, they also become infeasible to ground. Recently, lifted planners came back into play, aiming at problems where grounding is a bottleneck. In this work, we survey recent advances in lifted planning. The main techniques rely either on state-space search or logic satisfiability. For lifted search-based planners, we show the direct connections to other areas of computer science, such as constraint satisfaction problems and databases. For lifted planners based on satisfiability, the advances in modeling are crucial to their scalability. We briefly describe the main planners available in the literature and their techniques.

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.

IJCAI Conference 2024 Conference Paper

Planning for Temporally Extended Goals in Pure-Past Linear Temporal Logic (Extended Abstract)

  • Luigi Bonassi
  • Giuseppe De Giacomo
  • Marco Favorito
  • Francesco Fuggitti
  • Alfonso Emilio Gerevini
  • Enrico Scala

We study classical planning for temporally extended goals expressed in Pure-Past Linear Temporal Logic (PPLTL). PPLTL is as expressive as Linear-time Temporal Logic on finite traces (LTLf), but as shown in this paper, it is computationally much better behaved for planning. Specifically, we show that planning for PPLTL goals can be encoded into classical planning with minimal overhead, introducing only a number of new fluents that is at most linear in the PPLTL goal and no spurious additional actions. Based on these results, we implemented a system called Plan4Past, which can be used along with state-of-the-art classical planners, such as LAMA. An empirical analysis demonstrates the practical effectiveness of Plan4Past, showing that a classical planner generally performs better with our compilation than with other existing compilations for LTLf goals over the considered benchmarks.

ICAPS Conference 2024 Conference Paper

Planning with Object Creation

  • Augusto B. Corrêa
  • Giuseppe De Giacomo
  • Malte Helmert
  • Sasha Rubin

Classical planning problems are defined using some specification language, such as PDDL. The domain expert defines action schemas, objects, the initial state, and the goal. One key aspect of PDDL is that the set of objects cannot be modified during plan execution. While this is fine in many domains, sometimes it makes modeling more complicated. This may impact the performance of planners, and it requires the domain expert to bound the number of required objects beforehand, which can be a challenge. We introduce an extension to the classical planning formalism, where action effects can create and remove objects. This problem is semi-decidable, but it becomes decidable if we can bound the number of objects in any given state, even though the state space is still infinite. On the practical side, we extend the Powerlifted planning system to support this PDDL extension. Our results show that this extension improves the performance of Powerlifted while supporting more natural PDDL models.

KR Conference 2024 Conference Paper

Proper Linear-time Specifications of Environment Behaviors in Nondeterministic Planning and Reactive Synthesis

  • Benjamin Aminof
  • Giuseppe De Giacomo
  • Sasha Rubin
  • Florian Zuleger

To help it achieve its goal, an agent exploits assumptions it has about the behavior of its environment. The common view in planning and reactive synthesis is that such assumptions are sets of traces. This trace-centric view has the advantage of having well-understood specification formalisms, such as linear-time temporal logic. An alternative view, that we have promoted as being conceptually superior, is strategy-centric: assumptions are non-empty sets of environment strategies. In this work we relate these views and show that the strategy-centric view is a refinement of the trace-centric view. We thus address the following fundamental question: when should a set of traces be considered an assumption that the agent has about the environment's behavior? Our answer is in terms of coverability: every trace in the set should be consistent with some environment strategy that enforces it. We call such sets ``proper environment specifications''. Typical examples are given by (the traces consistent with a given) planning domain, and fairness constraints, but not arbitrary trace constraints. We provide an algorithm that, given a specification in linear-time temporal logic (LTL) decides whether or not it is a proper environment specification. Furthermore, we show that every set of traces has a ``proper environment core'', which excludes traces that the agent can ignore when devising its plan. We provide an algorithm for computing a representation of the core of an LTL formula, and prove that the core of an LTL-definable property is itself LTL-definable.

AAAI Conference 2024 Conference Paper

Pure-Past Action Masking

  • Giovanni Varricchione
  • Natasha Alechina
  • Mehdi Dastani
  • Giuseppe De Giacomo
  • Brian Logan
  • Giuseppe Perelli

We present Pure-Past Action Masking (PPAM), a lightweight approach to action masking for safe reinforcement learning. In PPAM, actions are disallowed (“masked”) according to specifications expressed in Pure-Past Linear Temporal Logic (PPLTL). PPAM can enforce non-Markovian constraints, i.e., constraints based on the history of the system, rather than just the current state of the (possibly hidden) MDP. The features used in the safety constraint need not be the same as those used by the learning agent, allowing a clear separation of concerns between the safety constraints and reward specifications of the (learning) agent. We prove formally that an agent trained with PPAM can learn any optimal policy that satisfies the safety constraints, and that they are as expressive as shields, another approach to enforce non-Markovian constraints in RL. Finally, we provide empirical results showing how PPAM can guarantee constraint satisfaction in practice.

ECAI Conference 2024 Conference Paper

Shielded FOND: Planning with Safety Constraints in Pure-Past Linear Temporal Logic

  • Luigi Bonassi
  • Giuseppe De Giacomo
  • Alfonso Emilio Gerevini
  • Enrico Scala

In this paper, we introduce Shielded FOND planning (S-FOND), which is the problem of computing a strategy to reach a final-state goal while preserving a safety specification called shield. In particular, we characterize shields as Pure-Past Linear Temporal Logic formulas that must hold in every prefix of a state trace induced by a solution strategy, thus capturing the whole safety fragment of Linear Temporal Logic formulas over finite traces. We propose three solution encodings for handling S-FOND problems: the first, which is our baseline, simply views a shield as a temporally extended goal; the second, instead, blocks the execution of further actions when the shield gets violated, and the third prevents the execution of actions that could violate the shield by using the notion of regression. We formally prove the correctness of each encoding and experimentally prove their effectiveness over a set of benchmark shields.

IJCAI Conference 2024 Conference Paper

The Trembling-Hand Problem for LTLf Planning

  • Pian Yu
  • Shufang Zhu
  • Giuseppe De Giacomo
  • Marta Kwiatkowska
  • Moshe Vardi

Consider an agent acting to achieve its temporal goal, but with a ``trembling hand". In this case, the agent may mistakenly instruct, with a certain (typically small) probability, actions that are not intended due to faults or imprecision in its action selection mechanism, thereby leading to possible goal failure. We study the trembling-hand problem in the context of reasoning about actions and planning for temporally extended goals expressed in Linear Temporal Logic on finite traces (LTLf), where we want to synthesize a strategy (aka plan) that maximizes the probability of satisfying the LTLf goal in spite of the trembling hand. We consider both deterministic and nondeterministic (adversarial) domains. We propose solution techniques for both cases by relying respectively on Markov Decision Processes and on Markov Decision Processes with Set-valued Transitions with LTLf objectives, where the set-valued probabilistic transitions capture both the nondeterminism from the environment and the possible action instruction errors from the agent. We formally show the correctness of our solution techniques and demonstrate their effectiveness experimentally through a proof-of-concept implementation.

IJCAI Conference 2023 Conference Paper

Abstraction of Nondeterministic Situation Calculus Action Theories

  • Bita Banihashemi
  • Giuseppe De Giacomo
  • Yves Lesperance

We develop a general framework for abstracting the behavior of an agent that operates in a nondeterministic domain, i. e. , where the agent does not control the outcome of the nondeterministic actions, based on the nondeterministic situation calculus and the ConGolog programming language. We assume that we have both an abstract and a concrete nondeterministic basic action theory, and a refinement mapping which specifies how abstract actions, decomposed into agent actions and environment reactions, are implemented by concrete ConGolog programs. This new setting supports strategic reasoning and strategy synthesis, by allowing us to quantify separately on agent actions and environment reactions. We show that if the agent has a (strong FOND) plan/strategy to achieve a goal/complete a task at the abstract level, and it can always execute the nondeterministic abstract actions to completion at the concrete level, then there exist a refinement of it that is a (strong FOND) plan/strategy to achieve the refinement of the goal/task at the concrete level.

AAAI Conference 2023 Conference Paper

Automata Cascades: Expressivity and Sample Complexity

  • Alessandro Ronca
  • Nadezda Alexandrovna Knorozova
  • Giuseppe De Giacomo

Every automaton can be decomposed into a cascade of basic prime automata. This is the Prime Decomposition Theorem by Krohn and Rhodes. Guided by this theory, we propose automata cascades as a structured, modular, way to describe automata as complex systems made of many components, each implementing a specific functionality. Any automaton can serve as a component; using specific components allows for a fine-grained control of the expressivity of the resulting class of automata; using prime automata as components implies specific expressivity guarantees. Moreover, specifying automata as cascades allows for describing the sample complexity of automata in terms of their components. We show that the sample complexity is linear in the number of components and the maximum complexity of a single component, modulo logarithmic factors. This opens to the possibility of learning automata representing large dynamical systems consisting of many parts interacting with each other. It is in sharp contrast with the established understanding of the sample complexity of automata, described in terms of the overall number of states and input letters, which implies that it is only possible to learn automata where the number of states is linear in the amount of data available. Instead our results show that one can learn automata with a number of states that is exponential in the amount of data available.

EUMAS Conference 2023 Conference Paper

Behavioral QLTL

  • Giuseppe De Giacomo
  • Giuseppe Perelli

Abstract This paper introduces Behavioral QLTL, a “behavioral” variant of Linear Temporal Logic ( ltl ) with second-order quantifiers. Behavioral qltl is characterized by the fact that the functions that assign the truth value of the quantified propositions along the trace can only depend on the past. In other words, such functions must be “processes” [ 1 ]. This gives the logic a strategic flavor that we usually associate with planning. Indeed we show that temporally extended planning in nondeterministic domains and ltl synthesis are expressed in Behavioral qltl through formulas with a simple quantification alternation. While as this alternation increases, we get to forms of planning/synthesis in which contingent and conformant planning aspects get mixed. We study this logic from the computational point of view and compare it to the original qltl (with non-behavioral semantics) and simpler forms of behavioral semantics.

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.

ECAI Conference 2023 Conference Paper

FOND Planning for Pure-Past Linear Temporal Logic Goals

  • Luigi Bonassi
  • Giuseppe De Giacomo
  • Marco Favorito
  • Francesco Fuggitti
  • Alfonso Emilio Gerevini
  • Enrico Scala

Recently, Pure-Past Temporal Logic (PPLTL) has proven highly effective in specifying temporally extended goals in deterministic planning domains. In this paper, we show its effectiveness also for fully observable nondeterministic (FOND) planning, both for strong and strong-cyclic plans. We present a notably simple encoding of FOND planning for PPLTL goals into standard FOND planning for final-state goals. The encoding only introduces few fluents (at most linear in the PPLTL goal) without adding any spurious action and allows planners to lazily build the relevant part of the deterministic automaton for the goal formula on-the-fly during the search. We formally prove its correctness, implement it in a tool called Plan4Past, and experimentally show its practical effectiveness.

KR Conference 2023 Conference Paper

Grounding LTLf Specifications in Image Sequences

  • Elena Umili
  • Roberto Capobianco
  • Giuseppe De Giacomo

A critical challenge in neuro-symbolic (NeSy) approaches is to handle the symbol grounding problem without direct supervision. That is mapping high-dimensional raw data into an interpretation over a finite set of abstract concepts with a known meaning, without using labels. In this work, we ground symbols into sequences of images by exploiting symbolic logical knowledge in the form of Linear Temporal Logic over finite traces (LTLf) formulas, and sequence-level labels expressing if a sequence of images is compliant or not with the given formula. Our approach is based on translating the LTLf formula into an equivalent deterministic finite automaton (DFA) and interpreting the latter in fuzzy logic. Experiments show that our system outperforms recurrent neural networks in sequence classification and can reach high image classification accuracy without being trained with any single-image label.

ECAI Conference 2023 Conference Paper

LTL f Best-Effort Synthesis in Nondeterministic Planning Domains

  • Giuseppe De Giacomo
  • Gianmarco Parretti
  • Shufang Zhu 0001

We study best-effort strategies (aka plans) in fully observable nondeterministic domains (FOND) for goals expressed in Linear Temporal Logic on Finite Traces (LTLf). The notion of best-effort strategy has been introduced to also deal with the scenario when no agent strategy exists that fulfills the goal against every possible nondeterministic environment reaction. Such strategies fulfill the goal if possible, and do their best to do so otherwise. We present a game-theoretic technique for synthesizing best-effort strategies that exploit the specificity of nondeterministic planning domains. We formally show its correctness and demonstrate its effectiveness experimentally, exhibiting a much greater scalability with respect to a direct best-effort synthesis approach based on re-expressing the planning domain as generic environment specifications.

LAMAS&SR Workshop 2023 Workshop Paper

LTLf Synthesis Under Environment Specifications for Reachability and Safety Properties

  • Benjamin Aminof
  • Giuseppe De Giacomo
  • Antonio Di Stasio
  • Hugo Francon
  • Sasha Rubin
  • Shufang Zhu

In this paper, we study LTLf synthesis under environment specifications for arbitrary reachability and safety properties. We consider both kinds of properties for both agent tasks and environment specifications, providing a complete landscape of synthesis algorithms. For each case, we devise a specific algorithm (optimal wrt complexity of the problem) and prove its correctness. All these algorithms adopt some common building blocks, though combining them in different ways. While some cases are already studied in literature others are studied here for the first time.

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.

ICAPS Conference 2023 Conference Paper

Planning for Temporally Extended Goals in Pure-Past Linear Temporal Logic

  • Luigi Bonassi
  • Giuseppe De Giacomo
  • Marco Favorito
  • Francesco Fuggitti
  • Alfonso Emilio Gerevini
  • Enrico Scala

We study classical planning for temporally extended goals expressed in Pure-Past Linear Temporal Logic (PPLTL). PPLTL is as expressive as Linear-time Temporal Logic on finite traces (LTLf), but as shown in this paper, it is computationally much better behaved for planning. Specifically, we show that planning for PPLTL goals can be encoded into classical planning with minimal overhead, introducing only a number of new fluents that is at most linear in the PPLTL goal and no spurious additional actions. Based on these results, we implemented a system called Plan4Past, which can be used along with state-of-the-art classical planners, such as LAMA. An empirical analysis demonstrates the practical effectiveness of Plan4Past, showing that a classical planner generally performs better with our compilation than with other existing compilations for LTLf goals over the considered benchmarks.

PRL Workshop 2023 Workshop Paper

Preemptive Restraining Bolts

  • Giovanni Varricchione
  • Natasha Alechina
  • Mehdi Dastani
  • Giuseppe De Giacomo
  • Brian Logan
  • Giuseppe Perelli

We present preemptive restraining bolts (PRBs), a new approach to safe reinforcement learning which uses non-Markovian action masking, i.e., actions are masked (disallowed) based on the history of the system, rather than just the current state. PRBs are expressed in Pure Past Linear Temporal Logic and have minimal overhead (linear in the size of the state) compared to Markovian action masking, while having the same expressive power as other non-Markovian approaches such as shields (that can express any safety Linear Temporal Logic property). As with restraining bolts, the language in which safety properties are expressed does not have to be the same as the language specifying the features of the state for the learning agent. Critically, PRBs can be applied in the learning process to learn an optimal safe policy while using only safe actions during learning. As a result, PRBs can be used to provide general safety guarantees, without compromising efficiency.

AAAI Conference 2023 Conference Paper

Reactive Synthesis of Dominant Strategies

  • Benjamin Aminof
  • Giuseppe De Giacomo
  • Sasha Rubin

We study the synthesis under environment specifications problem for LTL/LTLf which, in particular, generalizes FOND (strong) planning with these temporal goals. We consider the case where the agent cannot enforce its goal --- for which the argument for using best-effort strategies has been made --- and study the intermediate ground, between enforcing and best-effort strategies, of dominant strategies. Intuitively, such strategies achieve the goal against any environment for which it is achievable. We show that dominant strategies may exist when enforcing ones do not, while still sharing with the latter many desirable properties such as being interchangeable with each other, and being monotone with respect to tightening of environment specifications. We give necessary and sufficient conditions for the existence of dominant strategies, and show that deciding if they exist is 2EXPTIME-complete --- the same as for enforcing strategies. Finally, we give a uniform, optimal, game-theoretic algorithm for simultaneously solving the three synthesis problems of enforcing, dominant, and best-effort strategies.

EUMAS Conference 2023 Conference Paper

sc ltl f Synthesis Under Environment Specifications for Reachability and Safety Properties

  • Benjamin Aminof
  • Giuseppe De Giacomo
  • Antonio Di Stasio 0001
  • Hugo Francon
  • Sasha Rubin
  • Shufang Zhu 0001

Abstract In this paper, we study \({\textsc {ltl}}_f\) synthesis under environment specifications for arbitrary reachability and safety properties. We consider both kinds of properties for both agent tasks and environment specifications, providing a complete landscape of synthesis algorithms. For each case, we devise a specific algorithm (optimal wrt complexity of the problem) and prove its correctness. The algorithms combine common building blocks in different ways. While some cases are already studied in literature others are studied here for the first time.

EUMAS Conference 2023 Conference Paper

Symbolic sc ltl f Best-Effort Synthesis

  • Giuseppe De Giacomo
  • Gianmarco Parretti
  • Shufang Zhu 0001

Abstract We consider an agent acting to fulfil tasks in a nondeterministic environment. When a strategy that fulfills the task regardless of how the environment acts does not exist, the agent should at least avoid adopting strategies that prevent from fulfilling its task. Best-effort synthesis captures this intuition. In this paper, we devise and compare various symbolic approaches for best-effort synthesis in Linear Temporal Logic on finite traces ( \(\textsc {ltl}_f\) ). These approaches are based on the same basic components, however they change in how these components are combined, and this has a significant impact on the performance of the approaches as confirmed by our empirical evaluations.

KR Conference 2022 Conference Paper

Act for Your Duties but Maintain Your Rights

  • Shufang Zhu
  • Giuseppe De Giacomo

Most of the synthesis literature has focused on studying how to synthesize a strategy to fulfill a task. This task is a duty for the agent. In this paper, we argue that intelligent agents should also be equipped with rights, that is, tasks that the agent itself can choose to fulfill (e. g. , the right of recharging the battery). The agent should be able to maintain these rights while acting for its duties. We study this issue in the context of LTLf synthesis: we give duties and rights in terms of LTLf specifications, and synthesize a suitable strategy to achieve the duties that can be modified on-the-fly to achieve also the rights, if the agent chooses to do so. We show that handling rights does not make synthesis substantially more difficult, although it requires a more sophisticated solution concept than standard LTLf synthesis. We also extend our results to the case in which further duties and rights are given to the agent while already executing.

KR Conference 2022 Conference Paper

Automatic Synthesis of Dynamic Norms for Multi-Agent Systems

  • Natasha Alechina
  • Giuseppe De Giacomo
  • Brian Logan
  • Giuseppe Perelli

Norms have been widely proposed to coordinate and regulate multi-agent systems (MAS) behaviour. We consider the problem of synthesising and revising the set of norms in a normative MAS to satisfy a design objective expressed in Alternating Time Temporal Logic (ATL*). ATL* is a well-established language for strategic reasoning, which allows the specification of norms that constrain the strategic behaviour of agents. We focus on dynamic norms, that is, norms corresponding to Mealy machines, that allow us to place different constraints on the agents' behaviour depending on the state of the norm and the state of the underlying MAS. We show that synthesising dynamic norms is (k + 1)-EXPTIME, where k is the alternation depth of quantifiers in the ATL* specification. Note that for typical cases of interest, k is either 1 or 2. We also study the problem of removing existing norms to satisfy a new objective, which we show to be 2EXPTIME-complete.

IJCAI Conference 2022 Conference Paper

Beyond Strong-Cyclic: Doing Your Best in Stochastic Environments

  • Benjamin Aminof
  • Giuseppe De Giacomo
  • Sasha Rubin
  • Florian Zuleger

``Strong-cyclic policies" were introduced to formalize trial-and-error strategies and are known to work in Markovian stochastic domains, i. e. , they guarantee that the goal is reached with probability 1. We introduce ``best-effort" policies for (not necessarily Markovian) stochastic domains. These generalize strong-cyclic policies by taking advantage of stochasticity even if the goal cannot be reached with probability 1. We compare such policies with optimal policies, i. e. , policies that maximize the probability that the goal is achieved, and show that optimal policies are best-effort, but that the converse is false in general. With this framework at hand, we revisit the foundational problem of what it means to plan in nondeterministic domains when the nondeterminism has a stochastic nature. We show that one can view a nondeterministic planning domain as a representation of infinitely many stochastic domains with the same support but different probabilities, and that for temporally extended goals expressed in LTL/LTLf a finite-state best-effort policy in one of these domains is best-effort in each of the domains. In particular, this gives an approach for finding such policies that reduces to solving finite-state MDPs with LTL/LTLf goals. All this shows that ``best-effort" policies are robust to changes in the probabilities, as long as the support is unchanged.

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.

PRL Workshop 2022 Workshop Paper

Graph-Based Representation of Automata Cascades with an Application to Regular Decision Processes

  • Alessandro Ronca
  • Giuseppe De Giacomo

Cascades allow for expressing any automaton as the composition of some basic automata of a restricted number of kinds. Cascades can be constructed in a completely incremental way, by adding one component at a time. Adding a new automaton amounts to a refinement of the previous cascade. The complexity of the phenomena described by a cascade increases greatly with the number of components because each new automaton has access to the states of the previous automata. Furthermore, components are taken from some wellidentified classes of basic automata. We believe such characteristics are of great value. However, the potential of cascades is blocked by the lack of an appropriate representation formalism. We present a graph-based formalism to represent automata cascades, and we demonstrate its effectiveness through an application in Regular Decision Processes, where automata are employed to capture temporal dependencies in the dynamics of a domain.

NeSy Conference 2022 Conference Paper

Grounding LTLf Specifications in Images

  • Elena Umili
  • Roberto Capobianco
  • Giuseppe De Giacomo

A critical challenge in neurosymbolic approaches is to handle the symbol grounding problem without direct supervision. That is mapping high-dimensional raw data into an interpretation over a finite set of abstract concepts with a known meaning, without using labels. In this work, we ground symbols into sequences of images by exploiting symbolic logical knowledge in the form of Linear Temporal Logic over finite traces (LTLf) formulas, and sequence-level labels expressing if a sequence of images is compliant or not with the given formula. Our approach is based on translating the LTLf formula into an equivalent deterministic finite automaton (DFA) and interpreting the latter in fuzzy logic. Experiments show that our system outperforms recurrent neural networks in sequence classification and can reach high image classification accuracy without being trained with any single-image label.

ICAPS Conference 2022 Conference Paper

Iterative Depth-First Search for FOND Planning

  • Ramon Fraga Pereira
  • André Grahl Pereira
  • Frederico Messa
  • Giuseppe De Giacomo

Fully Observable Non-Deterministic (FOND) planning models uncertainty through actions with non-deterministic effects. Existing FOND planning algorithms are effective and employ a wide range of techniques. However, most of the existing algorithms are not robust for dealing with both non-determinism and task size. In this paper, we develop a novel iterative depth-first search algorithm that solves FOND planning tasks and produces strong cyclic policies. Our algorithm is explicitly designed for FOND planning, addressing more directly the non-deterministic aspect of FOND planning, and it also exploits the benefits of heuristic functions to make the algorithm more effective during the iterative searching process. We compare our proposed algorithm to well-known FOND planners, and show that it has robust performance over several distinct types of FOND domains considering different metrics.

IJCAI Conference 2022 Conference Paper

LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work

  • Giuseppe De Giacomo
  • Marco Favorito
  • Jianwen Li
  • Moshe Y. Vardi
  • Shengping Xiao
  • Shufang Zhu

Synthesis techniques for temporal logic specifications are typically based on exploiting symbolic techniques, as done in model checking. These symbolic techniques typically use backward fixpoint computation. Planning, which can be seen as a specific form of synthesis, is a witness of the success of forward search approaches. In this paper, we develop a forward-search approach to full-fledged Linear Temporal Logic on finite traces (LTLf) synthesis. We show how to compute the Deterministic Finite Automaton (DFA) of an LTLf formula on-the-fly, while performing an adversarial forward search towards the final states, by considering the DFA as a sort of AND-OR graph. Our approach is characterized by branching on suitable propositional formulas, instead of individual evaluations, hence radically reducing the branching factor of the search space. Specifically, we take advantage of techniques developed for knowledge compilation, such as Sentential Decision Diagrams (SDDs), to implement the approach efficiently.

IJCAI Conference 2022 Conference Paper

Markov Abstractions for PAC Reinforcement Learning in Non-Markov Decision Processes

  • Alessandro Ronca
  • Gabriel Paludo Licks
  • Giuseppe De Giacomo

Our work aims at developing reinforcement learning algorithms that do not rely on the Markov assumption. We consider the class of Non-Markov Decision Processes where histories can be abstracted into a finite set of states while preserving the dynamics. We call it a Markov abstraction since it induces a Markov Decision Process over a set of states that encode the non-Markov dynamics. This phenomenon underlies the recently introduced Regular Decision Processes (as well as POMDPs where only a finite number of belief states is reachable). In all such kinds of decision process, an agent that uses a Markov abstraction can rely on the Markov property to achieve optimal behaviour. We show that Markov abstractions can be learned during reinforcement learning. Our approach combines automata learning and classic reinforcement learning. For these two tasks, standard algorithms can be employed. We show that our approach has PAC guarantees when the employed algorithms have PAC guarantees, and we also provide an experimental evaluation.

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

Synthesis of Maximally Permissive Strategies for LTLf Specifications

  • Shufang Zhu
  • Giuseppe De Giacomo

In this paper, we study synthesis of maximally permissive strategies for Linear Temporal Logic on finite traces (LTLf) specifications. That is, instead of computing a single strategy (aka plan, or policy), we aim at computing the entire set of strategies at once and then choosing among them while in execution, without committing to a single one beforehand. Maximally permissive strategies have been introduced and investigated for safety properties, especially in the context of Discrete Event Control Theory. However, the available results for safety properties do not apply to reachability properties (eventually reach a given state of affair) nor to LTLf properties in general. In this paper, we show that maximally permissive strategies do exist also for reachability and general LTLf properties, and can in fact be computed with minimal overhead wrt the computation of a single strategy using state-of-the-art tools.

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.

IJCAI Conference 2021 Conference Paper

Best-Effort Synthesis: Doing Your Best Is Not Harder Than Giving Up

  • Benjamin Aminof
  • Giuseppe De Giacomo
  • Sasha Rubin

We study best-effort synthesis under environment assumptions specified in LTL, and show that this problem has exactly the same computational complexity of standard LTL synthesis: 2EXPTIME-complete. We provide optimal algorithms for computing best-effort strategies, both in the case of LTL over infinite traces and LTL over finite traces (i. e. , LTLf). The latter are particularly well suited for implementation.

ICAPS Conference 2021 Conference Paper

Compositional Approach to Translate LTLf/LDLf into Deterministic Finite Automata

  • Giuseppe De Giacomo
  • Marco Favorito

The translation from temporal logics to automata is the workhorse algorithm of several techniques in computer science and AI, such as reactive synthesis, reasoning about actions, FOND planning with temporal specifications, and reinforcement learning with non-Markovian rewards, to name a few. Unfortunately, the problem is computationally intractable, requiring the implementation of several heuristics to make it usable in practice. In this paper, following the recent interest in temporal logic formalisms over finite traces, we present a compositional approach for dealing with translations of Linear Temporal Logic (LTLf) and Linear Dynamic Logic (LDLf) on finite traces into Deterministic Finite Automata (DFA). We inductively transform each LTLf/LDLf subformula into a DFA and combine them through automata operators. By relying on efficient semi-symbolic automata representations, we empirically show our approach's effectiveness and competitiveness with similar tools. Moreover, this is the first work that provides a scalable and practical tool supporting the translation to DFA not only for LTLf but also for full LDLf.

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.

PRL Workshop 2021 Workshop Paper

Efficient PAC Reinforcement Learning in Regular Decision Processes

  • Alessandro Ronca
  • Giuseppe De Giacomo

Recently regular decision processes have been proposed as a well-behaved form of non-Markov decision process. Regular decision processes are characterised by a transition function and a reward function that depend on the whole history, though regularly (as in regular languages). In practice both the transition and the reward functions can be seen as finite transducers. We study reinforcement learning in regular decision processes. Our main contribution is to show that a near-optimal policy can be PAC-learned in polynomial time in a set of parameters that describe the underlying decision process. We argue that the identified set of parameters is minimal and it reasonably captures the difficulty of a regular decision process.

IJCAI Conference 2021 Conference Paper

Efficient PAC Reinforcement Learning in Regular Decision Processes

  • Alessandro Ronca
  • Giuseppe De Giacomo

Recently regular decision processes have been proposed as a well-behaved form of non-Markov decision process. Regular decision processes are characterised by a transition function and a reward function that depend on the whole history, though regularly (as in regular languages). In practice both the transition and the reward functions can be seen as finite transducers. We study reinforcement learning in regular decision processes. Our main contribution is to show that a near-optimal policy can be PAC-learned in polynomial time in a set of parameters that describe the underlying decision process. We argue that the identified set of parameters is minimal and it reasonably captures the difficulty of a regular decision process.

IJCAI Conference 2021 Conference Paper

Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis

  • Giuseppe De Giacomo
  • Antonio Di Stasio
  • Lucas M. Tabajara
  • Moshe Vardi
  • Shufang Zhu

Linear Temporal Logic (LTL) synthesis aims at automatically synthesizing a program that complies with desired properties expressed in LTL. Unfortunately it has been proved to be too difficult computationally to perform full LTL synthesis. There have been two success stories with LTL synthesis, both having to do with the form of the specification. The first is the GR(1) approach: use safety conditions to determine the possible transitions in a game between the environment and the agent, plus one powerful notion of fairness, Generalized Reactivity(1), or GR(1). The second, inspired by AI planning, is focusing on finite-trace temporal synthesis, with LTLf (LTL on finite traces) as the specification language. In this paper we take these two lines of work and bring them together. We first study the case in which we have an LTLf agent goal and a GR(1) assumption. We then add to the framework safety conditions for both the environment and the agent, obtaining a highly expressive yet still scalable form of LTL synthesis.

IJCAI Conference 2021 Conference Paper

HyperLDLf: a Logic for Checking Properties of Finite Traces Process Logs

  • Giuseppe De Giacomo
  • Paolo Felli
  • Marco Montali
  • Giuseppe Perelli

Temporal logics over finite traces, such as LTLf and its extension LDLf, have been adopted in several areas, including Business Process Management (BPM), to check properties of processes whose executions have an unbounded, but finite, length. These logics express properties of single traces in isolation, however, especially in BPM it is also of interest to express properties over the entire log, i. e. , properties that relate multiple traces of the log at once. In the case of infinite-traces, HyperLTL has been proposed to express these ``hyper'' properties. In this paper, motivated by BPM, we introduce HyperLDLf, a logic that extends LDLf with the hyper features of HyperLTL. We provide a sound, complete and computationally optimal technique, based on DFAs manipulation, for the model checking problem in the relevant case where the set of traces (i. e. , the log) is a regular language. We illustrate how this form of model checking can be used for verifying log of business processes and for advanced forms of process mining.

JAIR Journal 2021 Journal Article

Instance-Level Update in DL-Lite Ontologies through First-Order Rewriting

  • Giuseppe De Giacomo
  • Xavier Oriol
  • Riccardo Rosati
  • Domenico Fabio Savo

In this paper we study instance-level update in DL-LiteA, a well-known description logic that influenced the OWL 2 QL standard. Instance-level update regards insertions and deletions in the ABox of an ontology. In particular we focus on formula-based approaches to instance-level update. We show that DL-LiteA, which is well-known for enjoying first-order rewritability of query answering, enjoys a first-order rewritability property also for instance-level update. That is, every update can be reformulated into a set of insertion and deletion instructions computable through a non-recursive Datalog program with negation. Such a program is readily translatable into a first-order query over the ABox considered as a database, and hence into SQL. By exploiting this result, we implement an update component for DL-LiteA-based systems and perform some experiments showing that the approach works in practice.

IJCAI Conference 2021 Conference Paper

Intensional and Extensional Views in DL-Lite Ontologies

  • Marco Console
  • Giuseppe De Giacomo
  • Maurizio Lenzerini
  • Manuel Namici

The use of virtual collections of data is often essential in several data and knowledge management tasks. In the literature, the standard way to define virtual data collections is via views, i. e. , virtual relations defined using queries. In data and knowledge bases, the notion of views is a staple of data access, data integration and exchange, query optimization, and data privacy. In this work, we study views in Ontology-Based Data Access (OBDA) systems. OBDA is a powerful paradigm for accessing data through an ontology, i. e. , a conceptual specification of the domain of interest written using logical axioms. Intuitively, users of an OBDA system interact with the data only through the ontology's conceptual lens. We present a novel framework to express natural and sophisticated forms of views in OBDA systems and introduce fundamental reasoning tasks for these views. We study the computational complexity of these tasks and present classes of views for which these tasks are tractable or at least decidable.

PRL Workshop 2021 Workshop Paper

Learning a Symbolic Planning Domain through the Interaction with Continuous Environments

  • Elena Umili
  • Emanuele Antonioni
  • Francesco Riccio
  • Roberto Capobianco
  • Daniele Nardi
  • Giuseppe De Giacomo

One of the main challenges in AI is performing dynamic tasks by using approaches that efficiently predict the environment’s future outcomes. State-of-the-art planners can reason effectively with symbolic representations of the environment. However, when the environment is continuous and unstructured, manually extracting an ad-hoc symbolic model to perform planning may be infeasible. Deep Reinforcement Learning is known to automatically learn compact representations of the state space through interaction with the environment. However, it is not suitable for planning, giving up the efficiency we would gain by predicting the consequences of actions. This work focuses on continuous state-space MDPs and proposes an approach that naturally combines interaction, symbolic representation learning, and symbolic online planning. Our system leverages experience-data gained from the environment to autonomously learn a symbolic planning model composed of: (1) a symbol grounding model to switch from continuous to symbolic space and vice versa; (2) a symbolic transition model; (3) a value function for symbolic states. This model is used at training time to lead the interaction with the world. At each interaction step, we perform fast symbolic online planning over a finite horizon to choose the action to execute in the environment. The success of this strategy in the environment implicitly validates our automatically extracted symbolic model, since the system is able to effectively plan actions in the original MDP by reasoning only in the finite and symbolic domain. The approach has been evaluated on several continual OpenAI gym environments, addressing successfully both control problems and games.

KR Conference 2021 Conference Paper

Synthesis with Mandatory Stop Actions

  • Giuseppe De Giacomo
  • Antonio Di Stasio
  • Giuseppe Perelli
  • Shufang Zhu

We study the impact of the need for the agent to obligatorily instruct the action stop in her strategies. More specifically we consider synthesis (i. e. , planning) for LTLf goals under LTL environment specifications in the case the agent must mandatorily stop at a certain point. We show that this obligation makes it impossible to exploit the liveness part of the LTL environment specifications to achieve her goal, effectively reducing the environment specifications to their safety part only. This has a deep impact on the efficiency of solving the synthesis, which can sidestep handling Buchi determinization associated to LTL synthesis, in favor of finite-state automata manipulation as in LTLf synthesis. Next, we add to the agent goal, expressed in LTLf, a safety goal, expressed in LTL. Safety goals must hold forever, even when the agent stops, since the environment can still continue its evolution. Hence the agent, before stopping, must ensure that her safety goal will be maintained even after she stops. To do synthesis in this case, we devise an effective approach that mixes a synthesis technique based on finite-state automata (as in the case of LTLf goals) and model-checking of nondeterministic Buchi automata. In this way, again, we sidestep Buchi automata determinization, hence getting a synthesis technique that is intrinsically simpler than standard LTL synthesis.

KR Conference 2021 Conference Paper

Synthesizing Best-effort Strategies under Multiple Environment Specifications

  • Benjamin Aminof
  • Giuseppe De Giacomo
  • Alessio Lomuscio
  • Aniello Murano
  • Sasha Rubin

We formally introduce and solve the synthesis problem for LTL goals in the case of multiple, even contradicting, assumptions about the environment. Our solution concept is based on ``best-effort strategies'' which are agent plans that, for each of the environment specifications individually, achieve the agent goal against a maximal set of environments satisfying that specification. By means of a novel automata theoretic characterization we demonstrate that this best-effort synthesis for multiple environments is 2ExpTime-complete, i. e. , no harder than plain LTL synthesis. We study an important case in which the environment specifications are increasingly indeterminate, and show that as in the case of a single environment, best-effort strategies always exist for this setting. Moreover, we show that in this setting the set of solutions are exactly the strategies formed as follows: amongst the best-effort agent strategies for ɸ under the environment specification E1, find those that do a best-effort for ɸ under (the more indeterminate) environment specification E2, and amongst those find those that do a best-effort for ɸ under the environment specification E3, etc.

KR Conference 2021 Conference Paper

The Nondeterministic Situation Calculus

  • Giuseppe De Giacomo
  • Yves Lespérance

The standard situation calculus assumes that atomic actions are deterministic. But many domains involve nondeterministic actions, with problems such as fully observable nondeterministic (FOND) planning and high-level program execution requiring solutions. Various approaches have been proposed to accommodate nondeterminism on top of the standard situation calculus language, for instance by introducing nondeterministic programs as in Golog and ConGolog. But a key problem in these approaches is that they don’t clearly distinguish between choices that can be made by the agent and choices that are made by the environment, i. e. , angelic vs. devilish nondeterminism. In this paper, we propose a simple extension to the standard situation calculus that accommodates nondeterministic actions and preserves Reiter’s solution to the frame problem and answering projection queries through regression. We also provide a formalization of FOND planning and show how ConGolog high-level program execution in nondeterministic domains can be defined.

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.

AAAI Conference 2020 Conference Paper

ElGolog: A High-Level Programming Language with Memory of the Execution History

  • Giuseppe De Giacomo
  • Yves Lespérance
  • Eugenia Ternovska

Most programming languages only support tests that refer exclusively to the current state. This applies even to high-level programming languages based on the situation calculus such as Golog. The result is that additional variables/fluents/data structures must be introduced to track conditions that the program uses in tests to make decisions. In this paper, drawing inspiration from McCarthy’s Elephant 2000, we propose an extended version of Golog, called ElGolog, that supports rich tests about the execution history, where tests are expressed in a first-order variant of two-way linear dynamic logic that uses ElGolog programs with converse. We show that in spite of rich tests, ElGolog shares key features with Golog, including a sematics based on macroexpansion into situation calculus formulas, upon which regression can still be applied. We also show that like Golog, our extended language can easily be implemented in Prolog.

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

LTLƒ Synthesis with Fairness and Stability Assumptions

  • Shufang Zhu
  • Giuseppe De Giacomo
  • Geguang Pu
  • Moshe Y. Vardi

In synthesis, assumptions are constraints on the environment that rule out certain environment behaviors. A key observation here is that even if we consider systems with LTLf goals on finite traces, environment assumptions need to be expressed over infinite traces, since accomplishing the agent goals may require an unbounded number of environment action. To solve synthesis with respect to finite-trace LTLf goals under infinite-trace assumptions, we could reduce the problem to LTL synthesis. Unfortunately, while synthesis in LTLf and in LTL have the same worst-case complexity (both 2EXPTIME-complete), the algorithms available for LTL synthesis are much more difficult in practice than those for LTLf synthesis. In this work we show that in interesting cases we can avoid such a detour to LTL synthesis and keep the simplicity of LTLf synthesis. Specifically, we develop a BDD-based fixpoint-based technique for handling basic forms of fairness and of stability assumptions. We show, empirically, that this technique performs much better than standard LTL synthesis.

KR Conference 2020 Conference Paper

Nondeterministic Strategies and their Refinement in Strategy Logic

  • Giuseppe De Giacomo
  • Bastien Maubert
  • Aniello Murano

Nondeterministic strategies are strategies (or protocols, or plans) that, given a history in a game, assign a set of possible actions, all of which are winning. An important problem is that of refining such strategies. For instance, given a nondeterministic strategy that allows only safe executions, refine it to, additionally, eventually reach a desired state of affairs. We show that strategic problems involving strategy refinement can be solved elegantly in the framework of Strategy Logic (SL), a very expressive logic to reason about strategic abilities. Specifically, we introduce an extension of SL with nondeterministic strategies and an operator expressing strategy refinement. We show that model checking this logic can be done at no additional computational cost with respect to standard SL, and can be used to solve a variety of problems such as synthesis of maximally permissive strategies or refinement of Nash equilibria.

IJCAI Conference 2020 Conference Paper

Pure-Past Linear Temporal and Dynamic Logic on Finite Traces

  • Giuseppe De Giacomo
  • Antonio Di Stasio
  • Francesco Fuggitti
  • Sasha Rubin

We review PLTLf and PLDLf, the pure-past versions of the well-known logics on finite traces LTLf and LDLf, respectively. PLTLf and PLDLf are logics about the past, and so scan the trace backwards from the end towards the beginning. Because of this, we can exploit a foundational result on reverse languages to get an exponential improvement, over LTLf /LDLf, for computing the corresponding DFA. This exponential improvement is reflected in several forms of sequential decision making involving temporal specifications, such as planning and decision problems in non-deterministic and non-Markovian domains. Interestingly, PLTLf (resp. , PLDLf ) has the same expressive power as LTLf (resp. , LDLf ), but transforming a PLTLf (resp. , PLDLf ) formula into its equivalent LTLf (resp. ,LDLf) is quite expensive. Hence, to take advantage of the exponential improvement, properties of interest must be directly expressed in PLTLf /PLDLf.

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

ICAPS Conference 2020 Conference Paper

Stochastic Fairness and Language-Theoretic Fairness in Planning in Nondeterministic Domains

  • Benjamin Aminof
  • Giuseppe De Giacomo
  • Sasha Rubin

We address two central notions of fairness in the literature of nondeterministic fully observable domains. The first, which we call stochastic fairness, is classical, and assumes an environment which operates probabilistically using possibly unknown probabilities. The second, which is language-theoretic, assumes that if an action is taken from a given state infinitely often then all its possible outcomes should appear infinitely often; we call this state-action fairness. While the two notions coincide for standard reachability goals, they differ for temporally extended goals. This important difference has been overlooked in the planning literature and has led to the use of a product-based reduction in a number of published algorithms which were stated for state-action fairness, for which they are incorrect, while being correct for stochastic fairness. We remedy this and provide a correct optimal algorithm for solving state-action fair planning for ltl/ltlf goals, as well as a correct proof of the lower bound of the goal-complexity. Our proof is general enough that it also provides, for the no-fairness and stochastic-fairness cases, multiple missing lower bounds and new proofs of known lower bounds. Overall, we show that stochastic fairness is better behaved than state-action fairness.

IJCAI Conference 2020 Conference Paper

Synthesizing strategies under expected and exceptional environment behaviors

  • Benjamin Aminof
  • Giuseppe De Giacomo
  • Alessio Lomuscio
  • Aniello Murano
  • Sasha Rubin

We consider an agent that operates with two models of the environment: one that captures expected behaviors and one that captures additional exceptional behaviors. We study the problem of synthesizing agent strategies that enforce a goal against environments operating as expected while also making a best effort against exceptional environment behaviors. We formalize these concepts in the context of linear-temporal logic, and give an algorithm for solving this problem. We also show that there is no trade-off between enforcing the goal under the expected environment specification and making a best-effort for it under the exceptional one.

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.

KR Conference 2020 Conference Paper

Two-Stage Technique for LTLf Synthesis Under LTL Assumptions

  • Giuseppe De Giacomo
  • Antonio Di Stasio
  • Moshe Y. Vardi
  • Shufang Zhu

In synthesis, assumption are constraints on the environments that rule out certain environment behaviors. A key observation is that even if we consider system with LTLf goals on finite traces, assumptions need to be expressed considering infinite traces, using LTL on infinite traces, since the decision to stop the trace is controlled by the agent. To solve synthesis of LTLf goals under LTL assumptions, we could reduce the problem to LTL synthesis. Unfortunately, while synthesis in LTLf and in LTL have the same worst-case complexity (both are 2EXPTIME-complete), the algorithms available for LTL synthesis are much harder in practice than those for LTLf synthesis. Recently, it has been shown that in basic forms of fairness and stability assumptions we can avoid such a detour to LTL and keep the simplicity of LTLf synthesis. In this paper, we generalize these results and show how to effectively handle any kind of LTL assumptions. Specifically, we devise a two-stage technique for solving LTLf under general LTL assumptions and show empirically that this technique performs much better than standard LTL synthesis.

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.

IJCAI Conference 2019 Conference Paper

Planning for LTLf /LDLf Goals in Non-Markovian Fully Observable Nondeterministic Domains

  • Ronen I. Brafman
  • Giuseppe De Giacomo

In this paper, we investigate non-Markovian Nondeterministic Fully Observable Planning Domains (NMFONDs), variants of Nondeterministic Fully Observable Planning Domains (FONDs) where the next state is determined by the full history leading to the current state. In particular, we introduce TFONDs which are NMFONDs where conditions on the history are succinctly and declaratively specified using the linear-time temporal logic on finite traces LTLf and its extension LDLf. We provide algorithms for planning in TFONDs for general LTLf/LDLf goals, and establish tight complexity bounds w. r. t. the domain representation and the goal, separately. We also show that TFONDs are able to capture all NMFONDs in which the dependency on the history is "finite state". Finally, we show that TFONDs also capture Partially Observable Nondeterministic Planning Domains (PONDs), but without referring to unobservable variables.

ICAPS Conference 2019 Conference Paper

Planning under LTL Environment Specifications

  • Benjamin Aminof
  • Giuseppe De Giacomo
  • Aniello Murano
  • Sasha Rubin

Planning domains represent what an agent assumes or believes about the environment it acts in. In the presence of nondeterminism, additional temporal assumptions, such as fairness, are often expressed as extra conditions on the domain. Here we consider environment specifications expressed in arbitrary LTL, which generalize many forms of environment specifications, including classical specifications of nondeterministic domains, fairness, and other forms of linear-time constraints on the domain itself. Existing literature typically implicitly or explicitly considers environment specifications as constraints on possible traces. In contrast, in spite of the fact that we use a linear-time formalism, we propose to consider environment specifications as specifications of environment strategies. Planning in this framework is the problem of computing an agent strategy that achieves its goal against all environment strategies satisfying the specification. We study the mathematical and computational properties of planning in this general setting. We observe that not all LTL formulas correspond to legitimate environment specifications, and formally characterize the ones that do. Moreover, we show that our notion of planning generalizes the classical notion of Church’s synthesis, and that in spite this one can still solve it optimally using classical Church’s synthesis.

IJCAI Conference 2019 Conference Paper

Regular Decision Processes: A Model for Non-Markovian Domains

  • Ronen I. Brafman
  • Giuseppe De Giacomo

We introduce and study Regular Decision Processes (RDPs), a new, compact, factored model for domains with non-Markovian dynamics and rewards. In RDPs, transition and reward functions are specified using formulas in linear dynamic logic over finite traces, a language with the expressive power of regular expressions. This allows specifying complex dependence on the past using intuitive and compact formulas, and provides a model that generalizes MDPs and k-order MDPs. RDPs can also approximate POMDPs without having to postulate the existence of hidden variables, and, in principle, can be learned from observations only.

AAMAS Conference 2019 Conference Paper

Regular Decision Processes: Modelling Dynamic Systems without Using Hidden Variables: Extended Abstrac

  • Ronen I. Brafman
  • Giuseppe De Giacomo

We describe Regular Decision Processes (RDPs) a model in between MDPs and POMDPs. Like in POMDPs, the effect of an action may depend on the entire history of actions and observations, but this dependence is restricted to regular functions only. This makes RDP a tractable, yet rich model, that does not hypothesize hidden state, and could possibly be useful for learning dynamic systems.

AAAI Conference 2019 Conference Paper

Unbounded Orchestrations of Transducers for Manufacturing

  • Natasha Alechina
  • Tomáš Brázdil
  • Giuseppe De Giacomo
  • Paolo Felli
  • Brian Logan
  • Moshe Y. Vardi

There has recently been increasing interest in using reactive synthesis techniques to automate the production of manufacturing process plans. Previous work has assumed that the set of manufacturing resources is known and fixed in advance. In this paper, we consider the more general problem of whether a controller can be synthesized given sufficient resources. In the unbounded setting, only the types of available manufacturing resources are given, and we want to know whether it is possible to manufacture a product using only resources of those type(s), and, if so, how many resources of each type are needed. We model manufacturing processes and facilities as transducers (automata with output), and show that the unbounded orchestration problem is decidable and the (Pareto) optimal set of resources necessary to manufacture a product is computable for uni-transducers. However, for multitransducers, the problem is undecidable.

IJCAI Conference 2018 Conference Paper

Abstraction of Agents Executing Online and their Abilities in the Situation Calculus

  • Bita Banihashemi
  • Giuseppe De Giacomo
  • Yves Lespérance

We develop a general framework for abstracting online behavior of an agent that may acquire new knowledge during execution (e. g. , by sensing), in the situation calculus and ConGolog. We assume that we have both a high-level action theory and a low-level one that represent the agent's behavior at different levels of detail. In this setting, we define ability to perform a task/achieve a goal, and then show that under some reasonable assumptions, if the agent has a strategy by which she is able to achieve a goal at the high level, then we can refine it into a low-level strategy to do so.

IJCAI Conference 2018 Conference Paper

Automata-Theoretic Foundations of FOND Planning for LTLf and LDLf Goals

  • Giuseppe De Giacomo
  • Sasha Rubin

We study planning for LTLf and LDLf temporally extended goals in nondeterministic fully observable domains (FOND). We consider both strong and strong cyclic plans, and develop foundational automata-based techniques to deal with both cases. Using these techniques we provide the computational characterization of both problems, separating the complexity in the size of the domain specification from that in the size of the formula. Specifically we establish them to be EXPTIME-complete and 2EXPTIME-complete, respectively, for both problems. In doing so, we also show 2EXPTIME-hardness for strong cyclic plans, which was open.

AAMAS Conference 2018 Conference Paper

Hierarchical Agent Supervision

  • Bita Banihashemi
  • Giuseppe De Giacomo
  • Yves Lesp�rance

Agent supervision is a form of control/customization where a supervisor restricts the behavior of an agent to enforce certain requirements, while leaving the agent as much autonomy as possible. To facilitate supervision, it is often of interest to consider hierarchical models where a high level abstracts over low-level behavior details. We study hierarchical agent supervision in the context of the situation calculus and the ConGolog agent programming language, where we have a rich first-order representation of the agent state. We define the constraints that ensure that the controllability of individual actions at the high level in fact captures the controllability of their implementation at the low level. On the basis of this, we show that we can obtain the maximally permissive supervisor by first considering only the high-level model and obtaining a highlevel supervisor and then refining its actions locally, thus greatly simplifying the supervisor synthesis task.

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 2018 Conference Paper

Synthesis of Orchestrations of Transducers for Manufacturing

  • Giuseppe De Giacomo
  • Moshe Vardi
  • Paolo Felli
  • Natasha Alechina
  • Brian Logan

In this paper, we model manufacturing processes and facilities as transducers (automata with output). The problem of whether a given manufacturing process can be realized by a given set of manufacturing resources can then be stated as an orchestration problem for transducers. We first consider the conceptually simpler case of uni-transducers (transducers with a single input and a single output port), and show that synthesizing orchestrations for uni-transducers is EXPTIMEcomplete. Surprisingly, the complexity remains the same for the more expressive multi-transducer case, where transducers have multiple input and output ports and the orchestration is in charge of dynamically connecting ports during execution.

AAAI Conference 2017 Conference Paper

Abstraction in Situation Calculus Action Theories

  • Bita Banihashemi
  • Giuseppe De Giacomo
  • Yves Lesperance

We develop a general framework for agent abstraction based on the situation calculus and the ConGolog agent programming language. We assume that we have a high-level specification and a low-level specification of the agent, both represented as basic action theories. A refinement mapping specifies how each high-level action is implemented by a lowlevel ConGolog program and how each high-level fluent can be translated into a low-level formula. We define a notion of sound abstraction between such action theories in terms of the existence of a suitable bisimulation between their respective models. Sound abstractions have many useful properties that ensure that we can reason about the agent’s actions (e. g. , executability, projection, and planning) at the abstract level, and refine and concretely execute them at the low level. We also characterize the notion of complete abstraction where all actions (including exogenous ones) that the high level thinks can happen can in fact occur at the low level.

IJCAI Conference 2017 Conference Paper

Generalized Planning: Non-Deterministic Abstractions and Trajectory Constraints

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

We study the characterization and computation of general policies for families of problems that share a structure characterized by a common reduction into a single abstract problem. Policies mu that solve the abstract problem P have been shown to solve all problems Q that reduce to P provided that mu terminates in Q. In this work, we shed light on why this termination condition is needed and how it can be removed. The key observation is that the abstract problem P captures the common structure among the concrete problems Q that is local (Markovian) but misses common structure that is global. We show how such global structure can be captured by means of trajectory constraints that in many cases can be expressed as LTL formulas, thus reducing generalized planning to LTL synthesis. Moreover, for a broad class of problems that involve integer variables that can be increased or decreased, trajectory constraints can be compiled away, reducing generalized planning to fully observable non-deterministic planning.

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.

ICAPS Conference 2016 Conference Paper

Computing Trace Alignment against Declarative Process Models through Planning

  • Giuseppe De Giacomo
  • Fabrizio Maria Maggi
  • Andrea Marrella
  • Sebastian Sardiña

Process mining techniques aim at extracting non-trivial knowledge from event traces, which record the concrete execution of business processes. Typically, traces are "dirty" and contain spurious events or miss relevant events. Trace alignment is the problem of cleaning such traces against a process specification. There has recently been a growing use of declarative process models, e. g. , Declare (based on LTL over finite traces) to capture constraints on the allowed task flows. We demonstrate here how state-of-the-art classical planning technologies can be used for trace alignment by presenting a suitable encoding. We report experimental results using a real log from a financial domain.

IJCAI Conference 2016 Conference Paper

Imperfect-Information Games and Generalized Planning

  • Giuseppe De Giacomo
  • Aniello Murano
  • Sasha Rubin
  • Antonio Di Stasio

We study a generalized form of planning under partial observability, in which we have multiple, possibly infinitely many, planning domains with the same actions and observations, and goals expressed over observations, which are possibly temporally extended. By building on work on two-player (non-probabilistic) games with imperfect information in the Formal Methods literature, we devise a general technique, generalizing the belief-state construction, to remove partial observability. This reduces the planning problem to a game of perfect information with a tight correspondence between plans and strategies. Then we instantiate the technique and solve some generalized-planning problems.

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

Online Agent Supervision in the Situation Calculus

  • Bita Banihashemi
  • Giuseppe De Giacomo
  • Yves Lesp
  • eacute; rance

Agent supervision is a form of control / customization where a supervisor restricts the behavior of an agent to enforce certain requirements, while leaving the agent as much autonomy as possible. In this work, we investigate supervision of an agent that may acquire new knowledge about her environment during execution, for example, by sensing. Thus we consider an agent's online executions, where, as she executes the program, at each time point she must make decisions on what to do next based on what her current knowledge is. This is done in a setting based on the situation calculus and a variant of the ConGolog programming language. The main results of this paper are (i) a formalization of the online maximally permissive supervisor, (ii) a sound and complete technique for execution of the agent as constrained by such a supervisor, and (iii)a new type of lookahead search construct that ensures nonblockingness over such online executions.

KR Conference 2016 Short Paper

Online Situation-Determined Agents and their Supervision

  • Bita Banihashemi
  • Giuseppe De Giacomo
  • Yves Lesperance

Agent supervision is a form of control/customization where a supervisor restricts the behavior of an agent to enforce certain requirements, while leaving the agent as much autonomy as possible. In this work, we investigate supervision of an agent that may acquire new knowledge about her environment during execution, for example, by sensing. Thus we consider an agent’s online executions, where, as she executes the program, at each time point she must make decisions on what to do next based on what her current knowledge is. This is done in a setting based on the situation calculus and a variant of the ConGolog programming language. To reason about such agents, we first define a notion of online situation-determined agent which ensures that for any sequence of actions that the agent can perform online, the resulting agent configuration is unique. We then present our formalization of the online maximally permissive supervisor.

KR Conference 2016 Conference Paper

Regular Open APIs

  • Diego Calvanese
  • Giuseppe De Giacomo
  • Maurizio Lenzerini
  • Moshe Vardi

Open APIs are software intermediaries that make it possible for application programs to interact with data and processes, which can both be viewed as forms of services. In many scenarios, when one wants to obtain or publish a new service, one would like to check whether the new functionality can simply be obtained by suitably composing existing services. In this paper we study this problem by distinguishing between the two forms of services, that we call data-centric and process-centric, respectively. In the former, each API is an abstraction of a query specified on a data source, and composition amounts to building a new query by using the available APIs as views over the data. In the latter, each API abstracts a process made up by sequences of atomic actions, and composition means realizing a new process by suitably using the APIs exposed by the available services. We make the assumption that the semantics of services is specified by means of one of the most basic formalisms used in Computer Science, namely, regular languages. As a result, we get a rich analysis framework, where composition shows similarities to conformant and conditional planning. We describe composition principles and automated synthesis techniques for each of the two settings. 1 Moshe Y. Vardi Department of Computer Science Rice Univ., Houston, TX, U. S. A. vardi@cs. rice. edu

ECAI Conference 2016 Conference Paper

Situation Calculus Game Structures and GDL

  • Giuseppe De Giacomo
  • Yves Lespérance
  • Adrian R. Pearce

We present a situation calculus-based account of multi-players synchronous games in the style of general game playing. Such games can be represented as action theories of a special form, situation calculus synchronous game structures (SCSGSs), in which we have a single action tick whose effects depend on the combination of moves selected by the players. Then one can express properties of the game, e. g. , winning conditions, playability, weak and strong winnability, etc. in a first-order alternating-time &mu; -calculus. We discuss verification in this framework considering computational effectiveness. We also show that SCSGSs can be considered as a first-order variant of the Game Description Language (GDL) that supports infinite domains and possibly non-terminating games. We do so by giving a translation of GDL specifications into SCSGSs and showing its correctness. Finally, we show how a player's possible moves can be specified in a Golog-like programming language.

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

Data Complexity of Query Answering in Description Logics (Extended Abstract)

  • Diego Calvanese
  • Giuseppe De Giacomo
  • Domenico Lembo
  • Maurizio Lenzerini
  • Riccardo Rosati

We study the data complexity of answering conjunctive queries over Description Logic knowledge bases constituted by a TBox and an ABox. In particular, we are interested in characterizing the FOrewritability and the polynomial tractability boundaries of conjunctive query answering, depending on the expressive power of the DL used to express the knowledge base. What emerges from our complexity analysis is that the Description Logics of the DL-Lite family are essentially the maximal logics allowing for conjunctive query answering through standard database technology.

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.

Highlights Conference 2015 Conference Abstract

LTL and LDL on Finite Traces

  • Giuseppe De Giacomo

In this talk we look at temporal logics on traces that are assumed to be finite, as typical of action planning in Artificial Intelligence and of processes modeling in Business Process Management. Having to deal with finite traces has been considered a sort of accident in much of the AI and BPM literature, and standard temporal logics (on infinite traces) have been hacked to fit this assumption. Only recently a specific interest in studying the impact of such an assumption has emerged. We will look at two specific logics (i) LTLf, i. e. , LTL interpreted over finite traces, which has the expressive power of FOL and star-free regular expression over finite stings; and (ii) LDLf, i. e. , Linear-time Dynamic Logic on finite traces, which has the expressive power of MSO and full regular expression. We review the main results on satisfiability, verification, and synthesis, also drawing connections with work in AI planning. The main catch is that working with these logics can be based on manipulation of regular automata on finite strings, simplifying greatly reasoning and especially synthesis. Joint work with Moshe Y. Vardi (Rice Univ. , USA) 14: 30 14: 40 Break

IJCAI Conference 2015 Conference Paper

On the Undecidability of the Situation Calculus Extended with Description Logic Ontologies

  • Diego Calvanese
  • Giuseppe De Giacomo
  • Mikhail Soutchanski

In this paper we investigate situation calculus action theories extended with ontologies, expressed as description logics TBoxes that act as state constraints. We show that this combination, while natural and desirable, is particularly problematic: it leads to undecidability of the simplest form of reasoning, namely satisfiability, even for the simplest kinds of description logics and the simplest kind of situation calculus action theories.

IJCAI Conference 2015 Conference Paper

Synthesis for LTL and LDL on Finite Traces

  • Giuseppe De Giacomo
  • Moshe Vardi

In this paper, we study synthesis from logical specifications over finite traces expressed in LTLf and its extension LDLf. Specifically, in this form of synthesis, propositions are partitioned in controllable and uncontrollable ones, and the synthesis task consists of setting the controllable propositions over time so that, in spite of how the value of the uncontrollable ones changes, the specification is fulfilled. Conditional planning in presence of declarative and procedural trajectory constraints is a special case of this form of synthesis. We characterize the problem computationally as 2EXPTIME-complete and present a sound and complete synthesis technique based on DFA (reachability) games.

TIME Conference 2015 Invited Paper

Temporal Reasoning in Bounded Situation Calculus

  • Giuseppe De Giacomo

In this talk, we survey recent results on situation calculus bounded action theories. These are action theories with the constraints that the size of the extension of fluents in every situation must be bounded, though such an extension changes from situation to situation. Such action theories give rise to infinite transition systems that can be faithfully abstracted into finite ones, making verification decidable.

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.

AAAI Conference 2014 Conference Paper

Reasoning on LTL on Finite Traces: Insensitivity to Infiniteness

  • Giuseppe De Giacomo
  • Riccardo De Masellis
  • Marco Montali

In this paper we study when an LTL formula on finite traces (LTLf formula) is insensitive to infiniteness, that is, it can be correctly handled as a formula on infinite traces under the assumption that at a certain point the infinite trace starts repeating an end event forever, trivializing all other propositions to false. This intuition has been put forward and (wrongly) assumed to hold in general in the literature. We define a necessary and sufficient condition to characterize whether an LTLf formula is insensitive to infiniteness, which can be automatically checked by any LTL reasoner. Then, we show that typical LTLf specification patterns used in process and service modeling in CS, as well as trajectory constraints in Planning and transition-based LTLf specifications of action domains in KR, are indeed very often insensitive to infiniteness. This may help to explain why the assumption of interpreting LTL on finite and on infinite traces has been (wrongly) blurred. Possibly because of this blurring, virtually all literature detours to Büchi automata for constructing the NFA that accepts the traces satisfying an LTLf formula. As a further contribution, we give a simple direct algorithm for computing such NFA.

ICAPS Conference 2013 Conference Paper

A Generic Technique for Synthesizing Bounded Finite-State Controllers

  • Yuxiao Hu 0002
  • Giuseppe De Giacomo

Finite-state controllers are a compact and effective plan representation for agent widely used in AI. In this paper, we proposea generic framework and related solver for synthesizing bounded finite-state controllers, and show its instantiations to three different applications, including generalized planning, planning programs and service composition under partial observability and controllability. We show that our generic solver is sound and complete, and amenable to heuristics that take into account the structure of the specific target instantiation. Experiments show that instantiations of our solver to the problems above often outperform tailored approaches in the literature. This suggests that our proposal is a promising base point for future research on finite-state controller synthesis.

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

Linear Temporal Logic and Linear Dynamic Logic on Finite Traces

  • Giuseppe De Giacomo
  • Moshe Y. Vardi

In this paper we look into the assumption of interpreting LTL over finite traces. In particular we show that LTLf, i. e. , LTL under this assumption, is less expressive than what might appear at first sight, and that at essentially no computational cost one can make a significant increase in expressiveness while maintaining the same intuitiveness of LTLf. Indeed, we propose a logic, LDLf for Linear Dynamic Logic over finite traces, which borrows the syntax from Propositional Dynamic Logic (PDL), but is interpreted over finite traces. Satisfiability, validity and logical implication (as well as model checking) for LDLf are PSPACE-complete as for LTLf (and LTL).

IJCAI Conference 2013 Conference Paper

Supremal Realizability of Behaviors with Uncontrollable Exogenous Events

  • Nitin Yadav
  • Paolo Felli
  • Giuseppe De Giacomo
  • Sebastian Sardina

The behavior composition problem involves the automatic synthesis of a controller able to “realize” (i. e. , implement) a desired target behavior specification by suitably coordinating a set of already available behaviors. While the problem has been thoroughly studied, one open issue has resisted a principled solution: if the target specification is not fully realizable, is there a way to realize it “at best”? In this paper we answer positively, by showing that there exists a unique supremal realizable target behavior satisfying the specification. More importantly we give an effective procedure to compute such a target. Then, we introduce exogenous events, and show that the supremal can again be computed, though this time, into two variants, depending on the ability to observe such events.

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.

AAMAS Conference 2012 Conference Paper

On Supervising Agents in Situation-Determined ConGolog

  • Giuseppe De Giacomo
  • Yves Lesp
  • eacute; rance
  • Christian Muise

We investigate agent supervision, a form of customization, which constrains the actions of an agent so as to enforce certain desired behavioral specifications. This is done in a setting based on the Situation Calculus and a variant of the ConGolog programming language which allows for nondeterminism, but requires the remainder of a program after the execution of an action to be determined by the resulting situation. Such programs can be fully characterized by the set of action sequences that they generate. Hence operations like intersection and difference become natural. The main results of the paper are a characterization of the maximally permissive supervisor that minimally constrains the agent so as to enforce the desired behavioral constraints when some agent actions are uncontrollable, and a sound and complete technique to execute the agent as constrained by such a supervisor.

AAAI Conference 2012 Conference Paper

Ontology-Based Data Access with Dynamic TBoxes in DL-Lite

  • Floriana Di Pinto
  • Giuseppe De Giacomo
  • Maurizio Lenzerini
  • Riccardo Rosati

In this paper we introduce the notion of mapping-based knowledge base (MKB) to formalize the situation where both the extensional and the intensional level of the ontology are determined by suitable mappings to a set of (relational) data sources. This allows for making the intensional level of the ontology as dynamic as traditionally the extensional level is. To do so, we resort to the meta-modeling capabilities of higher-order Description Logics, which allow us to see concepts and roles as individuals, and vice versa. The challenge in this setting is to design tractable query answering algorithms. Besides the definition of MKBs, our main result is that answering instance queries posed to MKBs expressed in Hi(DL-LiteR) can be done efficiently. In particular, we define a query rewriting technique that produces first-order (SQL) queries to be posed to the data sources.

KR Conference 2012 Conference Paper

Synthesizing agent protocols for LTL specifications against multiple partially-observable environments

  • Giuseppe De Giacomo
  • Paolo Felli
  • Alessio Lomuscio

An automata-based approach to planning for full-fledged We consider the problem of synthesizing an agent protocol satisfying LTL specifications for multiple, partiallyobservable environments. We present a sound and complete procedure for solving the synthesis problem in this setting and show it is computationally optimal from a theoretical complexity standpoint. While this produces perfect-recall, hence unbounded, strategies we show how to transform these into agent protocols with bounded number of states.

ECAI Conference 2012 Conference Paper

Verification of Description Logic Knowledge and Action Bases

  • Babak Bagheri Hariri
  • Diego Calvanese
  • Giuseppe De Giacomo
  • Riccardo De Masellis
  • Paolo Felli
  • Marco Montali

We introduce description logic (DL) Knowledge and Action Bases (KAB), a mechanism that provides both a semantically rich representation of the information on the domain of interest in terms of a DL KB and a set of actions to change such information over time, possibly introducing new objects. We resort to a variant of DL-Lite where UNA is not enforced and where equality between objects may be asserted and inferred. Actions are specified as sets of conditional effects, where conditions are based on epistemic queries over the KB (TBox and ABox), and effects are expressed in terms of new ABoxes. We address the verification of temporal properties expressed in a variant of first-order &mu; -calculus where a controlled form of quantification across states is allowed. Notably, we show decidability of verification, under a suitable restriction inspired by the notion of weak acyclicity in data exchange.

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.

IJCAI Conference 2011 Conference Paper

Efficient Reasoning in Proper Knowledge Bases with Unknown Individuals

  • Giuseppe De Giacomo
  • Yves Lesp
  • eacute; rance
  • Hector J. Levesque

This work develops an approach to efficient reasoning in first-order knowledge bases with incomplete information. We build on Levesque's proper knowledge bases approach, which supports limited incomplete knowledge in the form of a possibly infinite set of positive or negative ground facts. We propose a generalization which allows these facts to involve unknown individuals, as in the work on labeled null values in databases. Dealing with such unknown individuals has been shown to be a key feature in the database literature on data integration and data exchange. In this way, we obtain one of the most expressive first-order open-world settings for which reasoning can still be done efficiently by evaluation, as in relational databases. We show the soundness of the reasoning procedure and its completeness for queries in a certain normal form.

IJCAI Conference 2011 Conference Paper

Generalized Planning: Synthesizing Plans that Work for Multiple Environments

  • Yuxiao Hu
  • Giuseppe De Giacomo

We give a formal definition of generalized planning that is independent of any representation formalism. We assume that our generalized plans must work on a set of deterministic environments, which are essentially unrelated to each other. We prove that generalized planning for a finite set of environments is always decidable and EXPSPACE-complete. Our proof is constructive and gives us a sound, complete and complexity-wise optimal technique. We also consider infinite sets of environments, and show that generalized planning for the infinite "one-dimensional problems, " known in the literature to be recursively enumerable when restricted to finite-state plans, is EXPSPACE-decidable without sequence functions, and solvable by generalized planning for finite sets.

AAAI Conference 2011 Conference Paper

Higher-Order Description Logics for Domain Metamodeling

  • Giuseppe De Giacomo
  • Maurizio Lenzerini
  • Riccardo Rosati

We investigate an extension of Description Logics (DL) with higher-order capabilities, based on Henkin-style semantics. Our study starts from the observation that the various possibilities of adding higher-order constructs to a DL form a spectrum of increasing expressive power, including domain metamodeling, i. e. , using concepts and roles as predicate arguments. We argue that higher-order features of this type are sufficiently rich and powerful for the modeling requirements arising in many relevant situations, and therefore we carry out an investigation of the computational complexity of satisfiability and conjunctive query answering in DLs extended with such higher-order features. In particular, we show that adding domain metamodeling capabilities to SHIQ (the core of OWL 2) has no impact on the complexity of the various reasoning tasks. This is also true for DL-LiteR (the core of OWL 2 QL) under suitable restrictions on the queries.

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

Node Selection Query Languages for Trees

  • Diego Calvanese
  • Giuseppe De Giacomo
  • Maurizio Lenzerini
  • Moshe Vardi

The study of node-selection query languages for (finite) trees has been a major topic in the recent research on query languages for Web documents. On one hand, there has been an extensive study of XPath and its various extensions. On the other hand, query languages based on classical logics, such as first-order logic (FO) or monadic second-order logic (MSO), have been considered. Results in this area typically relate an Xpath-based language to a classical logic. What has yet to emerge is an XPath-related language that is expressive as MSO, and at the same time enjoys the computational properties of XPath, which are linear query evaluation and exponential query-containment test. In this paper we propose µXPath, which is the alternation-free fragment of XPath extended with fixpoint operators. Using two-way alternating automata, we show that this language does combine desired expressiveness and computational properties, placing it as an attractive candidate as the definite query language for trees.

KR Conference 2010 Conference Paper

Situation calculus-based programs for representing and reasoning about game structures

  • Giuseppe De Giacomo
  • Yves Lesperance
  • Adrian Pearce

A wide range of problems, from contingent and multiagent planning to process/service orchestration, can be viewed as games. In many of these, it is natural to specify the possible behaviors procedurally. In this paper, we develop a logical framework for specifying these types of problems/games based on the situation calculus and ConGolog. The framework incorporates gametheoretic path quantifiers as in ATL. We show that the framework can be used to model such problems in a natural way. We also show how verification/synthesis techniques can be used to solve problems expressed in the framework. In particular, we develop a method for dealing with infinite state settings using fixpoint approximation and “characteristic graphs”.

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.

IJCAI Conference 2009 Conference Paper

  • Sebastian Sardina
  • Giuseppe De Giacomo

We look at composition of (possibly nonterminating) high-level programs over situation calculus action theories. Specifically the problem we look at is as follows: given a library of available ConGolog programs and a target program not in the library, verify whether the target program executions be realized by composing fragments of the executions of the available programs; and, if so, synthesize a controller that does the composition automatically. This kind of composition problems have been investigated in the CS and AI literature, but always assuming finite states settings. Here, instead, we investigate the issue in the context of infinite domains that may go through an infinite number of states as a result of actions. Obviously in this context the problem is undecidable. Nonetheless, by exploiting recent results in the AI literature, we devise a sound and well characterized technique to actually solve the problem.

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.

AAMAS Conference 2008 Conference Paper

A Model of Contingent Planning for Agent Programming Languages

  • Yves Lesperance
  • Giuseppe De Giacomo
  • Atalay Ozgovde

In this paper, we develop a formal model of planning for an agent that is operating in a dynamic and incompletely known environment. We assume that both the agent’s task and the behavior of the agents in the environment are expressed as high-level nondeterministic concurrent programs in some agent programming language (APL). In this context, planning must produce a deterministic conditional plan for the agent that can be successfully executed against all possible executions of the environment program. We handle actions with nondeterministic effects, as well as sensing actions, by treating them as actions that trigger an environmental reaction that is not under the planning agent’s control. Our model of contingent planning is specified for a generic APL with a transition semantics. Within this model, we devise a general procedure for computing the contingent plans. We also show how the model can be instantiated in the situation calculus with programs for the agent and the environment expressed in ConGolog, and we describe an implementation of the planning mechanism in this case.

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.

KR Conference 2008 Conference Paper

Path-Based Identification Constraints in Description Logics

  • Diego Calvanese
  • Giuseppe De Giacomo
  • Domenico Lembo
  • Maurizio Lenzerini
  • Riccardo Rosati

In spite of the importance of identification mechanisms in ontology engineering, the Description Logics at the basis of current reasoners do not include modeling features for expressing identification constraints. In this paper, we consider a powerful class of identification constraints, which allow for using roles, inverses, and paths, thus capturing sophisticated forms of identifications often needed in real-world applications. We show that, when used with no limitations, such path-based identification constraints are problematic with respect to effectiveness/efficiency of reasoning. We then propose a restricted form of these constraints, called local, requiring that at least one of the component paths of the concept identifier is a direct property of the concept. We argue that such a restriction is not a severe limitation in practice, and we show that local path-based identification constraints do not increase the complexity of reasoning both in very expressive Description Logics and in the tractable DL-Lite family.

ICAPS Conference 2008 Conference Paper

Realizing Multiple Autonomous Agents through Scheduling of Shared Devices

  • Sebastian Sardiña
  • Giuseppe De Giacomo

Imagine a collection of available devices, such as a camera, a vacuum cleaner, or robotic arm, each of which is able to act (that is, perform actions) according to a given behavior specification, expressed as a finite transition system. Imagine next a set of virtual independent and autonomous agents, such as a surveillance agent or a cleaning agent, which are meant to operate concurrently, each within a given specification of its capabilities, again expressed as a finite transition system. The question then is: can we guarantee the realization of every agent by intelligently scheduling the available devices while fully preserving the agents' autonomy? In this paper, we define the problem formally, and propose a technique to actually generate a solution by appealing to recent results in LTL-based synthesis of reactive systems. We also show that the proposed technique is optimal with respect to computational complexity.

KR Conference 2008 Conference Paper

View-Based Query Answering over Description Logic Ontologies

  • Diego Calvanese
  • Giuseppe De Giacomo
  • Maurizio Lenzerini
  • Riccardo Rosati

View-based query answering is the problem of answering a query based only on the answers precomputed for a set of views. While this problem has been widely investigated in databases, it is largely unexplored in the context of Description Logic ontologies. Differently from traditional databases, Description Logics may express several forms of incomplete information, and this poses challenging problems in characterizing the semantics of views. In this paper, we first present a general framework for view-based query answering, where we address the above semantical problems by defining a spectrum of notions of view-based query answering over ontologies, all based on the idea that the precomputed answers to views are the certain answers to the corresponding queries. We also relate such notions to relevant issues in ontology management, in particular ontology access authorization. Then, we provide decidability results, algorithms, and data complexity characterizations for view-based query answering in several Description Logics, ranging from the DL-Lite family to very expressive Description Logics.

IJCAI Conference 2007 Conference Paper

  • Giuseppe De Giacomo
  • Sebastian Sardina

We consider the problem of synthesizing a fully controllable target behavior from a set of available partially controllable behaviors that are to execute within a shared partially predictable, but fully observable, environment. Behaviors are represented with a sort of nondeterministic transition systems, whose transitions are conditioned on the current state of the environment, also represented as a nondeterministic finite transition system. On the other hand, the target behavior is assumed to be fully deterministic and stands for the behavior that the system as a whole needs to guarantee. We formally define the problem within an abstract framework, characterize its computational complexity, and propose a solution by appealing to satisfiability in Propositional Dynamic Logic, which is indeed optimal with respect to computational complexity. We claim that this problem, while novel to the best of our knowledge, can be instantiated to multiple specific settings in different contexts and can thus be linked to different research areas of AI, including agent-oriented programming and cognitive robotics, control, multi-agent coordination, plan integration, and automatic web-service composition.

IJCAI Conference 2007 Conference Paper

  • Diego Calvanese
  • Giuseppe De Giacomo
  • Domenico Lembo
  • Maurizio Lenzerini
  • Riccardo Rosati

Querying Description Logic knowledge bases has received great attention in the last years. In such a problem, the need of coping with incomplete information is the distinguishing feature with respect to querying databases. Due to this feature, we have to deal with two conflicting needs: on the one hand, we would like to query the knowledge base with sophisticated mechanisms provided by full first-order logic (FOL); on the other hand, the presence of incomplete information makes query answering a much more difficult task than in databases. In this paper we advocate the use of a nonmonotonic epistemic FOL query language as a means for expressing sophisticated queries over Description Logic knowledge bases. We show that through a controlled use of the epistemic operator, resulting in the language called EQL-Lite, we are able to formulate full FOL queries over Description Logic knowledge bases, while keeping computational complexity of query answering under control. In particular, we show that EQL-Lite queries over DL-Lite knowledge bases are FOL reducible (i. e. , compilable into SQL) and hence can be answered in LOGSPACE through standard database technologies.

AAAI Conference 2007 Conference Paper

On the Approximation of Instance Level Update and Erasure in Description Logics

  • Giuseppe De Giacomo
  • Antonella Poggi

A Description Logics knowledge base is constituted by two components, called TBox and ABox, where the former expresses general knowledge about the concepts and their relationships, and the latter describes the properties of instances of concepts. We address the problem of how to deal with changes to a Description Logic knowledge base, when these changes affect only its ABox. We consider two types of changes, namely update and erasure, and we characterize the semantics of these operations on the basis of the approaches proposed by Winslett and by Katsuno and Mendelzon. It is well known that, in general, Description Logics are not closed with respect to updates, in the sense that the set of models corresponding to an update applied to a knowledge base in a Description Logic L may not be expressible by ABoxes in L. We show that this is true also for erasure. To deal with this problem, we introduce the notion of best approximation of an update (erasure) in a DL L, with the goal of characterizing the L ABoxes that capture the update (erasure) at best. We then focus on DL-LiteF, a tractable Description Logic, and present polynomial algorithms for computing the best approximation of updates and erasures in this logic, which shows that the nice computational properties of DL-LiteF are retained in dealing with the evolution of the ABox.

KR Conference 2006 Conference Paper

Data Complexity of Query Answering in Description Logics

  • Diego Calvanese
  • Giuseppe De Giacomo
  • Domenico Lembo
  • Maurizio Lenzerini
  • Riccardo Rosati

In this paper we study data complexity of answering conjunctive queries over Description Logic knowledge bases constituted by an ABox and a TBox. In particular, we are interested in characterizing the FOL-reducibility and the polynomial tractability boundaries of conjunctive query answering, depending on the expressive power of the Description Logic used to specify the knowledge base. FOL-reducibility means that query answering can be reduced to evaluating queries over the database corresponding to the ABox. Since first-order queries can be expressed in SQL, the importance of FOL-reducibility is that, when query answering enjoys this property, we can take advantage of Data Base Management System (DBMS) techniques for both representing data, i. e., ABox assertions, and answering queries via reformulation into SQL. What emerges from our complexity analysis is that the Description Logics of the DL-Lite family are the maximal logics allowing conjunctive query answering through standard database technology. In this sense, they are the first Description Logics specifically tailored for effective query answering over very large ABoxes.

KR Conference 2006 Conference Paper

On the Limits of Planning over Belief States under Strict Uncertainty

  • Sardina Sebastian
  • Hector Levesque
  • Giuseppe De Giacomo
  • Yves Lesperance

A recent trend in planning with incomplete information is to model the actions of a planning problem as nondeterministic transitions over the belief states of a planner, and to search for a plan that terminates in a desired goal state no matter how these transitions turn out. We show that this view of planning is fundamentally limited. Any plan that is successful by this criteria has an upper bound on the number of actions it can execute. Specifically, the account will not work when iterative plans are needed. We also show that by modifying the definition slightly, we obtain another account of planning that does work properly even for iterative plans. Although the argument is presented in an abstract form, we illustrate the issues using a simple concrete example.

AAAI Conference 2006 Conference Paper

On the Update of Description Logic Ontologies at the Instance Level

  • Giuseppe De Giacomo
  • Antonella Poggi

We study the notion of update of an ontology expressed as a Description Logic knowledge base. Such a knowledge base is constituted by two components, called TBox and ABox. The former expresses general knowledge about the concepts and their relationships, whereas the latter describes the state of affairs regarding the instances of concepts. We investigate the case where the update affects only the instance level of the ontology, i. e. , the ABox. Building on classical approaches on knowledge base update, our first contribution is to provide a general semantics for instance level update in Description Logics. We then focus on DL-Lite, a specific Description Logic where the basic reasoning tasks are computationally tractable. We show that DL-Lite is closed with respect to instance level update, in the sense that the result of an update is always expressible as a new DL-Lite ABox. Finally we provide an algorithm that computes the result of an update in DL-Lite, and we show that it runs in polynomial time with respect to the size of both the original knowledge base and the update formula.

AAAI Conference 2005 System Paper

QuOnto: Querying Ontologies

  • Andrea Acciarri
  • Giuseppe De Giacomo
  • Maurizio Lenzerini

In this work, we present QUONTO, a query answering system based on DL-Lite. Our system provides three basic functionalities: (1) specification of the intensional level of the ontology (TBox), (2) specification of the extensional level of the ontology (ABox), and (3) query answering.

AAAI Conference 2004 Conference Paper

Scaling Up Reasoning about Actions Using Relational Database Technology

  • Giuseppe De Giacomo
  • Toni Mancini

Reiter’s variant of the Situation Calculus is tightly related to relational databases, when complete information on the initial situation is available. In particular, the information on the initial situation can be seen as a relational database, and actions, as specified by the preconditions and successor state axioms, can be seen as operations that change the state of the database. In this paper, we show how to exploit such a correspondence to build systems for reasoning about actions based on standard relational database technology. Indeed, by exploiting standard relational DBMS services, a system may be able to perform both Projection, exploiting DBMS querying services, and Progression, exploiting DBMS update services, in very large action theories. A key result towards such a realization, is that under very natural conditions Reiter’s basic action theories turn out to be made of “safe formulas” (where basically negation is used as a form of difference between predicates only) and that regression and progression preserve such a safeness. This is a fundamental property to efficiently exploit relational database technology for reasoning. We then show that, even when action theories are not “safe”, they can be made so while trying to retain efficiency as much as possible. Finally, we briefly discuss how such results can be extended to certain forms of incomplete information.

KR Conference 2004 Conference Paper

What to Ask to a Peer: Ontology-based Query Reformulation

  • Diego Calvanese
  • Giuseppe De Giacomo
  • Domenico Lembo
  • Maurizio Lenzerini
  • Riccardo Rosati

In the recent years, the issue of cooperation, integration, and coordination between information peers in a networked environment has been addressed in different contexts, including data integration, the Semantic Web, Peer-to-Peer and Grid computing, service-oriented computing and distributed agent systems. One of the main problems that arises in such systems is how to exploit the mappings between peers in order to answer queries posed to one peer. The goal of this paper is to present some basic, fundamental results on this problem. In particular, we focus on a simplified setting based on just two interoperating peers and we investigate how to solve the so-called ``What-To-Ask'' problem: find a way to answer queries posed to a peer by relying only on the query answering service available at the queried peer and at the other peer. We show that a solution to this problem exists in the case of peers based on a basic ontology language and provide an algorithm to compute it. We also show that, by slightly enriching the ontology language, the problem may become unsolvable.

IJCAI Conference 1999 Conference Paper

Projection using Regression and Sensors

  • Giuseppe De Giacomo
  • Hector J. Levesque

In this paper, we consider the projection task (determining what does or does not hold after performing a sequence of actions) in a general setting where a solution to the frame problem may or may not be available, and where online information from sensors may or may not be applicable. We formally characterize the projection task for actions theories of this sort, and show how a generalized form of regression produces correct answers whenever it can be used. We characterize conditions on action theories, sequences of actions, and sensing information that are sufficient to guarantee that regression can be used, and present a provably correct regressionbased procedure in Prolog for performing the task under these conditions.

IJCAI Conference 1999 Conference Paper

Reasoning in Expressive Description Logics with Fixpoints based on Automata on Infinite Trees

  • Diego Calvanese
  • Giuseppe De Giacomo
  • Maurizio Lenzerini

In the last years, the investigation on Description Logics (DLs) has been driven by the goal of applying them in several areas, such as, software engineering, information systems, databases, information integration, and intelligent access to the web. The modeling requirements arising in the above areas have stimulated the need for very rich languages, including fixpoint constructs to represent recursive structures. We study a DL comprising the most general form of fixpoint constructs on concepts, all classical concept forming constructs, plus inverse roles, n-ary relations, qualified number restrictions, and inclusion assertions. We establish the EXPTIME decidability of such logic by presenting a decision procedure based on a reduction to nonemptiness of alternating automata on infinite trees. We observe that this is the first decidability result for a logic combining inverse roles, number restrictions, and general fixpoints.

IJCAI Conference 1995 Conference Paper

What's in an Aggregate: Foundations for Description Logics with Tuples and Sets

  • Giuseppe De Giacomo
  • Maurizio Lenzerini

Based on the research done in the last decade, attempts have been made to propose description logics as unifying formalisms for the various class-based representation languages used in different areas. These attempts have made apparent that sound, complete, and decidable description logics still suffer from several limitations, regarding modeling classes of aggregate objects, expressing general inclusion axioms, and the ability of navigating links between classes. In this paper we make description logics accomplish the necessary leap in order to become suitable for the new challenging applications they are faced with. In particular, we propose a powerful description logic overcoming the above limitations and we show that its reasoning tasks are decidable in worst case exponential time.

AAAI Conference 1994 Conference Paper

Boosting the Correspondence between Description Logics and Propositional Dynamic Logics

  • Giuseppe De Giacomo

One of the main themes in the area of Terminological Reasoning has been to identify description logics (DLs) that are both very expressive and decidable. A recent paper by Schild showed that this issue can be profitably addressed by relying on a correspondence between DLs and propositional dynamic logics (PDL). However Schild left open three important problems, related to the translation into PDLs of functional restrictions on roles (both direct and inverse), number restrictions, and assertions on individuals. The work reported in this paper presents a solution to these problems. The results have a twofold significance. From the standpoint of DLs, we derive decidability and complexity results for some of the most expressive logics appeared in the literature, and from the standpoint of PDLs, we derive a general methodology for the representation of several forms of program determinism and for the specification of partial computations.

LOPSTR Conference 1993 Conference Paper

Intensional Query Answering: An Application of Partial Evaluation

  • Giuseppe De Giacomo

Abstract We consider intensional answers to be logical formulas expressing sufficient conditions for objects to belong to the usual answer to a query addressed to a knowledge base. We show that in the SLDNF-resolution framework, complete and procedurally complete sets of intensional answers can be generated by using partial evaluation. Specific treatments of recursion and negation are also presented.