Effective Stochastic Automata Model Checking by Interval Abstraction (extended version)

Dichiarazione del Problema
Gli Automi Stocastici (SA) sono un formalismo per modellare sistemi affidabili e ad alte prestazioni in cui i guasti dei componenti, la manutenzione e i tempi di servizio seguono distribuzioni di probabilità continue generali (ad esempio, Weibull, uniforme) piuttosto che le distribuzioni esponenziali richieste dalle Catene di Markov a Tempo Continuo (CTMC) o dai Reti di Petri Stocastiche Generalizzate (GSPN). Sebbene gli SA offrano una rappresentazione più realistica dei sistemi non-Markoviani, la loro analisi è complessa a causa della combinazione di tempo continuo, distribuzioni generali e scelte nondeterministiche.

Gli approcci di analisi esistenti affrontano limitazioni significative:

• Verifica Statistica del Modello (SMC): Strumenti come Fig utilizzano la simulazione Monte Carlo ma sono limitati agli SA (debolmente) deterministici, dove le probabilità di raggiungibilità minima e massima coincidono. Non possono gestire gli SA nondeterministici generali.
• Metodi Analitici: Algoritmi precedenti per gli SA generali (ad esempio, di Bryans et al.) si basano su "alberi di regioni" che richiedono integrali annidati che diventano impraticabili all'aumentare della profondità del modello, oppure utilizzano la discretizzazione che manca di supporto per gli strumenti. Altri formalismi come gli Automi Ibridi Stocastici (SHA) o gli Automi Temporizzati Stocastici (STA) esistono, ma il loro model checking soffre spesso di problemi di scalabilità a causa della complessità del raggiungimento ibrido o della rigidità della semantica degli orologi digitali (passi temporali fissi).

Metodologia
Il documento propone il primo approccio di model checking dedicato, generale ed efficace per gli SA basato sull'astrazione per intervalli. La metodologia principale consiste nel trasformare un SA a stato infinito in un Processo Decisionale di Markov (MDP) finito che sovra-approssima la semantica originale.

