Verification of Parametric Markov Automata under Time-bounded Reachability

Sintesi Tecnica: Verifica di Automi di Markov Parametrici sotto Raggiungibilità a Tempo Limitato

Definizione del Problema
Gli Automi di Markov (MA) sono un modello composizionale per sistemi stocastici deterministici e continui nel tempo, che fungono da semantica per modelli come le Reti di Petri Stocastiche Generalizzate e i Diagrammi di Guasto Dinamici. Tuttavia, gli algoritmi di model checking esistenti per gli MA richiedono modelli completamente specificati, dove tutti i tassi di transizione e le probabilità sono noti con precisione. Questa assunzione è spesso irrealistica per sistemi del mondo reale in cui i parametri possono essere soggetti a incertezza ambientale o essere sconosciuti.

Questo articolo affronta la verifica di Automi di Markov Parametrici (pMA), in cui i tassi di transizione e le distribuzioni probabilistiche dei successori sono definiti da funzioni parametriche piuttosto che da costanti fisse. Gli autori si concentrano sulle proprietà di raggiungibilità a tempo limitato (ad esempio, "La probabilità di raggiungere uno stato obiettivo entro il tempo $t$ è maggiore di $\theta$?"). Vengono affrontati due problemi specifici:

1. Verifica della Soddisfacibilità: Determinare se esiste una valutazione del parametro all'interno di una data regione che soddisfi o violi una proprietà.
2. Sintesi: Partizionare lo spazio dei parametri in regioni che soddisfano la proprietà e regioni che la violano.

L'analisi deve tenere conto di quattro distinti rapporti di soddisfazione basati sull'interazione tra lo scheduler del sistema (che compie scelte nondeterministiche) e la "natura" (che assegna i valori dei parametri): Feasibility (Fattibilità), Angelic-aid (Aiuto Angelico), Robust (Robusto) e Demonic (Demoniaco).

Metodologia
L'approccio proposto risolve questi problemi attraverso un processo in due fasi che trasforma il modello parametrico continuo in uno discreto adatto alle tecniche di sintesi esistenti, controllando al contempo l'errore introdotto.

1. Discretizzazione e Trasformazione:

   • Il pMA viene prima discretizzato utilizzando una dimensione del passo $\delta$, convertendo il modello a tempo continuo in un Processo Decisionale di Markov Parametrico (pMDP). Questo passaggio generalizza i precedenti risultati di discretizzazione per gli MA non parametrici.
   • Per gestire le transizioni immediate degli stati probabilistici (che avvengono senza trascorrere tempo), gli autori impiegano una tecnica di eliminazione degli stati. Gli stati probabilistici (PS) vengono accorpati in stati markoviani (MS), trasformando il modello in un problema standard di raggiungibilità a tempo limitato su un pMDP.
   • Poiché la discretizzazione introduce termini esponenziali ($e^{-\lambda \delta}$) difficili da gestire nella sintesi dei parametri simbolica, gli autori approcciano questi termini utilizzando espansioni di Taylor parziali. Ciò produce un "pMA discretizzato approssimato" in cui le probabilità di transizione sono rappresentate da funzioni razionali, vincolate da approssimazioni superiori e inferiori.

2. Parameter Lifting (PL) e Verifica:

   • Il pMDP trasformato viene analizzato utilizzando il Parameter Lifting (PL). Questa tecnica astrae le dipendenze tra gli stati trattando le scelte dei parametri come scelte nondeterministiche effettuate da un secondo giocatore ("la Natura") in un gioco stocastico.
   • Il metodo PL calcola i limiti superiori e inferiori della probabilità di raggiungibilità. Questi limiti vengono confrontati con la soglia specificata dall'utente $\theta$.
   • L'approccio utilizza uno schema di raffinamento: se i limiti sono inconcludenti (ovvero, l'intervallo attraversa la soglia), la regione del parametro viene partizionata e il processo viene ripetuto.
   • L'errore totale è governato da tre termini: l'errore di discretizzazione ($\epsilon_\delta$), l'errore dell'approssimazione di Taylor e l'errore introdotto dall'astrazione PL. Gli autori dimostrano che l'errore di discretizzazione è il fattore dominante.

