Online Synthesis for Runtime Enforcement of Safety in Multi-Agent Systems

TL;DR

This paper introduces a decentralized, runtime shield synthesis method for multi-agent systems that ensures safety without requiring global information, significantly improving scalability over traditional design-time approaches.

Contribution

It presents a novel decentralized approach where each agent has an onboard shield that operates at runtime, reducing complexity from exponential to quadratic in the number of agents.

Findings

Runtime synthesis is efficient for 50 agents, taking seconds per agent.

Centralized design-time synthesis becomes intractable beyond 4 agents.

The method guarantees safety with bounded deviation from original behavior.

Abstract

A shield is attached to a system to guarantee safety by correcting the system's behavior at runtime. Existing methods that employ design-time synthesis of shields do not scale to multi-agent systems. Moreover, such shields are typically implemented in a centralized manner, requiring global information on the state of all agents in the system. We address these limitations through a new approach where the shields are synthesized at runtime and do not require global information. There is a shield onboard every agent, which can only modify the behavior of the corresponding agent. In this approach, which is fundamentally decentralized, the shield on every agent has two components: a pathfinder that corrects the behavior of the agent and an ordering mechanism that dynamically modifies the priority of the agent. The current priority determines if the shield uses the pathfinder to modify behavior of the agent. We derive an upper bound on the maximum deviation for any agent from its original behavior. We prove that the worst-case synthesis time is quadratic in the number of agents at runtime as opposed to exponential at design-time for existing methods. We test the performance of the decentralized, runtime shield synthesis approach on a collision-avoidance problem. For 50 agents in a 50x50 grid, the synthesis at runtime requires a few seconds per agent whenever a potential collision is detected. In contrast, the centralized design-time synthesis of shields for a similar setting is intractable beyond 4 agents in a 5x5 grid.