1. Astrazione per Intervalli: Invece di discretizzare l'esito del campionamento da una distribuzione di probabilità continua (CPD), il metodo partiziona il supporto di ciascuna distribuzione in un insieme finito di intervalli.

   • Il campionamento di un valore da una CPD è sostituito da un processo in due fasi: (1) una scelta probabilistica discreta di un intervallo (basata sulla massa di probabilità di quell'intervallo), seguita da (2) una scelta nondeterministica continua di un valore specifico all'interno di quell'intervallo.
   • Questo trasforma l'SA in un MDP in cui gli stati tracciano la posizione corrente e gli intervalli contenenti i possibili valori dei timer attivi.

2. Semantica dei Grandi Passi Temporali (Big Time Steps): L'approccio utilizza la semantica dei "grandi passi temporali" degli SA. Le transizioni avvengono solo quando un timer scade o un insieme di guardie è soddisfatto, piuttosto che ad ogni infinitesimo passo temporale. Ciò evita la complessità del "tempo denso" presente in altre semantiche.

   • L'astrazione propaga gli intervalli in modo simbolico. Quando un timer scade, il sistema transita verso un nuovo stato in cui l'intervallo del timer viene aggiornato o resettato.
   • L'MDP risultante è finito perché il numero di locazioni è finito e il numero di combinazioni di intervalli è fissato dalla partizione definita dall'utente.

3. Sovra-approssimazione e Limiti (Bounds):

   • La strategia dell'MDP può scegliere il valore preciso all'interno di un intervallo, mentre la semantica originale dell'SA prevede una scelta casuale. Ciò introduce il nondeterminismo che sovra-approssima il sistema originale.
   • Di conseguenza, il calcolo della probabilità di raggiungibilità massima sull'MDP fornisce un limite superiore per l'SA, mentre la probabilità di raggiungibilità minima fornisce un limite inferiore.
   • Il documento dimostra che man mano che gli intervalli diventano più piccoli, l'errore di approssimazione dovrebbe diminuire, sebbene la monotonicità non sia garantita con tutte le strategie di partizione.

4. Strumenti e Formalismi:

   • Gli autori hanno esteso il linguaggio di modellazione Modest e il formato di scambio Jani per supportare gli SA, inclusi la dichiarazione dei timer e gli insiemi di guardie.
   • Un prototipo implementato in Rust esegue l'astrazione per intervalli, costruisce l'MDP e calcola i limiti utilizzando la Iterazione di Valore (VI).

Contributi Chiave

• Primo Model Checker Dedicato per SA: Il documento presenta il primo approccio basato su strumenti per il model checking di SA generali che non è limitato a sottoclassi deterministiche.
• Astrazione per Intervalli per SA: Adatta l'astrazione per intervalli (precedentemente usata per SHA) specificamente per gli SA, sostituendo le scelte probabilistiche continue con scelte probabilistiche discrete seguite da scelte nondeterministiche continue, risultando in un MDP finito.
• Correttezza Formale: Gli autori forniscono una prova formale (Teorema 1) che stabilisce che le probabilità di raggiungibilità dell'MDP delimitano le vere probabilità dell'SA ($p_{min}^{MDP} \le p_{min}^{SA} \le p_{max}^{SA} \le p_{max}^{MDP}$).
• Estensioni del Linguaggio: L'estensione di Modest e Jani per supportare gli SA fornisce un'interfaccia di modellazione ad alto livello user-friendly e uno standard per lo scambio di modelli.
• Implementazione del Prototipo: Un prototipo in Rust dimostra la fattibilità dell'approccio.

Risultati Sperimentali
Gli autori hanno valutato il prototipo su tre set di esempi:

1. Piccoli Modelli SA: Includendo l'esempio di esecuzione e modelli dalla letteratura che distinguono le classi di strategia. Lo strumento ha calcolato con successo i limiti che approssimano da vicino le probabilità reali (ad esempio, approssimando 0,25 e 0,75 con i limiti [0,245, 0,755] usando 0,0125 di probabilità per intervallo).
2. Modelli di Code (Queueing Models): Code M/M/1 e Weibull/E6/1 non-Markoviane con limiti di buffer. Nonostante la generazione di MDP con milioni di stati (ad esempio, ~3,3 milioni di stati), lo strumento ha completato l'analisi in meno di 3 minuti su un laptop standard.
3. Modello di File Server: Un confronto con lo strumento mcsta (che usa orologi digitali per STA).
   • Per le distribuzioni uniformi, l'approccio SA ha ottenuto una maggiore accuratezza in meno del 30% del tempo di esecuzione rispetto a mcsta, largamente perché la semantica dei "grandi passi temporali" ha prodotto MDP significativamente più piccoli rispetto all'approccio dell'orologio digitale (che forza passi temporali di durata 1).
   • Per le distribuzioni esponenziali, gli intervalli a larghezza fissa di mcsta hanno performato meglio rispetto agli intervalli a probabilità uguale del prototipo, evidenziando come le strategie di generazione degli intervalli impattino le prestazioni. Gli autori notano che la raffinazione degli intervalli per timer è possibile nel loro approccio, a differenza del vincolo di larghezza fissa degli orologi digitali.

Significatività e Rivendicazioni
Il documento sostiene di introdurre un approccio di model checking generale ed efficace per gli SA che pone poche restrizioni sui modelli di input.

• Scalabilità: I risultati sperimentali suggeriscono che l'approccio scala bene per esempi non triviali, gestendo modelli con centinaia di migliaia o milioni di stati MDP, cosa che le precedenti tecniche analitiche non potevano gestire.
• Praticità: Nonostante sia un prototipo, lo strumento funziona bene per SA di dimensioni ragionevoli e fornisce utili limiti per l'analisi di sicurezza e prestazioni.
• Flessibilità: L'approccio supporta varie distribuzioni continue (Uniforme, Esponenziale, Erlang, Weibull) e caratteristiche complesse come le corse tra timer (timer races) e scelte nondeterministiche.

Gli autori rimangono modesti riguardo al processo di raffinazione, osservando che, sebbene intervalli più piccoli migliorino generalmente l'accuratezza, la relazione non è strettamente monotona con la loro attuale strategia di partizione, e una prova formale di convergenza rimane una sfida aperta. Posizionano questo lavoro come una base per futuri strumenti ottimizzati per le prestazioni ed estensioni a alberi di guasti dinamici e proprietà temporali limitate.