TERA: A Unified Taylor Model Enabled Reachability Analysis Framework

Resumen Técnico: TERA – Un Marco de Análisis de Alcanzabilidad Habilitado por Modelos de Taylor Unificados

Planteamiento del Problema
La verificación de sistemas críticos para la seguridad, definidos por dinámicas como $\dot{x} = f(x, u, w)$ donde $w$ representa perturbaciones o incertidumbres acotadas, requiere envolventes rigurosas de todas las posibles trayectorias de estado sobre un horizonte de tiempo finito. Si bien el cómputo exacto de los tubos de flujo (flowpipes) es generalmente infactible para sistemas no lineales, las sobre-aproximaciones basadas en conjuntos son necesarias para la verificación de seguridad. Sin embargo, las representaciones tradicionales como (hiper-)intervalos y zonotopos sufren del "efecto de envoltorio" (wrapping effect), donde las sobre-aproximaciones acumuladas conducen a envolventes de conjuntos alcanzables excesivamente conservadoras. Además, las herramientas existentes basadas en Modelos de Taylor (TM) (por ejemplo, Flow*, CORA, JuliaReach) suelen estar escritas en lenguajes compilados (C++, MATLAB, Julia), lo que dificulta el prototipado rápido, o carecen de soporte para sistemas estocásticos y una amplia clase de sistemas dentro de un flujo de trabajo unificado.

Metodología
TERA aborda estas limitaciones proporcionando un marco nativo de Python que se integra con el ecosistema científico de Python y aprovecha el sistema de álgebra computacional SageMath. La metodología central se basa en Modelos de Taylor (TM) de la forma $P(x_0, t) + I$, donde $P$ es una aproximación polinómica de Taylor de alto orden de la solución e $I$ es un resto de intervalo que garantiza que la solución verdadera está contenida.

Los componentes metodológicos clave incluyen:

• Propagación: Las dinámicas de tiempo continuo se propagan utilizando esquemas de integración de TM validados, fundamentados en el trabajo de Berz y Makino, junto con enfoques de construcción de tubos de flujo para sistemas no lineales por Chen.
• Mitigación del Efecto de Envoltorio: Para mantener envolventes ajustadas sobre horizontes de tiempo largos, TERA implementa la propagación composicional izquierda-derecha utilizando el método de "encogimiento de envoltorio" (shrink-wrapping).
• Soporte de Sistemas:
  • EDOs No Lineales: Soporta sistemas con no linealidades no polinómicas (por ejemplo, funciones trascendentales como $\sin$ y $\cos$).
  • Sistemas Híbridos: Computa las intersecciones de guardas de autómatas híbridos y transiciones discretas siguiendo la semántica de alcanzabilidad híbrida basada en TM.
  • Sistemas Estocásticos: Para sistemas estocásticos de tiempo continuo, TERA combina tubos de flujo de TM deterministas con límites de desviación probabilística para computar envolventes de conjuntos alcanzables $\delta$-probabilísticos ($\delta$-PRS). Esto garantiza que las trayectorias permanezcan dentro de los conjuntos computados con una probabilidad de al menos $1-\delta$.
• Aritmética Rigurosa: El redondeo correcto se logra mediante la biblioteca GNU MPFR integrada dentro de SageMath para asegurar el rigor matemático.

Contribuciones Clave

1. Marco Unificado: TERA se presenta como el primer marco gratuito, de código abierto y nativo de Python capaz de manejar sistemas continuos, híbridos y estocásticos dentro de un único flujo de trabajo simbólico-numérico.
2. Extensibilidad: Al aprovechar Python y SageMath, el marco facilita el prototipado rápido de técnicas de análisis de alcanzabilidad, abordando la rigidez de las herramientas actuales de C++ o MATLAB propietarias.
3. Capacidad Estocástica: El marco extiende la alcanzabilidad basada en TM a sistemas estocásticos de tiempo continuo, computando envolventes $\delta$-PRS.
4. Disponibilidad Abierta: El software se distribuye bajo la licencia GPLv2 y está disponible vía GitHub.

Resultados y Validación
Los autores validaron TERA contra la suite de problemas de referencia de la competencia ARCH [5]. Los resultados demuestran la capacidad del marco para computar sobre-aproximaciones de conjuntos alcanzables ajustadas para problemas de referencia difíciles:

• Sistemas Continuos No Lineales: TERA computó con éxito una envolvente ajustada para una red de reacción bioquímica de la clase de Laub-Loomis de 7 dimensiones sobre $t \in [0, 20]$ en 13 segundos. También escaló a un problema de cuadricóptero controlado de 12 dimensiones que involucra funciones trascendentales.
• Sistemas Híbridos: El marco generó envolventes rigurosas para un sistema híbrido de bola rebotante, proyectando correctamente los tubos de flujo sobre el plano $(x, t)$ mientras distinguía entre modos activos (arriba/abajo).
• Sistemas Estocásticos: TERA computó una envolvente $\delta$-PRS ($\delta = 0.001$) para un modelo de resorte estocástico sobre $t \in [0, 20]$. Se demostró que la envolvente resultante contiene 2000 trayectorias de muestra de Monte Carlo de Euler-Maruyama.

Significancia y Perspectiva Futura
El artículo posiciona a TERA como un paso fundacional hacia una infraestructura robusta de código abierto en Python para el análisis de alcanzabilidad rigurosa. Su significancia radica en democratizar el acceso a métodos de alto orden basados en TM para una amplia clase de sistemas, incluyendo aquellos con perturbaciones estocásticas. Los autores afirman que el trabajo en curso se centra en extender las capacidades a sistemas híbridos estocásticos. El objetivo a largo plazo es aplicar esta infraestructura a clases de sistemas aún más amplias, como aquellas controladas por redes neuronales artificiales. Los autores mantienen un tono modesto, señalando que, si bien la implementación actual maneja benchmarks difíciles, el marco está diseñado para evolucionar y soportar clases de sistemas más complejas.