💻 computer science

Predictive Varanus: Combining CSP Conformance Monitoring with Predictive LTL Runtime Verification

Este artículo presenta Predictive Varanus, un proceso de verificación en tiempo de ejecución de dos etapas que combina el monitoreo de conformidad basado en CSP con el análisis predictivo de LTL para permitir la detección temprana de violaciones de seguridad en sistemas autónomos mediante el aprovechamiento de los modelos de diseño existentes.

Autores originales: Angelo Ferrando, Matt Luckcuck, Pedro Ribeiro

Publicado 2026-09-17

📖 6 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Angelo Ferrando, Matt Luckcuck, Pedro Ribeiro

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Los robots autónomos, desde los vehículos que exploran Marte hasta los drones que entregan paquetes, operan en un mundo que nunca es totalmente predecible. Incluso la máquina más cuidadosamente diseñada puede encontrarse con un fallo de sensor, un obstáculo inesperado o una situación que los ingenieros nunca imaginaron. Para mantener estos sistemas seguros, los científicos utilizan una técnica llamada verificación en tiempo de ejecución (runtime verification). Piense en ello como un copiloto vigilante que observa cada movimiento del robot en tiempo real, comprobando sus acciones contra un conjunto de reglas escritas antes de la misión. Si el robot intenta hacer algo prohibido, el copiloto hace sonar una alarma. Sin embargo, este enfoque tradicional tiene un fallo crítico: es reactivo. Solo lanza la alarma después de que el mal evento ya ha ocurrido. En entornos de alto riesgo, como una instalación nuclear o una misión en el espacio profundo, esperar a que ocurra un error antes de reaccionar puede ser demasiado tarde. El objetivo de los investigadores es construir un sistema que no solo vigile los errores, sino que los anticipe, prediciendo un fallo incluso antes de que el robot dé el primer paso hacia él.

Este es el desafío que aborda un equipo de investigadores que han desarrollado un nuevo sistema de monitorización llamado Predictive Varanus. El sistema está diseñado para robots autónomos, específicamente probado en un rover simulado encargado de inspeccionar un depósito de desechos nucleares. Los investigadores combinaron dos tecnologías existentes para crear un proceso que es estricto en cuanto a lo que el robot tiene permitido hacer y lo suficientemente inteligente como para prever qué sucederá después. La primera parte del sistema actúa como un guardián. Utiliza un mapa detallado del comportamiento previsto del robot, escrito en un lenguaje formal llamado Procesos Secuenciales Comunicantes (Communicating Sequential Processes), para comprobar cada uno de los eventos que el robot realiza. Si el robot intenta moverse a un lugar que no debía visitar, o ignora una orden de seguridad, el guardián rechaza inmediatamente esa acción como inválida. Esto asegura que el robot se mantenga dentro de los límites de su diseño.

La segunda parte del sistema es donde ocurre la predicción. Una vez que el guardián confirma que las acciones actuales del robot son válidas, el sistema mira hacia adelante. Se plantea una pregunta simple pero poderosa: dado que el robot se está comportando correctamente ahora, ¿cuáles son los únicos futuros posibles que puede tomar? Al analizar las rutas restantes permitidas por el mapa de diseño del robot, el sistema puede determinar si un resultado específico es ahora inevitable. No adivina posibilidades al azar; solo considera los futuros que son consistentes con las propias reglas del robot. Si el robot ha encontrado un nivel de radiación alto, el sistema sabe que el único camino futuro permitido es dar la vuelta y abortar la misión. Por lo tanto, incluso antes de que el robot realmente dé la vuelta, el sistema puede predecir con certeza que la misión fallará. Del mismo modo, si el robot ha visitado con éxito todos sus puntos de control requeridos, el sistema puede predecir que la misión tendrá éxito, incluso si el robot todavía tiene algunos movimientos más por hacer antes de detenerse oficialmente.

Los investigadores probaron este enfoque en su rover de inspección nuclear, el cual fue programado para visitar cinco puntos de control diferentes y comprobar los niveles de radiación. Los niveles fueron categorizados como verdes, naranjas o rojos. Si el rover veía naranja o rojo, las reglas dictaban que debía regresar al inicio y abortar. En la monitorización estándar, el sistema solo sabría que la misión está condenada después de que el rover realmente dé la vuelta. Con Predictive Varanus, el sistema pudo declarar la misión como un fallo dos eventos antes de que el rover siquiera comenzara su viaje de regreso. En otros escenarios, pudo predecir una finalización exitosa ocho eventos antes de que el rover terminara su última tarea. Esta alerta temprana otorga a los operadores humanos o al propio software de control del robot un tiempo valioso para reaccionar, quizás replanteando una ruta o preparando un apagado seguro, en lugar de simplemente observar cómo se desarrolla un fallo.

