FormIDEAble: Safe and Socially-aware Autonomous Systems

Resumen Técnico de FormIDEAble: Sistemas Autónomos Seguros y Socialmente Conscientes

Planteamiento del Problema
Los agentes autónomos que operan en entornos sociocríticos (por ejemplo, respuesta ante emergencias) deben coordinarse con humanos bajo condiciones de incertidumbre mientras cumplen estrictamente con restricciones de seguridad. Los enfoques existentes enfrentan una dicotomía: o bien modelan la dinámica social y el comportamiento humano sin proporcionar garantías formales de seguridad, o bien ofrecen aseguramiento formal abstrayendo el complejo comportamiento humano. Además, aunque la "Arquitectura de Identidad para Sistemas Autónomos" (IDEA) aprovecha la teoría de la identidad social para fomentar la cooperación, depende de un razonamiento de equilibrio que carece de garantías formales de que las restricciones de seguridad (como los límites de tiempo o la priorización de recursos) se satisfagan siempre. El desafío central es sintetizar estrategias de toma de decisiones que sean simultáneamente conscientes de lo social, formalmente verificadas y capaces de manejar la incertidumbre inherente en las respuestas humanas.

Metodología
FormIDEAble aborda este desafío modelando la interacción entre humanos y agentes autónomos como un Proceso de Decisión de Markov con Tiempo y Precios (PTMDP, por sus siglas en inglés). Este formalismo integra cuatro aspectos críticos:

1. Control: El agente autónomo selecciona entre acciones controlables.
2. Incertidumbre: Las respuestas humanas se modelan como reacciones del entorno probabilísticas e incontrolables, capturando comportamientos impulsados socialmente.
3. Tiempo: Las acciones incurren en retrasos y se imponen plazos mediante restricciones temporales.
4. Costo: Las decisiones acumulan costos que representan objetivos de desempeño (por ejemplo, tiempo de evacuación, uso de recursos).

El problema de toma de decisiones se formula como un problema de alcanzabilidad con límite de costo. El objetivo es sintetizar una estrategia $\sigma$ que minimice un costo esperado (por ejemplo, tiempo) sujeto a una restricción de seguridad: la probabilidad de alcanzar un estado objetivo $G$ (que satisface los requisitos de seguridad) dentro de un límite de costo $B$ debe exceder un umbral $p$.

El marco se implementa como un bucle MAPE-K (Monitoreo, Análisis, Planificación, Ejecución, Conocimiento):

• Monitoreo: Detecta puntos de decisión y recopila datos contextuales (distancias, disponibilidad de recursos) y estimaciones de identidad social de un "Predictor de Identidad".
• Análisis: Un "Constructor de Juegos Formales" construye un modelo PTMDP paramétrico utilizando patrones reutilizables para decisiones del controlador y decisiones adversarias (humanas), tanto observables como inobservables. Un "Solucionador de Juegos Formales" (usando Uppaal Stratego) computa la estrategia óptima.
• Planificación y Ejecución: El "Selector de la Mejor Decisión" elige la acción con la mayor probabilidad (menor costo esperado) prescrita por la estrategia, la cual es ejecutada por el agente.

Contribuciones Clave
El artículo introduce tres contribuciones principales:

1. Formalización: Una formalización de la cooperación entre humanos y agentes autónomos socialmente consciente utilizando PTMDPs, capturando explícitamente la incertidumbre de la identidad social.
2. Síntesis de Estrategia: Un enfoque novedoso que integra la incertidumbre de la identidad social con garantías de seguridad explícitas al formular el problema como un problema de alcanzabilidad con límite de costo sobre PTMDPs.
3. Evidencia Empírica: Evidencia experimental inicial que demuestra la efectividad del enfoque en un escenario de evacuación de emergencia, resaltando las compensaciones entre optimización y seguridad.

Resultados Experimentales
Los autores evaluaron FormIDEAble utilizando el entorno de simulación IMPACT+ y Uppaal Stratego contra cuatro líneas base: sin soporte, llamar siempre a los socorristas, pedir siempre ayuda a los supervivientes y el enfoque IDEA no formal.

• Desempeño vs. Líneas Base: En escenarios con recursos escasos de socorristas ($N_{fr}=9$), FormIDEable redujo significativamente el tiempo total de evacuación ($T_{evac}$) en comparación con IDEA y el soporte de solo supervivientes, manteniéndose comparable a la línea base de "llamar siempre al personal". Crucialmente, FormIDEable redujo consistentemente el número de llamadas a los socorristas en comparación con ambas líneas base de soporte de personal e IDEA.
• Predicción de Seguridad: El modelo formal demostró una alta precisión al predecir si se cumplirían los requisitos de seguridad, con precisión y exhaustividad (recall) consistentemente por encima del 93% en diversas configuraciones.
• Optimización vs. Seguridad: En los experimentos de Uppaal Stratego, FormIDEable sintetizó con éxito estrategias que minimizaban la duración de la tarea. Cuando se impusieron metas de seguridad específicas (por ejemplo, priorización de niños o limitación de llamadas a socorristas), el sistema mantuvo altas probabilidades de satisfacer estas propiedades de alcanzabilidad, a menudo a costa de un aumento modesto en la duración de la tarea.
• Sobrecarga (Overhead): La síntesis de la estrategia introdujo una sobrecarga de tiempo de ejecución (wall-clock time) no despreciable pero modesta (promediando <0.5s para configuraciones pequeñas/medianas y ~2.25s para las complejas), lo que sugiere su idoneidad para escenarios que permiten un tiempo de deliberación limitado.

Significancia y Reivindicaciones
El artículo posiciona a FormIDEable como una base fundamentada para la toma de decisiones socialmente consciente y con seguridad garantizada. Su significancia radica en cerrar la brecha entre las ciencias sociales (teoría de la identidad social) y los métodos formales (síntesis de estrategias). A diferencia del trabajo previo que trata la seguridad y la dinámica social de forma aislada, FormIDEable las integra para asegurar que los agentes autónomos puedan cooperar con humanos bajo incertidumbre sin violar restricciones de seguridad explícitas.

Los autores son modestos respecto al alcance actual, señalando que la evaluación es preliminar y depende de la simulación. Reconocen que el enfoque actualmente requiere esfuerzo manual para la instanciación del modelo y la formalización de la seguridad. El artículo afirma proporcionar los principios fundamentales de modelado y síntesis, dejando el análisis de escalabilidad integral, la validación empírica más amplia en diversos dominios sociocríticos y el desarrollo de herramientas de nivel superior para el trabajo futuro. El enfoque se presenta como un paso hacia sistemas autónomos que no solo son seguros, sino también socialmente competentes y confiables.