Layered controller synthesis for dynamic multi-agent systems
This addresses real-time control challenges in dynamic multi-agent systems, offering an incremental improvement by combining formal methods with learning.
The paper tackles the multi-agent control problem by decomposing it into three stages, using a SWA-SMT solver for correct-by-construction planning and then training a neural network policy with reinforcement learning, showing that the initial dataset from the solver is crucial for success.
In this paper we present a layered approach for multi-agent control problem, decomposed into three stages, each building upon the results of the previous one. First, a high-level plan for a coarse abstraction of the system is computed, relying on parametric timed automata augmented with stopwatches as they allow to efficiently model simplified dynamics of such systems. In the second stage, the high-level plan, based on SMT-formulation, mainly handles the combinatorial aspects of the problem, provides a more dynamically accurate solution. These stages are collectively referred to as the SWA-SMT solver. They are correct by construction but lack a crucial feature: they cannot be executed in real time. To overcome this, we use SWA-SMT solutions as the initial training dataset for our last stage, which aims at obtaining a neural network control policy. We use reinforcement learning to train the policy, and show that the initial dataset is crucial for the overall success of the method.