Safe Multi-agent Reinforcement Learning Using Formal Runtime Enforcement: A Case Study.

Cyber-Physical Systems (CPSs) are increasingly used in safety-critical tasks like search and rescue missions. They are often combined with machine-learning algorithms like Reinforcement Learning (RL) for improved performance and accuracy. There is a pressing need to ensure the safety of such learning-enabled CPSs. In recent research, the Runtime Enforcement (RE) approach has been very successful in formally ensuring the safety of learning-enabled CPS. RE is a formal verification technique that dynamically guarantees the safety of a system. We present a runtime enforcement mechanism for safeguarding a Multi-Agent Reinforcement Learning (MARL) enabled drone swarm CPS. We discuss the enforcement strategies that prevent drones from collision and boundary breach. We show how RE combined with MARL, in addition to guaranteeing safety, improves the overall performance of the swarm system.