Contributi Chiave

• Definizione di pMA: Il documento introduce formalmente gli Automi di Markov Parametrici, estendendo gli MA con funzioni di tasso e probabilistiche parametriche.
• Algoritmo per la Raggiungibilità a Tempo Limitato: Gli autori presentano il primo algoritmo capace di eseguire la verifica della soddisfabilità e la sintesi dei parametri per i pMA sotto vincoli di raggiungibilità a tempo limitato.
• Discretizzazione Generalizzata: Generalizzano i risultati di discretizzazione di Guck et al. [17] al contesto parametrico, dimostrando che il pMA discretizzato limita la vera probabilità di raggiungibilità del pMA.
• Discretizzazione Approssimata: Viene introdotto un metodo per gestire i termini esponenziali nel modello discretizzato tramite l'espansione di Taylor, consentendo l'uso di strumenti di sintesi basati su funzioni razionali.
• Implementazione: L'approccio è implementato utilizzando il model checker Storm (tramite l'interfaccia Stormpy) e supporta sia i pMA che i CTMC parametrici.

Risultati Sperimentali
Gli autori hanno valutato la loro implementazione su una suite di benchmark dal set di benchmark QCOMP, inclusi modelli come flexible-manufacturing, polling e kanban.

• Verifica: Per la verifica della soddisfabilità, lo strumento ha fornito risposte conclusive per tutti i benchmark testati, spesso in pochi secondi.
• Sintesi: Per la sintesi dei parametri, lo strumento ha partizionato con successo gli spazi dei parametri per i modelli più piccoli. Tuttavia, per modelli più grandi o complessi, il processo ha spesso raggiunto il timeout di 15 minuti.
• Colli di Bottiglia delle Prestazioni: L'analisi sperimentale identifica la discretizzazione come il principale collo di bottiglia delle prestazioni. Il costo computazionale aumenta significativamente man mano che la dimensione del passo di discretizzazione $\delta$ diminuisce (per ridurre l'errore) o man mano che il tasso massimo di sosta (sojourn rate) nel modello aumenta.
• Confronto: Rispetto a PRISM-PSY sui CTMC parametrici (dove PRISM-PSY non richiede la discretizzazione), il metodo proposto è stato più lento. Tuttavia, il metodo ha successo dove PRISM-PSY fallisce: può analizzare i pMA e i modelli con probabilità di transizione parametriche (non solo tassi), come il benchmark tandem.

Significatività e Rivendicazioni
Il documento sostiene di colmare una lacuna nella verifica formale consentendo l'analisi dell'incertezza negli Automi di Markov, una classe di modelli ampiamente utilizzata nell'ingegneria dell'affidabilità ma precedentemente limitata a istanze completamente specificate. Gli autori sottolineano che il loro approccio risolve i problemi di verifica e sintesi fino a un'arbitraria precisione, a condizione che la dimensione di discretizzazione sia sufficientemente piccola.

Gli autori rimangono modesti riguardo alla scalabilità, riconoscendo che l'implementazione attuale è limitata dal costo della discretizzazione. Affermano esplicitamente che i principali colli di bottiglia delle prestazioni derivano dalla discretizzazione del pMA. Di conseguenza, suggeriscono che il lavoro futuro debba investigare approcci che evitino interamente la discretizzazione, come l'analisi diretta di giochi stocastici a tempo continuo o l'utilizzo di tecniche di uniformizzazione, pur notando che queste alternative possono introdurre le proprie sfide computazionali. Il lavoro stabilisce un quadro fondamentale per l'analisi parametrica di sistemi nondeterministici a tempo continuo, estendendo le capacità degli strumenti esistenti come Storm per gestire l'incertezza parametrica in una classe più ampia di modelli.