Online Synthesis for Runtime Enforcement of Safety in Multiagent Systems

We study the problem of enforcing safety in multiagent systems at runtime by modifying the system behavior if a potential safety violation is detected. Traditional runtime enforcement methods that solve a reactive synthesis problem at design time have two significant drawbacks. First, these techniques do not scale as one has to take into account all possible behaviors from every agent, and this is computationally prohibitive. Second, these approaches require every agent to know the state of every other agent. We address these limitations through a new approach where online modifications to behavior are synthesized onboard every agent. There is an enforcer onboard every agent, which can modify the behavior of only the corresponding agent. In this approach, which is naturally decentralized, the enforcer on every agent has two components: 1) a pathfinder that corrects the behavior of the agent and 2) an ordering mechanism that dynamically modifies the priority of the agent. The current priority of an agent determines if the enforcer uses the pathfinder to modify the behavior of the agent. We derive an upper bound on the maximum deviation for any agent from its original behavior; that is, all agents make progress. 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 the existing methods that rely on design-time computation merely. Additionally, we prove the completeness of the technique under some mild assumptions; that is, if the agents can progress safely, then enforcers will find this behavior. We test the technique in collision avoidance scenarios. For 50 agents in a 50 × 50 grid world modeling the common workspace for the agents, the online synthesis requires only 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 four agents in a 5 × 5 grid world.