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

Probleemstelling
Stochastische Automata (SA) zijn een formalisme voor het modelleren van betrouwbare en hoogwaardige systemen waarbij componentfouten, onderhoud en servicetijden volgen door algemene continue kansverdelingen (bijv. Weibull, uniform) in plaats van de exponentiële verdelingen die vereist zijn voor Continuous-Time Markov Chains (CTMCs) of Generalized Stochastic Petri Nets (GSPNs). Hoewel SA een meer realistische representatie bieden van niet-Markoviaanse systemen, is hun analyse uitdagend vanwege de combinatie van continue tijd, algemene verdelingen en nondeterministische keuzes.

Bestaande analysemethoden kampen met aanzienlijke beperkingen:

• Statistical Model Checking (SMC): Tools zoals Fig maken gebruik van Monte Carlo-simulaties, maar zijn beperkt tot (zwak) deterministische SA, waarbij de minimale en maximale bereikbaarheidskansen samenvallen. Ze kunnen algemene nondeterministische SA niet aan.
• Analytische Methoden: Eerdere algoritmen voor algemene SA (bijv. door Bryans et al.) vertrouwen op "regio-trees" die geneste integralen vereisen, wat onhaalbaar wordt naarmate de modeldiepte toeneemt, of ze gebruiken discretisatie die een gebrek aan toolondersteuning heeft. Andere formalismen zoals Stochastic Hybrid Automata (SHA) of Stochastic Timed Automata (STA) bestaan wel, maar hun model checking lijdt vaak aan schaalbaarheidsproblemen vanwege de complexiteit van hybride bereikbaarheid of de rigiditeit van digitale kloksemantiek (vaste tijdstappen).

Methodologie
Het artikel stelt de eerste specifieke, algemene en effectieve model checking-aanpak voor SA voor, gebaseerd op intervalabstractie. De kernmethodologie bestaat uit het transformeren van een oneindig-toestands SA naar een eindige Markov Decision Process (MDP) die de oorspronkelijke semantiek overbenadert.

1. Intervalabstractie: In plaats van de uitkomst van het bemonsteren uit een continue kansverdeling (CPD) te discretiseren, verdeelt de methode het steungebied van elke verdeling in een eindige verzameling intervallen.

   • Het bemonsteren van een waarde uit een CPD wordt vervangen door een tweestaps-proces: (1) een discrete probabilistische keuze van een interval (gebaseerd op de kansmassa van dat interval), gevolgd door (2) een continue nondeterministische keuze van een specifieke waarde binnen dat interval.
   • Dit transformeert de SA naar een MDP waarbij toestanden de huidige locatie en de intervallen bevatten die de mogelijke waarden van actieve timers bevatten.

2. Big Time Steps Semantiek: De aanpak maakt gebruik van de "big time steps" semantiek van SA. Transities vinden alleen plaats wanneer een timer verloopt of een guard-set wordt voldaan, in plaats van bij elke infinitesimale tijdstap. Dit voorkomt de "dense time" complexiteit die wordt gevonden in andere semantieken.

   • De abstractie propageert intervallen symbolisch. Wanneer een timer verloopt, gaat het systeem over naar een nieuwe toestand waar het interval van de timer wordt bijgewerkt of gereset.
   • De resulterende MDP is eindig omdat het aantal locaties eindig is en het aantal intervalcombinaties wordt bepaald door de door de gebruiker gedefinieerde partitie.

3. Overbenadering en Grenzen:

   • De MDP-strategie kan de exacte waarde binnen een interval kiezen, terwijl de oorspronkelijke SA-semantiek een willekeurige keuze inhoudt. Dit introduceert nondeterminisme dat de oorspronkelijke SA overbenadert.
   • Bijgevolg levert het berekenen van de maximale bereikbaarheidskans op de MDP een bovengrens voor de SA op, en de minimale bereikbaarheidskans levert een ondergrens op.
   • Het artikel bewijst dat naarmate de intervallen kleiner worden, de benaderingsfout naar verwachting afneemt, hoewel monotoniciteit niet gegarandeerd is bij alle partitioneringsstrategieën.

4. Tooling en Formalismen:

   • De auteurs hebben de Modest modellerings taal en het Jani interchange formaat uitgebreid om SA te ondersteunen, inclusief timer-declaraties en guard-sets.
   • Een prototype tool geïmplementeerd in Rust voert de intervalabstractie uit, construeert de MDP en berekent grenzen met behulp van Value Iteration (VI).

