Real-Time Model Checking for Closed-Loop Robot Reactive Planning

Planteamiento del Problema
Los métodos de evitación de obstáculos reactivos, como los utilizados en los vehículos de Braitenberg o en los robots de limpieza comerciales, suelen depender de un razonamiento de un solo paso (estímulo-respuesta). Aunque son efectivos para reflejos simples, estos métodos frecuentemente provocan que los agentes queden atrapados en mínimos locales, particularmente en entornos cóncavos como esquinas o callejones sin salida. Esto ocurre porque el agente no puede predecir las consecuencias de sus acciones inmediatas sobre estados futuros. En contextos de misión crítica, como la exploración espacial remota o la conducción autónoma, esta limitación puede conducir a fallos catastróficos. Además, los populares métodos de IA de caja negra, como el Aprendizaje por Refuerzo Profundo (DRL), a menudo carecen de transparencia y dependen de generalizaciones rígidas que pueden fallar en entornos no estructurados y no vistos. Si bien la Verificación de Modelos (MC) es una técnica robusta para verificar sistemas críticos para la seguridad, su aplicación a la planificación en tiempo real en robots físicos se ha visto limitada por altos costes computacionales, retrasos de compilación y el problema de la "explosión del espacio de estados". Los intentos actuales de MC en tiempo real suelen depender de herramientas genéricas (por ejemplo, SPIN) que introducen una latencia inaceptable (segundos) para la navegación de alta velocidad.

Metodología
Los autores proponen un algoritmo de verificación de modelos a medida, simplificado y diseñado para integrarse directamente en el código del robot para permitir una planificación reactiva de múltiples pasos en tiempo real. El enfoque se fundamenta en el concepto biológico de "ensayo y error vicario", donde un agente simula acciones futuras para predecir resultados.

• Arquitectura y Abstracción: El sistema utiliza una perspectiva egocéntrica, tratando los obstáculos como "perturbaciones" que interrumpen una acción predeterminada preferida (conducir recto). En lugar de mantener un mapa global, el robot construye instantáneas abstractas temporales de su entorno inmediato. Estas instantáneas se centran estrictamente en las relaciones espaciales relevantes para evitar la explosión del espacio de estados.
• Sistema de Transición Enfocado en Perturbaciones (DTS): El núcleo del método es un sistema de transición finito con 15 estados que representan posibles configuraciones futuras relativas al marco local del robot. Los estados codifican conocimiento "núcleo" sobre la evolución temporal de tareas de bucle cerrado (por ejemplo, rotar a la izquierda/derecha, conducir recto). El sistema modela secuencias de tareas (planes de 2, 3 y 4 pasos) para determinar si un robot puede regresar de forma segura a su estado por defecto tras evitar una perturbación.
• Planificación Basada en LTL: En lugar de verificar un sistema contra una propiedad, los autores utilizan una propiedad de trayectoria de Lógica Temporal Lineal (LTL) negada. Definen una propiedad $\varphi = \neg(\text{safe} \mathcal{U} (\text{safe} \land \text{horizon}))$. Al buscar contraejemplos a esta propiedad negada, el verificador de modelos genera "rutas de solución" válidas (secuencias seguras de tareas) que conducen a un estado donde el robot puede conducir indefinidamente sin perturbaciones.
• Ejecución en Tiempo de Ejecución: El algoritmo se ejecuta en hardware de baja potencia (por ejemplo, Raspberry Pi 3). Utiliza una búsqueda de profundidad hacia adelante (f-DFS) en el producto del sistema de transición y un Autómata Finito No Determinista (NFA) derivado de la propiedad LTL. El sistema prioriza planes cortos (2 pasos) y solo se expande a planes de 3 o 4 pasos si las secuencias más cortas se consideran inseguras (por ejemplo, si el robot está "encajonado" por obstáculos a ambos lados).

Contribuciones Clave

1. Algoritmo de Verificación de Modelos a Medida: Desarrollo de un algoritmo de verificación de modelos ligero y personalizado, diseñado para la ejecución en tiempo real en dispositivos con recursos limitados, evitando la sobrecarga de los verificadores de propósito general.
2. Integración Directa: Integración exitosa del verificador de modelos directamente en el bucle de control del robot (C++), eliminando los retrasos de precompilación y permitiendo un rendimiento de tiempo real estricto.
3. Mitigación del Espacio de Estados: Una estrategia de abstracción novedosa que utiliza instantáneas ambientales temporales y un enfoque de atención estricto en las perturbaciones para prevenir la explosión del espacio de estados.
4. Planificación de Contraejemplos: Utilización de propiedades LTL negadas para generar planes de evitación de obstáculos de múltiples pasos como contraejemplos, contrastando con los enfoques de verificación tradicionales.
5. Validación Empírica: Demostración del enfoque en un robot físico en entornos no estructurados, mostrando un rendimiento superior frente a las líneas base reactivas de un solo paso.

Resultados
Los autores evaluaron su método frente a un controlador reactivo de línea base en dos escenarios: un callejón sin salida y un entorno de parque con un obstáculo independiente.

• Escenario de Callejón sin Salida (Cuantitativo): En un estudio de 90 ejecuciones, el enfoque de verificación de modelos generó trayectorias significativamente más cortas (comparación de rango de la mediana, $p < .001$) y resultó en cero colisiones, mientras que el método de la línea base sufrió 3 colisiones y frecuentemente quedó atrapado. La latencia de procesamiento para el enfoque de verificación de modelos osciló entre 5.58 ms y 18.76 ms (media ~10.1 ms), dentro del plazo de 100 ms en tiempo real. El uso de memoria fue mínimo (372 bytes para el verificador propiamente dicho).
• Escenario de Parque (Cualitativo): En pruebas de libre movimiento, el método de la línea base revisitó repetidamente y quedó atrapado en el callejón sin salida (sumando un total de 89–168 segundos de atrapamiento en las ejecuciones) y causó 6 colisiones. El enfoque de verificación de modelos evitó con éxito el callejón sin salida por completo, con cero colisiones y cero tiempo de atrapamiento.
• Validación Multiplataforma: El método fue probado con éxito en una segunda plataforma de robot (Radxa Rock 5B) con hardware LiDAR diferente, confirmando su portabilidad.
• Garantías Teóricas: Los autores proporcionan pruebas informales que demuestran que, bajo supuestos de entorno estático y ruido de sensor acotado, el método evita estructuralmente que el robot alterne indefinidamente entre giros a la izquierda y a la derecha (quedar atrapado en una esquina) y asegura que las perturbaciones no entren en la zona segura definida durante la ejecución en línea recta.

Significancia y Reivindicaciones
El artículo afirma que este enfoque ofrece un "reemplazo directo" para la evitación de obstáculos puramente reactiva en aplicaciones críticas para la seguridad como vehículos autónomos y robots móviles. A diferencia del DRL, que depende de un entrenamiento opaco y de gran consumo de datos y lucha con entornos no estructurados, este método proporciona un proceso de razonamiento explicable basado en reglas que simula resultados futuros basados en la entrada sensorial inmediata. Los autores enfatizan que su método cumple con las restricciones de tiempo real estricto en hardware de baja potencia, lo que lo hace eficiente energéticamente y adecuado para su despliegue donde no se dispone de hardware acelerado costoso. Si bien la implementación actual se centra en la evitación local de obstáculos en lugar de la navegación dirigida a un objetivo, los autores lo postulan como un paso fundamental hacia la integración de la verificación formal con la descomposición jerárquica para una navegación autónoma segura, fiable y transparente.