LTL Synthesis Under Multi-Agent Environment Assumptions

KR2025

Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning

Melbourne, Australia. November 11-17, 2025.

Edited by

ISSN: 2334-1033
ISBN: 978-1-956792-08-9

Benjamin Aminof(University of Rome “La Sapienza”, Italy)
Giuseppe De Giacomo(University of Oxford, United Kingdom, University of Rome “La Sapienza”, Italy)
Giuseppe Perelli(University of Rome “La Sapienza”, Italy)
Sasha Rubin(The University of Sydney, Australia)

Keywords

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.