Verificación de Evitación de Colisiones de Sistemas Multiagente con Políticas Aprendidas

Para muchos problemas de control multiagente, las redes neuronales (NNs) han habilitado nuevas capacidades prometedoras. Sin embargo, muchos de estos sistemas carecen de garantías formales (por ejemplo, evitación de colisiones, robustez), lo que impide aprovechar estos avances en entornos críticos para la seguridad. Aunque hay trabajos recientes sobre verificación formal de sistemas controlados por NN, la mayoría de las técnicas existentes no pueden manejar escenarios con más de un agente. Para abordar esta brecha de investigación, este documento presenta un enfoque basado en la alcanzabilidad inversa para verificar las propiedades de evitación de colisiones de los Bucles de Retroalimentación Neural Multiagente (MA-NFLs). Dados los modelos de dinámica y las políticas de control entrenadas de cada agente, el algoritmo propuesto calcula conjuntos de retroproyección relativa resolviendo (simultáneamente) una serie de Programas Lineales Mixtos Enteros (MILPs) fuera de línea para cada par de agentes. Consideramos las incertidumbres de medición de estado, lo que lo alinea bien con escenarios del mundo real. Usando esos resultados, los agentes pueden verificar rápidamente la evitación de colisiones en línea resolviendo Programas Lineales (LPs) de baja dimensión. Demostramos que el algoritmo propuesto puede verificar propiedades libres de colisiones de un MA-NFL con agentes entrenados para imitar un algoritmo de evitación de colisiones (Obstáculos de Velocidad Recíproca). Además, demostramos la escalabilidad computacional del enfoque en sistemas con hasta 10 agentes.