El estudio también midió cuánta potencia de cómputo requería esta capa adicional de pensamiento. La parte del guardián del sistema se mantuvo muy rápida, tomando menos de un milisegundo por evento incluso a medida que el mapa de comportamiento del robot crecía. La parte predictiva, que realiza el trabajo pesado de mirar hacia adelante, tomó más tiempo, especialmente a medida que los comportos posibles del robot se volvían más complejos. Para un modelo con 200 estados diferentes, la comprobación predictiva tomó unos 700 milisegundos por evento. Aunque esto es más lento, los investigadores encontraron que el beneficio de conocer el resultado anticipadamente valía el coste en muchas situaciones. El sistema identificó con éxito fallos inevitables y éxitos inevitables en escenarios donde el robot aún seguía las reglas, demostrando que es posible mirar hacia el futuro sin romper las leyes del presente.

Lo que hace que este trabajo sea significativo no es solo que predice el futuro, sino cómo lo hace. No depende de un modelo separado y abstracto para la predicción. En su lugar, reutiliza el mismo mapa de diseño que se utilizó para verificar el comportamiento del robot en primer lugar. Esto significa que el sistema no está haciendo suposiciones sobre cómo podría comportarse el robot; está siguiendo estrictamente la lógica que los ingenieros ya integraron en la máquina. Los investigadores demostraron que, al combinar una comprobación estricta de la validez actual con una comprobación prospectiva de la inevitabilidad futura, podían proporcionar veredictos más tempranos y útiles que la monitorización estándar. El sistema no predice fallos aleatorios o fallos de sensores que nunca fueron modelados; predice las consecuencias lógicas del propio diseño del robot. En el complejo e incierto mundo de la robótica autónoma, esta capacidad de ver el resultado inevitable de un camino correcto ofrece un nuevo tipo de seguridad, convirtiendo una alarma reactiva en una guía proactiva.

Resumen Técnico: Predictive Varanus

Planteamiento del Problema
La Verificación en Tiempo de Ejecución (RV, por sus siglas en inglés) es una técnica crítica para sistemas autónomos y robóticos, que ofrece seguridad en línea mediante la comprobación de trazas de ejecución observadas frente a especificaciones formales sin requerir acceso al código fuente o a los estados internos. Sin embargo, la RV estándar es inherentemente reactiva; solo puede detectar violaciones después de que un evento adverso ya ha ocurrido. En dominios de seguridad crítica donde los fallos son costosos, esta latencia es insuficiente. Mientras que la Verificación Predictiva en Tiempo de Ejecución (PRV) aborda esto analizando posibles continuaciones futuras para determinar la satisfacción o violación inevitable de las propiedades, los enfoques existentes suelen depender de modelos que son distintos de las especificaciones de diseño del sistema. Además, la PRV estándar no distingue intrínsecamente entre un sistema que se comporta de acuerdo con su modelo pero viola una propiedad temporal, frente a un sistema que se comporta de una manera que no está modelada (fuera de especificación).

Metodología
El artículo presenta PREDICTIVE VARANUS, un pipeline de verificación de dos etapas que integra la herramienta existente VARANUS con la Verificación Predictiva en Tiempo de Ejecución para la Lógica Temporal de Tiempo Lineal (LTL). La innovación central es la reutilización de un único modelo de Procesos Secuenciales Comunicantes (CSP) de tiempo de diseño tanto para la comprobación de conformidad como para el razonamiento predictivo.

El pipeline opera de la siguiente manera:

Puerta de Conformidad CSP (VARANUS): El sistema bajo análisis (SUA) emite una traza de eventos. La primera etapa utiliza un modelo CSP como un oráculo determinista. VARANUS comprueba si la traza actual es un prefijo válido del lenguaje del modelo CSP. Si un evento no está permitido por el modelo, la traza es rechazada inmediatamente (rej). Esto asegura que el razonamiento predictivo solo se aplique al comportamiento que es consistente con el diseño del sistema.
Traducción del Modelo: Para las trazas que pasan la puerta de conformidad, el modelo CSP se traduce en un autómata de Büchi (en formato Hanoi Omega-Automata). Esta traducción implica:
- Extraer el Sistema de Transición Etiquetado (LTS) del proceso CSP.
- Mapear los eventos CSP a proposiciones atómicas.
- Añadir bucles de auto-salto skip a los estados terminales para convertir trazas finitas en palabras infinitas, permitiendo la semántica estándar de LTL.
Monitorización LTL Predictiva: El monitor predictivo utiliza el autómata de Büchi traducido para restringir el conjunto de futuros admisibles. Dado una propiedad LTL $\phi$ $ϕ$ , el monitor computa los productos sincrónicos del autómata derivado de CSP con los autómatas para $\phi$ $ϕ$ y $\neg\phi$ $\neg ϕ$ .
- Si todas las continuaciones consistentes con el modelo satisfacen $\phi$ , el veredicto es de satisfacción concluyente ( $\top$ ).
- Si todas las continuaciones consistentes con el modelo violan $\phi$ , el veredicto es de violación concluyente ( $\bot$ ).
- Si ambos resultados siguen siendo posibles, el veredicto es inconcluyente ( $?$ ).
- Si la traza fue rechazada por VARANUS, el veredicto es rej.

