Efficient control of multi-agent robust MDPs through tensor trees

This paper introduces a tensor-based framework for controller synthesis of stochastic multi-agent systems under temporal logic specifications that couple the agents, such as one agent reaching its goal only after another agent has reached its own. The agents are modeled as robust Markov decision processes (RMDPs), whose transition probabilities are only known to lie in an ambiguity set, for instance due to abstraction errors, learned models, or uncertain parameters. We show that the decoupled nature of the ambiguity sets allows one to decompose the computation of a lower bound on the satisfaction probabilities into per-agent factors, so that only the per-agent ambiguity sets need to be stored. This leads to improved memory complexity compared to monolithic approaches. We compare our approach with state-of-the-art approaches based on approximate simulation relations and with interval MDP abstractions. On a four-agent ordered reach-avoid benchmark, our approach certifies a lower bound twice as high as the simulation relation- based approach with 20 times less memory, and needs about 200 times less memory than the interval MDP abstraction, even at a resolution with about a million times more joint cells.