Golog programs over Situation Calculus action theories were introduced as a specification of desired agent behavior, very much like temporally extended goals in planning, but with a focus on procedural aspects typical of programs. In the words of the original paper: "Golog allows the programmer to strike a compromise between the often computationally infeasible classical planning task, in which a plan must be deduced entirely from scratch, and detailed programming, in which every little step must be specified." In this paper, we study temporal synthesis with Golog programs as specifications over nondeterministic propositional action theories. We show that Golog has the same expressive power as linear dynamic logics on finite traces (LDLf), namely that of regular languages or monadic second-order logic (MSO) over finite traces, while exhibiting a markedly lower synthesis complexity: synthesis can be performed by constructing a polynomial-size program graph and taking its cross-product with the domain, whereas LDLf synthesis requires building a deterministic automaton of worst-case doubly exponential size. This advantage is confirmed experimentally.

Autonomous agents' goals typically change as they operate. Handling this is particularly challenging when the environment is nondetermnistic and the goals are temporally extended. In this paper, we assume that the agent operates in a fully observable nondeterministic (FOND) domain and uses Linear Temporal Logic over finite traces (LTLf) to represent goals. We use LTLf synthesis notions to formalize this problem of online agent goal management, handling goal adoption, goal dropping, and performing steps of the synthesized strategy, while ensuring that the agent's goals always remain realizable. We propose automata-based and formula progression-based methods to manage LTLf goals. We implement these methods and evaluate their effectiveness experimentally.

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.

We study a variant of LTLf synthesis that synthesizes adaptive strategies for achieving a multi-tier goal, consisting of multiple increasingly challenging LTLf objectives in nondeterministic planning domains. Adaptive strategies are strategies that at any point of their execution (i) enforce the satisfaction of as many objectives as possible in the multi-tier goal, and (ii) exploit possible cooperation from the environment to satisfy as many as possible of the remaining ones. This happens dynamically: if the environment cooperates (ii) and an objective becomes enforceable (i), then our strategies will enforce it. We provide a game-theoretic technique to compute adaptive strategies that is sound and complete. Notably, our technique is polynomial, in fact quadratic, in the number of objectives. In other words, it handles multi-tier goals with only a minor overhead compared to standard LTLf synthesis.

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.

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.

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.

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.