Resumen Técnico: Uppaal Coshy – Síntesis Automática de Escudos Compactos para Sistemas Híbridos

1. Planteamiento del Problema

El artículo aborda el desafío de la síntesis de estrategias de seguridad (escudos o shields) para Procesos de Decisión de Markov (MDP) sobre espacios de estados continuos con dinámicas híbridas complejas. A diferencia de los espacios de estados discretos donde la síntesis de escudos está bien establecida, los sistemas híbridos presentan dificultades algorítmicas, particularmente en lo que respecta al análisis de alcanzabilidad para dinámicas no lineales y la gestión de espacios de estados infinitos.

Un cuello de botella práctico primordial identificado es la escalabilidad y el almacenamiento de los escudos sintetizados. Los enfoques tradicionales basados en particiones almacenan las acciones permitidas para cada celda individual en una rejilla, lo que resulta en estructuras de datos masivas que son ineficientes para el almacenamiento y el despliegue, especialmente en dispositivos embebidos. Además, determinar las celdas seguras y las transiciones en sistemas híbridos generales suele implicar problemas de alcanzabilidad indecidibles.

2. Metodología

Los autores presentan Uppaal Coshy, una herramienta totalmente integrada en el entorno de modelado Uppaal. La metodología combina un algoritmo de síntesis basado en particiones con aproximaciones basadas en simulación y una novedosa técnica de compresión.

2.1 Síntesis de Escudos Basada en Particiones

El algoritmo central abstrae el espacio de estados continuo $S \subseteq \mathbb{R}^k$ en un conjunto finito de celdas rectangulares disjuntas utilizando una rejilla regular definida por un vector de granularidad $\gamma$ y un desplazamiento $\omega$.

