Quantitative Monitoring of Signal First-Order Logic

1. Problema

La verificación en tiempo de ejecución (runtime verification) es crucial para sistemas híbridos y ciberfísicos, donde se debe verificar si el comportamiento del sistema cumple con una especificación formal mientras se ejecuta.

• Limitaciones de la Lógica Temporal de Señales (STL): Aunque la STL es ampliamente utilizada, su expresividad es limitada para modelar comportamientos complejos que requieren cuantificación sobre valores y tiempos simultáneamente.
• Limitaciones de la Lógica de Primer Orden de Señales (SFO): La SFO, introducida previamente, ofrece una expresividad superior a la STL (permitiendo, por ejemplo, propiedades de estabilización acotada y restricciones de derivadas puntuales). Sin embargo, hasta este trabajo, la SFO solo tenía semántica booleana (satisface o viola) y carecía de herramientas de monitoreo en línea. Además, las fórmulas con comportamiento futuro ilimitado no son eficientemente monitorizables en tiempo real.
• Necesidad de Semántica Cuantitativa: En aplicaciones reales con dinámicas continuas, un resultado binario es insuficiente. Se requiere una semántica cuantitativa (basada en robustez) que mida cuánto se cumple o viola una especificación, proporcionando retroalimentación más rica para la toma de decisiones.

2. Metodología

Los autores proponen un enfoque integral que combina fundamentos semánticos, transformaciones sintácticas y algoritmos geométricos:

A. Semántica Cuantitativa Robusta

Se define una semántica de robustez para SFO que asigna un valor numérico ($\mu \in \mathbb{R} \cup \{-\infty, +\infty\}$) a cada fórmula respecto a una señal y una valoración.

• Definición Inductiva:
  • Las comparaciones atómicas ($\theta_1 < \theta_2$) se evalúan como la diferencia $\theta_2 - \theta_1$.
  • La negación invierte el signo ($-\mu$).
  • La disunción ($\lor$) toma el máximo ($\max$).
  • Los cuantificadores existenciales ($\exists$) se evalúan mediante el supremo ($\sup$) sobre el dominio de la variable.
• Corrección: Se demuestra que si $\mu > 0$, la fórmula se satisface booleanamente; si $\mu < 0$, se viola.

B. Fragmento de Tiempo Pasado y "Pastificación"

Para habilitar el monitoreo en línea (que no puede esperar al futuro), se identifica un fragmento de SFO llamado pSFO (Signal First-Order Logic de Tiempo Pasado), donde el acceso a las señales solo depende de tiempos anteriores o actuales ($t + \delta$ con $\delta \le 0$).

• Procedimiento de Pastificación: Se introduce un algoritmo para transformar fórmulas SFO de "respuesta acotada" (bounded-response) en fórmulas pSFO equisatisfacibles.
• Horizonte Futuro: Se calcula un horizonte futuro máximo ($H^+$) que indica cuánto hacia adelante necesita mirar la fórmula. Al sustituir la variable de tiempo libre $t$ por $t - H^+$, se desplaza la ventana de evaluación hacia el pasado, eliminando la necesidad de mirar el futuro.

C. Algoritmo de Monitoreo en Línea

Se desarrolla un algoritmo eficiente para evaluar fórmulas pSFO sobre señales lineales a trozos (piecewise-linear).

• Representación Poliedral: Las señales, términos y fórmulas se representan geométricamente como colecciones de poliedros convexos definidos por restricciones lineales.
• Operaciones Simbólicas:
  • Los operadores lógicos se traducen en operaciones poliedrales (intersección, unión, proyección).
  • La cuantificación existencial se resuelve mediante eliminación de variables calculando el supremo de la función de robustez sobre el intervalo de la variable cuantificada.
  • Se utiliza un enfoque de "ventana deslizante" basada en el horizonte de tiempo pasado ($H^-$), descartando datos antiguos que ya no son necesarios, lo que garantiza un uso de memoria acotado.
• Implementación: El algoritmo se implementa utilizando representaciones de doble descripción para poliedros y optimización lineal paramétrica.

3. Contribuciones Clave

1. Semántica Cuantitativa para SFO: Primera definición robusta de semántica cuantitativa para la lógica SFO completa, generalizando la semántica booleana estándar.
2. Fragmento pSFO y Pastificación: Definición de un fragmento sintáctico adecuado para monitoreo en línea y un procedimiento automático para transformar fórmulas de respuesta acotada a este fragmento.
3. Algoritmo de Monitoreo Eficiente: Un algoritmo novedoso que calcula valores de robustez simbólicamente utilizando representaciones poliedrales, capaz de manejar cuantificadores anidados y combinaciones booleanas complejas.
4. Prototipo y Evaluación: Implementación de una herramienta prototipo (en Python con SymPy y Parma Polyhedra Library) y evaluación exhaustiva en benchmarks de sistemas ciberfísicos.

4. Resultados

Los experimentos se realizaron en dos escenarios de referencia:

1. Evitación de Obstáculos Dinámicos (Drones):
   • Se probaron propiedades de velocidad segura, suavidad de movimiento (derivadas) y separación de obstáculos.
   • Rendimiento: El tiempo de cálculo por segmento fue significativamente menor que el intervalo de control (0.1s), incluso con horizontes de memoria cortos. Esto demuestra que el monitoreo puede usarse para tomar decisiones de control en tiempo real.
2. Control de Altitud (F-16 Fighter Jet):
   • Se evaluaron propiedades de altitud segura, velocidad segura y recuperación de altitud (con cuantificadores temporales anidados).
   • Rendimiento: Para la propiedad de recuperación (con un horizonte de 20 segundos y ~600 segmentos de memoria), el tiempo de análisis fue de ~0.2s por segmento. Aunque no es lo suficientemente rápido para control directo en este caso específico, es adecuado para generar advertencias y supervisión.

Tabla de Resultados (Resumen):

• Las propiedades sin horizonte (horizonte 0) o con horizonte muy corto se procesan en milisegundos (0.002s - 0.014s).
• Las propiedades con cuantificadores y horizontes largos aumentan el tiempo de cómputo (hasta 0.532s para combinaciones complejas), pero siguen siendo factibles para monitoreo en línea.

5. Significado e Impacto

• Avance Teórico: Este trabajo cierra la brecha entre la alta expresividad de la lógica de primer orden y la necesidad práctica de monitoreo en tiempo real con métricas cuantitativas. Es el primer prototipo público disponible para el monitoreo cuantitativo en línea de SFO completa.
• Aplicabilidad Práctica: Demuestra que es posible monitorear propiedades complejas (como estabilización acotada y relaciones entre duraciones de eventos en diferentes señales) en sistemas híbridos reales sin sacrificar la eficiencia.
• Futuro: Abre la puerta a nuevas aplicaciones, como el uso de la robustez como función de recompensa en el aprendizaje por refuerzo para síntesis de controladores, y la integración con mecanismos de "escudo" (shielding) para corrección en tiempo de ejecución de sistemas de IA.

En resumen, el paper presenta un marco sólido y una implementación funcional que transforma la SFO de una herramienta teórica de especificación a una tecnología viable para la supervisión y garantía de seguridad en sistemas ciberfísicos complejos.