Belangrijkste Bijdragen

• Eerste Specifieke SA Model Checker: Het artikel presenteert de eerste tool-gebaseerde aanpak voor het model checken van algemene SA die niet beperkt is tot deterministische subklassen.
• Intervalabstractie voor SA: Het past intervalabstractie (voorheen gebruikt voor SHA) specifiek toe op SA, waarbij continue probabilistische keuzes worden vervangen door discrete probabilistische gevolgd door continue nondeterministische keuzes, wat resulteert in een eindige MDP.
• Formele Correctheid: De auteurs leveren een formeel bewijs (Theorem 1) dat vaststelt dat de bereikbaarheidskansen van de MDP de ware kansen van de SA begrenzen ($p_{min}^{MDP} \le p_{min}^{SA} \le p_{max}^{SA} \le p_{max}^{MDP}$).
• Taaluitbreidingen: De uitbreiding van Modest en Jani om SA te ondersteunen, biedt een gebruiksvriendelijke high-level modelleringsinterface en een standaard voor modeluitwisseling.
• Prototype Implementatie: Een Rust-gebaseerd prototype demonstreert de haalbaarheid van de aanpak.

Experimentele Resultaten
De auteurs hebben de prototype geëvalueerd op drie sets voorbeelden:

1. Kleine SA Modellen: Inclusief het lopende voorbeeld en modellen uit de literatuur die strategieklassen onderscheiden. De tool berekende succesvol grenzen die de ware kansen nauwkeurig benaderden (bijv. het benaderen van 0,25 en 0,75 met grenzen [0,245, 0,755] met behulp van 0,0125 per-interval kans).
2. Queueing Modellen: Niet-Markoviaanse M/M/1 en Weibull/E6/1 wachtrijen met bufferlimieten. Ondanks het genereren van MDP's met miljoenen toestanden (bijv. ~3,3 miljoen toestanden), voltooide de tool de analyse in minder dan 3 minuten op een standaard laptop.
3. File Server Model: Een vergelijking met de mcsta tool (die digitale klokken gebruikt voor STA).
   • Voor uniforme verdelingen bereikte de SA-aanpak een hogere nauwkeurigheid in minder dan 30% van de runtime vergeleken met mcsta, grotendeels omdat de "big time steps" semantiek resulteerde in aanzienlijk kleinere MDP's dan de digitale klok-aanpak (die tijdstappen van duur 1 afdwingt).
   • Voor exponentiële verdelingen presteerden de vaste-breedte intervallen van mcsta beter dan de gelijke-kans intervallen van de prototype, wat benadrukt dat intervalgeneratiestrategieën de prestaties beïnvloeden. De auteurs merken op dat het verfijnen van intervallen per timer mogelijk is in hun aanpak, in tegen tegenstelling tot de vaste-breedte beperking van digitale klokken.

Betekenis en Claims
Het artikel claimt een algemene en effectieve model checking-aanpak voor SA te introduceren die weinig restricties oplegt aan invoermodellen.

• Schaalbaarheid: De experimentele resultaten suggereren dat de aanpak goed schaalt voor niet-triviale voorbeelden, waarbij modellen met honderdduizenden tot miljoenen MDP-toestanden worden afgehandeld, wat eerdere analytische technieken niet konden beheren.
• Praktische Bruikbaarheid: Ondanks dat het een prototype is, werkt de tool goed voor redelijk grote SA en biedt het nuttige grenzen voor veiligheids- en prestatieanalyse.
• Flexibiliteit: De aanpak ondersteunt diverse continue verdelingen (Uniform, Exponential, Erlang, Weibull) en complexe functies zoals timer races en nondeterministische keuzes.

De auteurs blijven bescheiden over het verfijningsproces en merken op dat hoewel kleinere intervallen de nauwkeurigheid over het algemeen verbeteren, de relatie niet strikt monotoon is met hun huidige partitioneringsstrategie, en een formeel convergentiebewijs een openstaand vraagstuk blijft. Zij positioneren dit werk als een fundament voor toekomstige prestatie-geoptimaliseerde tools en uitbreidingen naar dynamische faaltabellen en tijdgebonden eigenschappen.