• Formulación del Juego de Seguridad: La síntesis se enmarca como un juego de seguridad de dos jugadores. El objetivo es computar el conjunto máximo de "celdas seguras" ($C_\phi$) desde las cuales el sistema puede permanecer dentro de una propiedad de seguridad $\phi$ indefinidamente.
• Aproximación mediante Simulación: Dado que la alcanzabilidad exacta es a menudo indecidible para sistemas híbridos generales, la herramienta emplea un enfoque basado en simulación:
  • Celdas Inicialmente Seguras ($C^0_\phi$): En lugar de un razonamiento simbólico, la herramienta muestrea sistemáticamente puntos dentro de cada celda. Una celda se considera inicialmente segura solo si todos los puntos muestreados satisfacen la especificación de seguridad.
  • Relación de Transición: Para determinar si existe una transición entre celdas ($C \xrightarrow{a} C'$), la herramienta simula las dinámicas del sistema desde estados muestreados en $C$ utilizando la acción $a$. Si la simulación alcanza un estado donde el controlador debe realizar una nueva elección, la celda objetivo correspondiente se añade a la relación de transición.
  • Estocasticidad: A diferencia de trabajos previos que requerían la creación manual de muestreo para dimensiones estocásticas, Uppaal Coshy permite que el simulador muestree directamente de distribuciones estocásticas, soportando distribuciones generales con soporte no acotado.

2.2 Manejo de Desafíos Prácticos

• Espacios de Estados No Acotados: La herramienta maneja sistemas donde los límites de estado no están claros de inmediato (por ejemplo, una pelota que rebota) introduciendo una celda ficticia de "fuera de límites" ($C_{out}$). Los usuarios pueden configurar si salir de los límites es seguro, inseguro o determinado mediante muestreo.
• Omisión de Variables: Para reducir la dimensionalidad, los usuarios pueden omitir variables (por ejemplo, contadores de costo o relojes) de la partición de la rejilla. Estas variables se fijan a sus valores iniciales durante la síntesis, siempre que no influyan en la lógica de seguridad.

2.3 Representación Compacta: El Algoritmo Caap

Para abordar la ineficiencia de almacenamiento de los escudos basados en rejillas, los autores introducen Caap (Coarsify Axis-Aligned Partitionings).

• Objetivo: Transformar un escudo de rejilla de grano fino y alineado con los ejes en un árbol de decisión compacto y equivalente.
• Mecanismo: El algoritmo fusiona iterativamente celdas vecinas que comparten el mismo conjunto de acciones permitidas en "regiones" rectangulares más grandes.
• Restricciones: Las fusiones están sujetas a tres reglas de expansión para asegurar que la partición resultante siga siendo válida:
  1. Todas las celdas en la nueva región deben tener el mismo conjunto de acciones.
  2. La nueva región no debe intersectar con regiones existentes en la nueva partición.
  3. La expansión no debe cortar ninguna región original en fragmentos no rectangulares.
• Resultado: Esto genera un árbol de decisión donde los nodos internos representan predicados alineados con los ejes ($s_i < c$) y las hojas representan conjuntos de acciones permitidas, reduciendo significativamente el tamaño de la representación.

3. Contribuciones Clave

1. Herramienta Uppaal Coshy: Una herramienta totalmente automática para la síntesis de escudos en Uppaal, que soporta formalismos expresivos incluyendo autómatas híbridos estocásticos y llamadas a librerías externas de C. Se integra con Uppaal Stratego para permitir el aprendizaje por refuerzo bajo un escudo sintetizado.
2. Algoritmo Caap: Un algoritmo novedoso para comprimir escudos basados en rejillas en árboles de decisión, preservando la funcionalidad mientras reduce drásticamente el tamaño.
3. Aproximación Basada en Simulación: Una estrategia de implementación práctica que evita los problemas de alcanzabilidad indecidibles mediante el uso de muestreo sistemático y simulación, soportando control no periódico y distribuciones estocásticas generales.

4. Resultados y Evaluación

Los autores evaluaron la herramienta en cuatro modelos: una pelota que rebota (bouncing ball), un convertidor boost, un camino aleatorio (random walk) y un tanque de agua.

• Síntesis y Reducción: La Tabla 2 en el artículo demuestra reducciones significativas en el tamaño del escudo. Para el modelo de la pelota que rebota, el escudo se redujo de 1,430,000 celdas a 2,972 regiones (un factor de reducción de ~480x) en 53 segundos. El convertidor boost pasó de 136,800 a 571 regiones.
• Verificación de Seguridad: Todos los escudos sintetizados fueron evaluados estadísticamente con intervalos de confianza del 99% sobre 10,000 ejecuciones. No se observaron ejecuciones inseguras, confirmando que los escudos mantuvieron las propiedades de seguridad (por ejemplo, evitando que la pelota se detenga o que el voltaje exceda los límites).
• Demostración del Flujo de Trabajo: El caso de estudio de la pelota que rebota (Sección 5.1) ilustra un flujo de trabajo completo: la síntesis de una estrategia básica "eficiente" (que falla en seguridad), la generación de un escudo, su compresión mediante Caap y, finalmente, el uso de Uppaal Stratego para aprender una estrategia casi óptima bajo el escudo compacto. La estrategia resultante fue tanto segura como eficiente.

5. Significado y Reivindicaciones

El artículo posiciona a Uppaal Coshy como un puente entre la síntesis teórica de escudos y la aplicación práctica en sistemas híbridos complejos.

• Expresividad: La herramienta afirma manejar una clase de modelos más rica que las herramientas existentes (como Tempest o Uppaal Tiga), soportando específicamente sistemas híbridos estocásticos con control no periódico e integración de código externo.
• Desplegabilidad: Al introducir el algoritmo Caap, los autores afirman resolver el problema crítico del tamaño del escudo, haciendo factible el despliegue de estrategias sintetizadas en dispositivos embebidos con recursos limitados.
• Integración: La integración fluida con Uppaal Stratego permite un flujo de trabajo donde la seguridad es garantizada por el escudo, mientras que el rendimiento se optimiza mediante el aprendizaje por refuerzo, una capacidad que los autores destacan como un beneficio distintivo sobre el trabajo previo.

Los autores mantienen la modestia respecto a la naturaleza de aproximación de su enfoque, señalando que la sub-aproximación basada en simulación depende del número de muestras ($n$) y de las ejecuciones de re-muestreo ($m$) para acercarse a la solución real, y que el algoritmo Caap es actualmente una herramienta independiente que proponen integrar directamente en la interfaz de usuario de Uppaal en trabajos futuros.