Specifying Agent Strategy Spaces via LTL Synthesis

We study a model of Agentic AI, building on LTL synthesis originally studied in formal methods, that consists of autonomous agents with independent sequential decision-making capabilities. Specifically, we associate with each agent a goal expressed in LTL, and assumptions on the strategies employed by its peers and that the agent can exploit while synthesizing a strategy to realize its goal. While we can solve the synthesis problem under assumptions for each such agent we are not only interested in (1) synthesizing strategies for individual agents. Indeed, assumptions in turn are recursively defined through these strategy spaces. Importantly, we do not assume the ability to access or analyze an agent's internal strategy, as we make no assumptions about the nature of the decision makers, which may be, for example, ML-based. Instead, we focus on (2) characterizing the set of traces that are generated by strategies that realize the specification assigned to each agent. Using this characterization, we are able to (3) verify that the whole system, when in execution, satisfies a global objective, regardless of the strategies chosen by the agents from their allowed spaces. Moreover, by observing the evolution of the execution trace, we can (4) identify whether an agent makes a move that violates its specification and assign precise responsibility for the violation. Technically, we present automata-theoretic techniques to solve these problems, and show that each of them is 2EXPTIME-complete, matching the complexity of classical LTL synthesis.