Stability Checking of Markov Jump Linear Systems via Probabilistic Temporal Logic (Extended Version)

Resumen Técnico: Verificación de la Estabilidad de Sistemas Lineales con Saltos de Markov mediante Lógica Temporal Probabilística

Planteamiento del Problema
Los Sistemas Lineales con Saltos de Markov (MJLS, por sus siglas en inglés) modelan fenómenos dinámicos sujetos a cambios aleatorios entre múltiples modos lineales, gobernados por una cadena de Markov de tiempo discreto subyacente. El análisis de estabilidad clásico para los MJLS se basa en nociones globales como la estabilidad de la media (MS) y la estabilidad de la media cuadrática (MSS), que caracterizan el comportamiento asintótico de el primer y segundo momento del estado del sistema. Estos enfoques clásicos suelen requerir garantías de estabilidad para todas las condiciones iniciales. Los autores argumentan que esta perspectiva global puede ser excesivamente conservadora o engañosa en la práctica. Específicamente, la inestabilidad podría surgir solo para un subconjunto negligible de estados iniciales (por ejemplo, configuraciones físicamente inalcanzables), mientras que el sistema permanece estable para todos los estados prácticamente relevantes. Por el contrario, un sistema podría converger para todas las condiciones iniciales pero hacia diferentes valores límite, fallando en la definición estricta de estabilidad (que requiere la convergencia a un valor común, típicamente el origen), a pesar de exhibir un comportamiento de convergencia deseable.

El artículo aborda la brecha en la literatura respecto a la verificación de propiedades de estabilidad relativas a conjuntos específicos de estados iniciales. Esto se enmarca en un problema de verificación de modelos (model-checking), donde el objetivo es determinar si se cumplen propiedades temporales específicas de convergencia de momentos para un subconjunto dado del espacio de estados.

Metodología
Los autores abordan el problema integrando el análisis de estabilidad en el marco de la Lógica de Árbol de Computación Probabilística (PCTL).

1. Formalización de PCTL en MJLS:
   El artículo primero formaliza la PCTL estándar para los MJLS. El espacio de estados se define como $S_J = \mathbb{R}^n \times \{1, \dots, m\}$, combinando variables de estado continuas con modos de Markov discretos. Las proposiciones atómicas se definen sobre politopos convexos para estados continuos y modos específicos para estados discretos. La relación de satisfacción se define sobre caminos infinitos, calculando las probabilidades sobre conjuntos cilíndricos derivados de la cadena de Markov subyacente.

2. Limitaciones del Model-Checking General de PCTL:
   Los autores analizan la decidibilidad de la lógica PCTL completa (incluyendo el operador "hasta" (until) no acotado) en los MJLS. Establecen que los MJLS pueden integrarse en Procesos de Markov Generales (GMP). Aprovechando el hecho de que los Sistemas Dinámicos Lineales (LDS) son un caso determinista especial de los MJLS, demuestran que el problema de alcanzabilidad para PCTL en los MJLS hereda los resultados de indecidibilidad asociados con el problema de Skolem. Específicamente, determinar la alcanzabilidad para conjuntos de dimensión cuatro o superior en los LDS es un problema abierto, lo que implica que el problema general de verificación de modelos para PCTL en los MJLS (más allá del fragmento acotado por pasos $PCTL^-$) también es abierto y probablemente indecidible.

3. Extensión con Operadores de Estabilidad:
   Para superar las limitaciones de las definiciones globales de estabilidad y la indecidibilidad de la alcanzabilidad general, los autores extienden la PCTL con nuevas proposiciones atómicas que capturan propiedades de estabilidad basadas en momentos relativas a estados iniciales específicos.

• Operadores: Introducen operadores acotados por pasos ($E^k_\Pi, V^k_\Xi$) y no acotados por pasos ($E_\Pi, V_\Xi$).
  • $E_\Pi$ y $V_\Xi$ comprueban si el límite de Cesàro (límite de promedio temporal) del primer momento (valor esperado) y del segundo momento (varianza no centrada), respectivamente, se encuentra dentro de un politopo convexo especificado ($\Pi$ o $\Xi$).
  • Estos operadores utilizan el límite de Cesàro en lugar de límites puntuales para manejar comportamientos oscilatorios que pueden no converger puntualmente, pero que poseen un promedio bien definido.
