An Abstraction-based Method To Check Multi-agent Deep Reinforcement-learning Behaviors

Abstract

Multi-agent reinforcement learning (RL) often struggles to ensure the safe behaviours of the learning agents, and therefore it is generally not adapted to safety-critical applications. To address this issue, we present a methodology that combines formal verification with (deep) RL algorithms to guarantee the satisfaction of formally-specified safety constraints both in training and testing. The approach we propose expresses the constraints to verify in Probabilistic Computation Tree Logic (PCTL) and builds an abstract representation of the system to reduce the complexity of the verification step. This abstract model allows for model checking techniques to identify a set of abstract policies that meet the safety constraints expressed in PCTL. Then, the agents' behaviours are restricted according to these safe abstract policies. We provide formal guarantees that by using this method, the actions of the agents always meet the safety constraints, and provide a procedure to generate an abst

Stats

• citations1
• S2 citations—
• github stars0
• HF likes0
• heat score2.26
• arxiv keymqirmi2021an

Related papers

• Probabilistic Model Checking Of Stochastic Reinforcement Learning Policies (2024)0.00
• Think Smart, Act SMARL! Analyzing Probabilistic Logic Shields For Multi-agent Reinforcement Learning (2024)0.00
• On Assessing The Safety Of Reinforcement Learning Algorithms Using Formal Methods (2021)0.00
• Actsafe: Active Exploration With Safety Constraints For Reinforcement Learning (2024)0.00
• Safe Multi-agent Reinforcement Learning With Convergence To Generalized Nash Equilibrium (2024)0.00
• Implicit Safe Set Algorithm For Provably Safe Reinforcement Learning (2024)0.00
• Multi-agent Constrained Policy Optimisation (2021)0.00
• Co-activation Graph Analysis Of Safety-verified And Explainable Deep Reinforcement Learning Policies (2025)0.00