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

Résumé Technique : Vérification de la Stabilité des Systèmes Linéaires à Sauts de Markov via la Logique Temporelle Probabiliste

Énoncé du Problème
Les systèmes linéaires à sauts de Markov (MJLS - Markov Jump Linear Systems) modélisent des phénomènes dynamiques soumis à des commutations aléatoires entre plusieurs modes linéaires, régies par une chaîne de Markov à temps discret sous-jacente. L'analyse de stabilité classique pour les MJLS repose sur des notions globales telles que la stabilité en moyenne (MS - Mean Stability) et la stabilité au sens du carré moyen (MSS - Mean-Square Stability), qui caractérisent le comportement asymptotique du premier et du second moment de l'état du système. Ces approches classiques exigent généralement des garanties de stabilité pour toutes les conditions initiales. Les auteurs soutiennent que cette perspective globale peut être excessivement conservatrice ou trompeuse en pratique. Plus précisément, l'instabilité peut ne survenir que pour un sous-ensemble négligeable d'états initiaux (par exemple, des configurations physiquement inaccessibles), tandis que le système reste stable pour tous les états pratiquement pertinents. Inversement, un système peut converger pour toutes les conditions initiales mais vers des valeurs limites différentes, échouant ainsi à la définition stricte de la stabilité (qui exige la convergence vers une valeur commune, typiquement l'origine), malgré un comportement de convergence souhaitable.

L'article traite de la lacune dans la littérature concernant la vérification des propriétés de stabilité par rapport à des ensembles spécifiques d'états initiaux. Cela est formulé comme un problème de model-checking, où l'objectif est de déterminer si des propriétés temporelles spécifiques concernant la convergence des moments sont satisfaites pour un sous-ensemble donné de l'espace d'états.

Méthodologie
Les auteurs abordent le problème en intégrant l'analyse de stabilité dans le cadre de la logique PCTL (Probabilistic Computation Tree Logic).

1. Formalisation de la PCTL sur les MJLS :
   Le papier formalise d'abord la PCTL standard pour les MJLS. L'espace d'états est défini par $S_J = \mathbb{R}^n \times \{1, \dots, m\}$, combinant des variables d'état continues avec des modes de Markov discrets. Les propositions atomiques sont définies sur des polytopes convexes pour les états continus et sur des modes spécifiques pour les états discrets. La relation de satisfaction est définie sur des chemins infinis, les probabilités étant calculées sur des ensembles cylindriques dérivés de la chaîne de Markov sous-jacente.

2. Limitations du Model-Checking Général de la PCTL :
   Les auteurs analysent la décidabilité de la logique PCTL complète (incluant l'opérateur "jusqu'à" [until] non borné) sur les MJLS. Ils établissent que les MJLS peuvent être intégrés dans les processus de Markov généraux (GMP - General Markov Processes). En exploitant le fait que les systèmes linéaires dynamiques (LDS) sont un cas particulier déterministe des MJLS, ils démontent que le problème de raggiungibilité pour la PCTL sur les MJLS hérite des résultats d'indécidabilité associés au problème de Skolem. Plus précisément, déterminer la raggiungibilité pour des ensembles de dimension quatre ou supérieure dans les LDS est un problème ouvert, ce qui implique que le problème général de model-checking pour la PCTL sur les MJLS (au-delà du fragment borné par étapes $PCTL^-$) est également ouvert et probablement indécidable.

3. Extension avec des Opérateurs de Stabilité :
   Pour surmonter les limitations des définitions globales de stabilité et l'indécidabilité de la raggiungibilité générale, les auteurs étendent la PCTL avec de nouvelles propositions atomiques qui capturent les propriétés de stabilité basées sur les moments par rapport à des états initiaux spécifiques.

• Opérateurs : Ils introduisent des opérateurs bornés par étapes ($E^k_\Pi, V^k_\Xi$) et non bornés par étapes ($E_\Pi, V_\Xi$).
  • $E_\Pi$ et $V_\Xi$ vérifient si la limite de Cesàro (limite de la moyenne temporelle) du premier moment (espérance mathématique) et du second moment (variance non centrée), respectivement, se situe dans un polytope convexe spécifié ($\Pi$ ou $\Xi$).
  • Ces opérateurs utilisent la limite de Cesàro plutôt que des limites ponctuelles pour gérer les comportements oscillatoires qui peuvent ne pas converger ponctuellement mais possèdent une moyenne bien définie.
• Approche Algébrique : La vérification de ces nouveaux opérateurs repose sur des techniques d'algèbre linéaire plutôt que sur une analyse de raggiungibilité générale.
  • L'évolution des moments conditionnels est régie par des opérateurs linéaires : $B_J$ pour le premier moment et $T_J$ pour le second moment.
  • L'ensemble de satisfaction pour les opérateurs non bornés est calculé en analysant les propriétés spectrales (valeurs propres et vecteurs propres/blocs de Jordan) de ces opérateurs.
  • Pour les opérateurs diagonalisables, la limite est déterminée par la projection de l'état initial sur le sous-espace propre correspondant aux valeurs propres sur le cercle unité.
  • Pour les opérateurs non diagonalisables, les auteurs emploient la forme normale de Jordan pour calculer les limites de manière symbolique, en gérant les cas où les termes divergent ou s'annulent.

Contributions Clés et Résultats

• Cadre Logique : Le papier fournit une sémantique formelle pour la PCTL sur les MJLS et l'étend avec des opérateurs pour spécifier la stabilité par rapport à des ensembles d'états initiaux spécifiques.
• Vérification Algorithmique :
  • Une procédure de décision est fournie pour le fragment borné par étapes ($PCTL^-$) et pour les nouveaux opérateurs de stabilité ($E_\Pi, V_\Xi$, etc.).
  • Les algorithmes pour les opérateurs de stabilité réduisent le problème de vérification à la résolution de systèmes d'équations linéaires et à la vérification de l'appartenance à des polytopes convexes. Cela garantit que les ensembles de satisfaction résultants sont représentables (comme des ensembles convexes ou des unions de ceux-ci) et calculables, sous réserve que les valeurs propres puissent être calculées.
  • Les auteurs démontrent que, bien que le problème de model-checking général de la PCTL soit ouvert en raison de ses connexions avec le problème de Skolem, le fragment spécifique traitant de la stabilité des moments est décidable via l'algèbre linéaire.
• Gestion des Oscillations : En utilisant les limites de Cesàro, les opérateurs proposés capturent une notion de convergence qui reste bien définie même lorsque les séquences de moments oscillent, contrastant avec les définitions classiques qui pourraient échouer dans de tels cas.
• Études de Cas : Le papier inclut des exemples de calcul (par exemple, un MJLS à 3 modes avec 2 variables d'état) visualisant les ensembles de satisfaction pour des formules telles que $P_{\ge 0.3}(\Lambda \mathcal{U}_{\le 5} E_\Pi)$, démontrant la capacité d'identifier des régions de l'espace d'états qui satisfont des exigences complexes de stabilité et de raggiungibilité.

Signification et Revendications
Les auteurs affirment que leur travail permet une vue "raffinée" de la stabilité des MJLS qui était auparavant impossible à exprimer ou à décider. En s'éloignant des garanties globales, le cadre permet aux analystes de :

1. Identifier des propriétés de stabilité pour des sous-ensembles d'états initiaux spécifiques et pratiquement pertinents, évitant ainsi le conservatisme de l'analyse globale.
2. Combiner les propriétés de stabilité avec la raggiungibilité classique ou des objectifs de temps de branchement au sein d'une seule formule logique.
3. Utiliser le model-checking probabiliste comme un cadre naturel pour l'analyse de stabilité dépendante de l'état.

Le papier reste modeste quant à la portée de ses résultats de décidabilité. Il reconnaît explicitement que le problème de model-checking général des propriétés PCTL non bornées par étapes sur les MJLS reste ouvert et est étroitement lié à des problèmes mathématiques de longue date (problème de Skolem). De plus, il note des limitations pratiques en termes d'implémentation : le calcul exact des valeurs propres pour des matrices de dimension supérieure à 4 est généralement impossible en raison du théorème d'Abel-Ruffini, ce qui signifie que pour des systèmes plus larges, l'analyse repose sur des approximations numériques plutôt que sur des solutions symboliques exactes. Le papier conclut que, bien que la logique spécifique enrichie d'opérateurs de stabilité (excluant l'opérateur "jusqu'à" général non borné) soit décidable via des techniques d'algèbre linéaire, l'imbrication inverse (insérer des formules PCTL à l'intérieur des opérateurs de stabilité) n'est pas supportée dans le cadre actuel, et son problème de model-checking serait également ouvert.