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

Sintesi Tecnica: Verifica della Stabilità di Sistemi Lineari a Salti di Markov tramite Logica Temporale Probabilistica

Enunciato del Problema
I Sistemi Lineari a Salti di Markov (MJLS) modellano fenomeni dinamici soggetti a commutazioni casuali tra molteplici modalità lineari, governate da una catena di Markov a tempo discreto sottostante. L'analisi classica della stabilità per gli MJLS si basa su nozioni globali come la stabilità media (MS) e la stabilità media al quadrato (MSS), che caratterizzano il comportamento asintotico del primo e del secondo momento dello stato del sistema. Questi approcci classici sono tipicamente troppo conservativi o fuorvianti nella pratica. Nello specifico, l'instabilità potrebbe derivare solo da un sottoinsieme trascurabile di stati iniziali (ad esempio, configurazioni fisicamente irraggiungibili), mentre il sistema rimane stabile per tutti gli stati praticamente rilevanti. Al contrario, un sistema potrebbe convergere per tutti gli stati iniziali ma verso valori limite differenti, fallendo la stretta definizione di stabilità (che richiede la convergenza verso un valore comune, tipicamente l'origine), nonostante presenti un comportamento di convergenza desiderabile.

Il presente lavoro affronta il vuoto nella letteratura riguardante la verifica delle proprietà di stabilità rispetto a specifici insiemi prefissati di stati iniziali. Ciò viene inquadrato come un problema di model-checking, dove l'obiettivo è determinare se specifiche proprietà temporali riguardanti la convergenza dei momenti valggano per un dato sottoinsieme dello spazio degli stati.

Metodologia
Gli autori affrontano il problema integrando l'analisi della stabilità nel framework della Logica Computazionale ad Albero Probabilistica (PCTL).

1. Formalizzazione della PCTL sugli MJLS:
   Il documento formalizza innanzitutto la PCTL standard per gli MJoli. Lo spazio degli stati è definito come $S_J = \mathbb{R}^n \times \{1, \dots, m\}$, combinando variabili di stato continue con modalità Markoviane discrete. Le proposizioni atomiche sono definite su politopi convessi per gli stati continui e modalità specifiche per gli stati discreti. La relazione di soddisfacimento è definita su cammini infiniti, con probabilità calcolate su insiemi cilindrici derivati dalla catena di Markov sottostante.

2. Limitazioni del Model Checking Generale della PCTL:
   Gli autori analizzano la decidibilità della logica PCTL completa (inclus dell'operatore "until" non limitato) sugli MJLS. Essi stabiliscono che gli MJLS possono essere incorporati in Processi di Markov Generali (GMP). Sfruttando il fatto che i Sistemi Dinamici Lineari (LDS) sono un caso deterministico speciale di MJLS, dimostrano che il problema della raggiungibilità per la PCTL sugli MJLS eredita i risultati di indecidibilità associati al problema di Skolem. Nello specifico, determinare la raggiungibilità per insiemi di dimensione quattro o superiore negli LDS è un problema aperto, il che implica che il problema generale di model-checking per la PCTL sugli MJLS (oltre al frammento limitato ai passi $PCTL^-$) è anch'esso aperto e probabilmente indecidibile.

3. Estensione con Operatori di Stabilità:
   Per superare i limiti delle definizioni globali di stabilità e l'indecidibilità del model-checking generale della raggiungibilità, gli autori estendono la PCTL con nuovi operatori atomici che catturano le proprietà di stabilità basate sui momenti rispetto a specifici stati iniziali.

   • Operatori: Introducono operatori limitati ai passi ($E^k_\Pi, V^k_\Xi$) e non limitati ai passi ($E_\Pi, V_\Xi$).
     • $E_\Pi$ e $V_\Xi$ verificano se il limite di Cesàro (limite della media temporale) del primo momento (valore atteso) e del secondo momento (varianza non centrata), rispettivamente, ricade entro un determinato politopo convesso ($\Pi$ o $\Xi$).
     • Questi operatori utilizzano il limite di Cesàro invece dei limiti puntuali per gestire comportamenti oscillatori che potrebbero non convergere puntualmente, ma possiedono una media ben definita.
   • Approccio Algebrico: La verifica di questi nuovi operatori si basa su tecniche di algebra lineare piuttosto che sulla generale analisi della raggiungibilità.
     • L'evoluzione dei momenti condizionali è governata da operatori lineari: $B_J$ per il primo momento e $T_J$ per il secondo momento.
     • L'insieme di soddisfacimento per gli operatori non limitati ai passi viene computato analizzando le proprietà spettrali (autovalori e autovettori/blocchi di Jordan) di tali operatori.
     • Per operatori diagonalizzabili, il limite è determinato dalla proiezione dello stato iniziale sull'autospazio corrispondente agli autovalori sulla circonferenza unitaria.
     • Per operatori non diagonalizzabili, gli autori impiegano la forma normale di Jordan per computare i limiti in modo simbolico, gestendo i casi in cui i termini divergono o si annullano.

Contributi Chiave e Risultati

• Framework Logico: Il documento fornisce una semantica formale per la PCTL sugli MJLS ed estende la stessa con operatori che permettono di specificare la stabilità rispetto a specifici insiemi di stati iniziali.
• Verifica Algoritmica:
  • Viene fornito un procedimento decisionale per il frammento limitato ai passi ($PCTL^-$) e per i nuovi operatori di stabilità ($E_\Pi, V_\Xi$, ecc.).
  • Gli algoritmi per gli operatori di stabilità riducono il problema di verifica alla risoluzione di sistemi di equazioni lineari e alla verifica dell'appartenenza a politopi convessi. Ciò assicura che gli insiemi di soddisfacimento risultanti siano rappresentabili (come insiemi convessi o loro unioni) e computazionalmente trattabili, a condizione che gli autovalori possano essere calcolati.
  • Gli autori dimostrano che, mentre il problema generale di model-checking per la PCTL sugli MJLS è aperto a causa delle connessioni con il problema di Skolem, il frammento specifico relativo alla stabilità dei momenti è decidibile tramite algebra lineare.
• Gestione delle Oscillazioni: Utilizzando i limiti di Cesàro, gli operatori proposti catturano una nozione di convergenza che rimane ben definita anche quando le sequenze dei momenti oscillano, contrastando con le definizioni classiche che potrebbero fallire in tali casi.
• Casi di Studio: Il documento include esempi computazionali (ad esempio, un MJLS a 3 modalità con 2 variabili di stato) che visualizzano gli insiemi di soddisfacimento per formule come $P_{\ge 0.3}(\Lambda \mathcal{U}_{\le 5} E_\Pi)$, dimostrando la capacità di identificare regioni dello spazio degli stati che soddisfano complessi requisiti di stabilità e raggiungibilità.

Significato e Rivendicazioni
Gli autori affermano che il loro lavoro consente una visione "raffinata" della stabilità degli MJLS che era precedentemente impossibile da esprimere o decidere. Allontanandosi dalle garanzie globali, il framework permette agli analisti di:

1. Identificare proprietà di stabilità per specifici sottoinsiemi di condizioni iniziali praticamente rilevanti, evitando il conservatorismo dell'analisi globale.
2. Combinare le proprietà di stabilità con obiettivi classici di raggiungibilità o di tempo di ramificazione (branching-time) all'interno di una singola formula logica.
3. Utilizzare il model-checking probabilistico come un framework naturale per l'analisi della stabilità dipendente dallo stato.

Il documento rimane modesto riguardo all'ambito dei suoi risultati di decidibilità. Esso riconosce esplicitamente che il problema generale di model-checking per le proprietà PCTL non limitate ai passi sugli MJLS rimane aperto ed è strettamente legato a problemi matematici di lunga data (problema di Skolem). Inoltre, nota i limiti pratici nell'implementazione: il calcolo esatto degli autovalori per matrici di dimensione superiore a 4 è generalmente impossibile a causa del teorema di Abel-Ruffini, il che significa che per sistemi più grandi, l'analisi si affida ad approssimazioni numeriche piuttosto che a soluzioni simboliche esatte. Il documento conclude che, sebbene la specifica logica arricchita con operatori di stabilità (escludendo l'unbounded "until" generale) sia decidibile tramite tecniche di algebra lineare, la conversione inversa (l'inserimento di formule PCTL all'interno di operatori di stabilità) non è supportata nell'attuale framework, e il relativo problema di model-checking sarebbe anch'esso aperto.