NATIONAL PHD IN ARTIFICIAL INTELLIGENCE

Thesis title: Synthesis Under Environment Specifications for LTLf

In recent years, (Reactive) Synthesis has emerged as a powerful tool for the development of autonomous AI agents: given a specification of its goal and of the environment in which it operates, the agent must compute a strategy that ensures the satisfaction of the goal regardless of the behavior of the external environment -- called a \emph{winning strategy}. In this dissertation, we advance the state of the art regarding the reasoning capabilities of autonomous agent based on reactive synthesis. Specifically, we extend reactive synthesis techniques to address the challenges that autonomous agents face while deliberating on how to achieve their goals. The first challenge that we consider is synthesis unrealizability: how should the agent act when there is no strategy that satisfies the goal regardless of how the external environment behaves? A solution has been proposed in the form of best-effort synthesis -- a generalization of reactive synthesis that captures the intuition that, when a winning strategy does not exist, the agent should use a strategy that guarantees that it will do its best to achieve the goal, called a best-effort strategy. In this dissertation, we provide symbolic approaches to LTLf best-effort synthesis inspired by those adopted in model checking and LTLf synthesis. We also study the connection of best-effort strategies with responsibility notions studied in the field of responsibility analysis. Finally, we define and solve best-effort synthesis directly in the context of Fully Observable Nondeterministic (FOND) Domains. The second challenge that we consider is uncertainty about the environment model: how should an agent act when is it hard to model the environment in which the agent operates using a single specification? In this context, we present algorithms for best-effort synthesis in multi-tier environment that compute a strategy that ensures that the agent does its best to achieve the goal while considering several environment models simultaneously. The third challenge that we consider is adaptability during strategy execution: how should an agent adapt its behavior during strategy execution when its specification changes? Consider an agent that is executing a strategy for a certain goal and that, at a certain point, a new goal arrives. In this setting, we introduce and solve incremental LTLf synthesis. The algorithms that we provide ensure that both the original and new goal are satisfied taking into account what has been observed during execution. Finally, recent work showed that, while LTLf is a formalism for expressing temporal properties over finite time-horizons, it can also be used to synthesize strategies for the infinite setting by using LTLf+ synthesis. Then, can we extend the symbolic framework at the base of LTLf synthesizers to do LTLf+ synthesis? We answer affirmatively by providing symbolic LTLf+ synthesis algorithms based on Emerson-Lei automata that perform and scale well.