• Enfoque Algebraico: La verificación de estos nuevos operadores se basa en técnicas de álgebra lineal en lugar de un análisis de alcanzabilidad general.
  • La evolución de los momentos condicionales está gobernada por operadores lineales: $B_J$ para el primer momento y $T_J$ para el segundo momento.
  • El conjunto de satisfacción para los operadores no acotados se computa analizando las propiedades espectrales (autovalores y autovectores/bloques de Jordan) de estos operadores.
  • Para operadores diagonalizables, el límite se determina mediante la proyección del estado inicial sobre el subespacio propio correspondiente a los autovalores en el círculo unitario.
  • Para operadores no diagonalizables, los autores emplean la forma normal de Jordan para computar los límites de manera simbólica, manejando casos donde los términos divergen o se cancelan.

Contribuciones Clave y Resultados

• Marco Lógico: El artículo proporciona una semántica formal para la PCTL en los MJLS y la extiende con operadores que especifican la estabilidad relativa a conjuntos de estados iniciales.
• Verificación Algorítmica:
  • Se proporciona un procedimiento de decisión para el fragmento acotado por pasos ($PCTL^-$) y los nuevos operadores de estabilidad ($E_\Pi, V_\Xi$, etc.).
  • Los algoritmos para los operadores de estabilidad reducen el problema de verificación a la resolución de sistemas de ecuaciones lineales y la comprobación de membresía en politopos convexos. Esto asegura que los conjuntos de satisfacción resultantes sean representables (como conjuntos convexos o uniones de los mismos) y computacionalmente tratables, siempre que se puedan computar los autovalores.
  • Los autores demuestran que, mientras el problema de verificación de modelos general para PCTL es abierto debido a su conexión con el problema de Skolem, el fragmento específico que trata la estabilidad de momentos es decidible mediante álgebra lineal.
• Manejo de Oscilaciones: Al utilizar límites de Cesàro, los operadores propuestos capturan una noción de convergencia que permanece bien definida incluso cuando las secuencias de momentos oscilan, contrastando con las definiciones clásicas que podrían fallar en tales casos.
• Casos de Estudio: El artículo incluye ejemplos computacionales (por ejemplo, un MJLS de 3 modos con 2 variables de estado) que visualizan los conjuntos de satisfacción para fórmulas como $P_{\ge 0.3}(\Lambda \mathcal{U}_{\le 5} E_\Pi)$, demostrando la capacidad de identificar regiones del espacio de estados que satisfacen requisitos complejos de estabilidad y alcanzabilidad.

Significancia y Reclamaciones
Los autores afirman que su trabajo permite una visión "refinada" de la estabilidad de los MJLS que anteriormente era imposible de expresar o decidir. Al alejarse de las garantías globales, el marco permite a los analistas:

1. Identificar propiedades de estabilidad para subconjuntos específicos y prácticamente relevantes de condiciones iniciales, evitando el conservadurismo del análisis global.
2. Combinar propiedades de estabilidad con objetivos clásicos de alcanzabilidad o de tiempo de ramificación dentro de una única fórmula lógica.
3. Utilizar la verificación de modelos probabilística como un marco natural para el análisis de estabilidad dependiente del estado.

El artículo mantiene la modestia respecto al alcance de sus resultados de decidibilidad. Reconoce explícitamente que el problema general de verificación de modelos para propiedades PCTL no acotadas por pasos en los MJLS sigue siendo abierto y está estrechamente vinculado a problemas matemáticos de larga data (problema de Skolem). Además, señala limitaciones prácticas en la implementación: la computación exacta de los autovalores para matrices de dimensión superior a 4 es generalmente imposible debido al teorema de Abel-Ruffini, lo que significa que, para sistemas más grandes, el análisis depende de aproximaciones numéricas en lugar de soluciones simbólicas exactas. El artículo concluye que, si bien la lógica específica enriquecida con operadores de estabilidad (excluyendo el "hasta" general no acotado) es decidible mediante técnicas de álgebra lineal, la inversión de anidamiento (embeber fórmulas PCTL dentro de los operadores de estabilidad) no está soportada en el marco actual, y su problema de verificación de modelos también sería abierto.