Synthesis Under Environment Specifications for LTLf

In recent years, (Reactive) Synthesis has emerged as a powerful framework 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 winning strategy. In this dissertation, we advance the state of the art regarding the reasoning capabilities of autonomous agents based on reactive synthesis for specifications in Linear Temporal Logic on finite traces (LTLf). Specifically, we extend reactive synthesis techniques to address some of 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 best-effort strategy that guarantees that it will do its best to achieve the goal. We provide three symbolic approaches to LTLf best-effort synthesis based on those employed in LTLf synthesis. These approaches base on the same core components, but differ in how these components are combined, which has a significant impact on their performance. This is confirmed by our empirical evaluations, which also show that best-effort synthesis is suited for efficient and scalable implementations: it brings a minimal overhead compared to standard reactive synthesis. Subsequently, we study the relation of best-effort strategies with responsibility notions studied in the field of responsibility analysis. In fact, this relation comes in the form of a strong result that can be summarized as follows: the agent should always use a best-effort strategy to avoid being held liable of bad outcomes that may occur during execution and prevent these outcomes at all, if possible. Based on this relation, we present a strong computational grounding of responsibility that uses strategy notions studied in LTLf synthesis: it establishes computational complexity and provides sound and complete algorithms to assess various forms of responsibility. Finally, we investigate best-effort synthesis directly in the context of Fully Observable Nondeterministic (FOND) domains -- state-based models of the world where the effects of agent actions are nondeterministically chosen by the environment. Specifically, we present a sound, complete and optimal (wrt computational complexity) best-effort synthesis algorithm that exploits the specificity of FOND domains as environment specifications. Our empirical evaluation shows its effectiveness experimentally: it exhibits greater scalability compared to a direct approach based on re-expressing the domain as generic LTLf environment specifications. The second challenge 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? Here, we devise an effective approach to best-effort synthesis in multi-tier environments -- a form of synthesis that concerns computing a strategy that ensures that the agent does its best to achieve the goal while considering several environment models (aka tiers) simultaneously. The algorithm we present is based on combining on-the-fly the solutions of various synthesis problems, each obtained from the goal and a single environment tier. This algorithm is only linear -- instead of exponential~-- in the number of environment tiers: it scales efficiently to multi-tier environments formed of several tiers. The third challenge we consider is adaptability during strategy execution: how should an agent adapt its behavior during strategy execution when its specification changes? To address this challenge, we study incremental LTLf synthesis -- a form of synthesis where the goals are given incrementally while in execution. The setting is as follows: the agent is executing a strategy for a certain goal and, at a certain point, a new goal arrives. At this point, the agent has to abandon the current strategy and synthesize a new strategy still fulfilling the original goal, which was given at the beginning, as well as the new goal, starting from the current instant. We propose a solution algorithm that efficiently performs incremental synthesis for multiple LTLf goals by leveraging auxiliary data structures constructed during automata-based synthesis. Furthermore, we consider an alternative solution algorithm -- which can be seen as a form of replanning from scratch -- based on LTLf formula progression. We show experimentally that this latter algorithm is not competitive with our automata-based solution, which exhibits better scalability and performance. As a final challenge, we consider scalability of synthesis for infinite-time specifications. Specifically, we consider infinite-time specifications in LTLf+ -- a formalism for expressing temporal properties over infinite-time horizons based on LTLf and the Manna-Pnueli hierarchy. The question we aim to address is: can we extend the symbolic framework at the base of LTLf synthesizers to do LTLf+ synthesis? In this dissertation, we present the first actual solvers for reactive synthesis in LTLf+. 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 based on composing the solutions to 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.