Layered controller synthesis for dynamic multi-agent systems

TL;DR

This paper introduces a layered multi-agent control synthesis method combining high-level planning, SMT-based refinement, and neural network reinforcement learning to create real-time executable policies.

Contribution

It presents a novel layered approach integrating formal methods and machine learning for multi-agent control synthesis.

Findings

The high-level plan effectively guides the detailed control synthesis.

Reinforcement learning improves real-time control performance.

Initial datasets from formal methods are crucial for training success.

Abstract

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.