Bernstein-based polynomial approach to study the stability of switched systems and formal verification using HOL Light

Resumen Técnico: Enfoque de Polinomios Basado en Bernstein para la Estabilidad de Sistemas Conmutados y Verificación Formal

Planteamiento del Problema
Los sistemas conmutados, compuestos por múltiples subsistemas gobernados por una señal de conmutación, presentan desafíos significativos en el análisis de estabilidad. Los métodos tradicionales suelen tener dificultades para proporcionar una descripción matemática unificada del comportamiento completo del sistema, particularmente cuando la señal de conmutación es compleja (por ejemplo, dependiente del estado o del tiempo). Si bien existen numerosos métodos para analizar estos sistemas, existe la necesidad de una formulación que pueda transformar la lógica de conmutación discreta en una expresión polinómica continua, facilitando así la construcción de funciones de Lyapunov y permitiendo la verificación formal rigurosa.

Metodología
El artículo propone una estrategia para reformular sistemas conmutados utilizando interpolación de Bernstein. El enfoque central implica los siguientes pasos:

1. Reformulación Polinómica: La señal de conmutación $\sigma$, que dicta la activación de los subsistemas $f_i$, se aproxima mediante polinomios de Bernstein. Al expresar la señal de conmutación como una combinación lineal de funciones de base de Bernstein, todo el sistema conmutado (originalmente definido por ecuaciones diferenciales por partes) se transforma en una única expresión polinómica unificada.

   • El sistema se describe inicialmente como una combinación convexa de subsistemas: $\dot{x} = \sum f_i(x)\sigma_i$, donde $\sum \sigma_i = 1$ y $\sigma_i \geq 0$.
   • La señal de conmutación $\sigma_i$ se reemplaza por su aproximación de serie de Bernstein $B_{i,m}^\sigma(\sigma(\nu), \nu)$, lo que resulta en un "sistema B-conmutado" descrito por una única ecuación diferencial polinómica.

2. Manejo de Tipos de Conmutación: El método acomoda diferentes comportamientos de conmutación:

   • Conmutación dependiente del estado: Se modela mediante funciones de signo (por ejemplo, $\sigma \equiv \text{sign}(\delta x_1 x_2)$), aproximadas por polinomios de Bernstein de un grado $m$ específico.
   • Conmutación dependiente del tiempo: Se modela mediante funciones de pulso para representar la activación periódica.
   • Flexibilidad: El grado $m$ del polinomio de Bernstein puede ajustarse para refinar la aproximación, o se pueden aplicar reglas de composición para obtener mayor precisión, aunque esto aumenta la complejidad de las expresiones resultantes.

3. Verificación Formal: Una vez que el sistema está representado como un polinomio, los autores proponen utilizar el asistente de pruebas HOL Light para verificar formalmente las propiedades de estabilidad.

   • Se identifica una función de Lyapunov candidata $V(x)$ para el sistema polinómico.
   • La tarea de verificación se reduce a probar la desigualdad $\dot{V}(x) < \epsilon$ (donde $\epsilon$ es una constante positiva pequeña) sobre un dominio definido $D$.
   • Esto se logra utilizando aritmética de intervalos con aproximaciones de Taylor, un método previamente validado en el proyecto Flyspeck. Esto permite la certificación rigurosa de que la derivada de la función de Lyapunov es negativa (o suficientemente cercana a cero) dentro de los límites especificados.

Resultados Clave
El artículo ilustra el enfoque propuesto a través de dos ejemplos numéricos derivados de la literatura existente, comparando la representación polinómica "B-conmutada" contra el sistema conmutado "estándar":

• Ejemplo 1 (Sistema Estable): Se analizó un sistema conmutado lineal con dos subsistemas estables. La aproximación de Bernstein logró imitar con éxito el comportamiento estabilizador del sistema estándar.
• Ejemplo 2 (Sistema Inestable): Se analizó un sistema conmutado lineal con subsistemas inestables. El método capturó correctamente el comportamiento divergente, observando que a medida que el producto del estado $x_1 x_2$ crece más allá del intervalo $[0, 1]$, la serie de Bernstein diverge naturalmente, reflejando la inestabilidad del sistema.
• Verificación Formal: Se utilizó un sistema estable lineal básico para demostrar el proceso de verificación de HOL Light. Los autores lograron generar un certificado de prueba formal que confirma que la derivada de una función de Lyapunov cuadrática se mantuvo por debajo de un umbral ($\epsilon = 0.01$) dentro del intervalo $[0, 1]$.

Significado y Reivindicaciones
Los autores presentan este trabajo como un estudio preliminar con las siguientes contribuciones y limitaciones específicas:

• Unificación: La contribución principal es la capacidad de "unificar" múltiples subsistemas conmutados en una única expresión polinómica mediante la interpolación de Bernstein. Esto simplifica la búsqueda de funciones candidatas de Lyapunov.
• Certificación Formal: El enfoque cierra la brecha entre la simulación numérica y la prueba formal, permitiendo que el asistente HOL Light verifique las propiedades de estabilidad de las funciones de Lyapunov derivadas.
• Alcance Modesto: El artículo establece explícitamente que asume que las propiedades de estabilidad del sistema B-conmutado son equivalentes a las del sistema conmutado estándar (al menos respecto a la estabilidad de Lyapunov), pero no pretende haber probado esta equivalencia de manera rigurosa aún.
• Trabajo Futuro: Los autores identifican varias áreas para investigación futura, que incluyen:
  • Demostrar la equivalencia matemática completa entre las representaciones estándar y B-conmutadas respecto a la estabilidad.
  • Extender el método a sistemas no lineales y no polinómicos.
  • Utilizar herramientas de Suma de Cuadrados (SOS) para calcular funciones de Lyapunov "óptimas" en lugar de solo verificar candidatas identificadas.

En conclusión, el artículo propone un marco novedoso que aprovecha los polinomios de Bernstein para convertir el análisis de sistemas conmutados en un problema polinómico, resoluble mediante herramientas de verificación formal, ofreciendo una vía potencial para la certificación de estabilidad rigurosa.