Contribuciones Clave

Pipeline Integrado: El artículo define un pipeline formal de dos etapas que combina la monitorización de conformidad basada en CSP con la verificación predictiva de LTL.
Reutilización de Modelos: Demuestra cómo un único modelo CSP, típicamente utilizado para el análisis en tiempo de diseño (por ejemplo, con FDR o RoboChart), puede servir para dos propósitos: como un oráculo de ejecución para la conformidad y como la fuente de futuros admisibles para la predicción.
Semántica Formal: Los autores proporcionan definiciones formales para la función de veredicto combinada, distinguiendo entre rej (no conformidad del modelo) y $\bot$ predictivo (violación inevitable dentro del modelo).
Implementación y Traducción: El trabajo detalla la construcción del $\omega$ -autómata proposicional a partir de procesos CSP, permitiendo el uso de herramientas de LTL estándar (como Spot) preservando al mismo tiempo las restricciones estructurales del modelo CSP.

Resultados
El enfoque fue evaluado utilizando un caso de estudio de un rover robótico para la inspección de almacenes nucleares y pruebas de estrés sintéticas.

Caso de Estudio del Rover: El sistema monitorizó propiedades relativas a la finalización de la misión, cobertura y condiciones de aborto.
- En escenarios donde se detectó radiación peligrosa, el sistema predijo el fallo de la misión (violación de completitud/cobertura) y la inevitabilidad de un aborto de 1 a 2 eventos antes de que ocurriera el evento de aborto real en la traza.
- Para misiones nominales, la propiedad de cobertura fue predicha como satisfecha 8 eventos antes del evento de finalización de la misión.
- Las trazas inválidas (por ejemplo, continuar tras un peligro) fueron rechazadas inmediatamente por VARANUS, sin ganancia predictiva, confirmando que el sistema maneja correctamente el comportamiento fuera del modelo.
- La sobrecarga de tiempo de ejecución fue modesta para el rover (aprox. 1.84 ms/evento en total), con la comprobación CSP tomando 0.19 ms y el monitor predictivo 1.64 ms.
Pruebas de Estrés Sintéticas:
- Escalabilidad: La comprobación de conformidad CSP se mantuvo ligera (<1 ms/evento) incluso a medida que aumentaba el tamaño del modelo. Sin embargo, el coste del monitor predictivo escaló significamente con el tamaño del modelo (de ~0.2 ms/evento con 10 estados a ~700 ms/evento con 200 estados), identificando la construcción y el mantenimiento de autómatas como el principal cuello de botella.
- Ganancia de Anticipación: En los benchmarks de decisión-cola (decision-tail), la ganancia de anticipación (el número de eventos ahorrados por la predicción) creció linealmente con la longitud de la cola forzada tras un punto de compromiso. Para una longitud de cola de 20, el sistema proporcionó un veredicto 21 eventos antes que un monitor reactivo.

Significancia y Reivindicaciones
El artículo afirma que PREDICTIVE VARANUS ofrece un método práctico para lograr veredictos más tempranos en la verificación en tiempo de ejecución aprovechando los modelos CSP de diseño existentes. Su significancia radica en:

Diferenciación de Modos de Fallo: Separa claramente el comportamiento "fuera del modelo" (detectado por VARANUS) de la "violación inevitable de la propiedad" dentro del modelo (detectada por PRV).
Utilidad Operativa: El caso de estudio demuestra que los veredictos predictivos pueden generarse lo suficientemente pronto como para ser útiles para operadores humanos o algoritmos de replanificación, específicamente al identificar abortos de misión o fallos inevitables antes de que se manifiesten físicamente.
Modularidad: El pipeline es modular; aunque la implementación actual utiliza LTL, la estructura permite integrar otras técnicas de razonamiento predictivo sin alterar la capa de conformidad CSP.

Los autores reconocen que la implementación actual enfrenta desafíos de escalabilidad respecto al componente predictivo para modelos grandes, sugiriendo que el trabajo futuro podría centrarse en optimizar el backend de autómatas o explorar representaciones simbólicas. No pretenden resolver el problema general de predecir fallos físicos no modelados, sino anticipar resultados que están forzados por el propio modelo de diseño del sistema.

Más como este