Paper #4 – Symbolic Reach-Avoid Control of Multi-Agent Systems

We consider the decentralized controller synthesis problem for multi-agent systems with global reach-avoid specifications. Each agent is modeled as a nonlinear dynamical system with disturbances. The objective is to synthesize local feedback controllers that guarantee that the overall multi-agent system meets the global specification despite the influence of disturbances. On the one hand, existing techniques based on planning or trajectory optimization usually ignore the effects of disturbances and produce open-loop nominal trajectories that are not generally sufficient in the presence of disturbances. On the other hand, techniques based on formal synthesis, which guarantee satisfaction of temporal specifications, do not scale as the number of agents increases.

We address these limitations by proposing a two-level solution approach that combines fast global nominal trajectory generation and local application of formal synthesis. At the top level, we ignore the effect of disturbances and obtain a joint open-loop plan for the system using a fast trajectory optimizer. At the lower level, we use abstraction-based controller design to synthesize a set of decentralized feedback controllers that track the high level plan against worst-case disturbances, thus ensuring satisfaction of the global specification.

We provide the implementation of our approach in an open-source tool called GAMARA. We demonstrate the effectiveness of GAMARA on several multi-robot examples using two particular classes of control specifications. In the first type, we assume that the robots need to fulfill their own reach-avoid tasks while avoiding collision with each other. In the second type, we require the robots to fulfill reach-avoid tasks while maintaining certain formation constraints. The experiments show that GAMARA produces formally guaranteed feedback controllers while scaling to many robots. In contrast, nominal open-loop controllers do not guarantee the satisfaction of the specification, and global formal approaches run out of memory before synthesizing a controller.