Verification of Parametric Markov Automata under Time-bounded Reachability

Technische Samenvatting: Verificatie van Parametrische Markov-automaten onder Tijdgebonden Bereikbaarheid

Probleemstelling
Markov-automaten (MA) zijn een compositioneel model voor niet-deterministische, continu-getimede stochastische systemen, die dienen als semantiek voor modellen zoals Generalized Stochastic Petri Nets en Dynamic Fault Trees. Echter, bestaande model checking-algoritmen voor MA vereisen volledig gespecificeerde modellen, waarbij alle transitieratent en kansverdelingen exact bekend zijn. Deze aanname is vaak onrealistisch voor real-world systemen waar parameters onderhevig kunnen zijn aan omgevingsonzekerheid of onbekendheid.

Dit artikel behandelt de verificatie van Parametrische Markov-automaten (pMA), waarbij transitieratent en probabilistische opvolgerverdelingen worden gedefinieerd door parametrische functies in plaats van vaste constanten. De auteurs richten zich op tijdgebonden bereikbaarheidseigenschappen (bijv. "Is de kans om een doeltoestand binnen tijd $t$ te bereiken groter dan $\theta$?"). Twee specifieke problemen worden aangepakt:

1. Verificatie van Verzadiging: Bepalen of er een parameterwaardering binnen een gegeven regio bestaat die een eigenschap verzadigt of schendt.
2. Synthese: Het partitioneren van de parameterruimte in regio's die de eigenschap verzadigen en regio's die de eigenschap schenden.

De analyse moet rekening houden met vier verschillende verzadigingsrelaties gebaseerd op de interactie tussen de scheduler van het systeem (die niet-deterministische keuzes maakt) en "de natuur" (die parameterwaarden toekent): Feasibility, Angelic-aid, Robust, en Demonic.

Methodologie
De voorgestelde aanpak lost deze problemen op via een tweestaps-proces dat het continue parametrische model transformeert naar een discreet model dat geschikt is voor bestaande synthesetechnieken, terwijl de geïntroduceerde fouten worden begrensd.

1. Discretisatie en Transformatie:

   • De pMA wordt eerst gediscretiseerd met behulp van een stapgrootte $\delta$, wat het continue-time model omzet in een Parametrische Markov-beslissingsproces (pMDP). Deze stap generaliseert eerdere discretisatieresultaten voor niet-parametrische MA's.
   • Om de onmiddellijke transities van probabilistische toestanden (die plaatsvinden zonder tijdsverloop) af te handelen, passen de auteurs een toestand-eliminatietechniek toe. Probabilistische toestanden (PS) worden samengevoegd tot Markoviaanse toestanden (MS), waardoor het model wordt getransformeerd tot een standaard stap-gebonden bereikbaarheidsprobleem op een pMDP.
   • Omdat de discretisatie exponentiële termen ($e^{-\lambda \delta}$) introduceert die moeilijk te hanteren zijn in symbolische parametersynthese, benaderen de auteurs deze termen met behulp van partiële Taylor-expansies. Dit levert een "benaderde gediscretiseerde pMA" op waarbij transitiekansen worden gerepresenteerd door rationale functies, begrensd door over- en onderbenaderingen.

2. Parameter Lifting (PL) en Verificatie:

   • Het getransformeerde pMDP wordt geanalyseerd met behulp van Parameter Lifting (PL). Deze techniek abstraheert inter-toestand afhankelijkheden door parameterkeuzes te behandelen als niet-deterministische keuzes gemaakt door een tweede speler ("de Natuur") in een stochastisch spel.
   • De PL-methode berekent boven- en ondergrenzen voor de bereikbaarheidskans. Deze grenzen worden vergeleken met de door de gebruiker gespecificeerde drempelwaarde $\theta$.
   • De aanpak maakt gebruik van een verfijningsschema: als de grenzen inconclusief zijn (d.w.z. het interval overschrijdt de drempelwaarde), wordt de parameterregio gepartitioneerd en wordt het proces herhaald.
   • De totale fout wordt beheerst door drie termen: de discretiefout ($\epsilon_\delta$), de fout van de Taylor-benadering, en de fout geïntroduceerd door de PL-abstractie. De auteurs tonen aan dat de discretiefout de dominante factor is.

Belangrijkste Bijdragen

• Definitie van pMA: Het artikel introduceert formeel Parametrische Markov-automaten, waarbij MA's worden uitgebreid met parametrische rate- en probabilistische functies.
• Algoritme voor Tijdgebonden Bereikbaarheid: De auteurs presenteren het eerste algoritme dat in staat is tot het uitvoeren van verzadigingsverificatie en parametersynthese voor pMA's onder tijdgebonden bereikbaarheidsrestricties.
• Gegeneraliseerde Discretisatie: Zij generaliseren de discretiseringsresultaten van Guck et al. [17] naar de parametrische setting, waarbij zij bewijzen dat de gediscretiseerde pMA de ware bereikbaarheidskans van de pMA begrenst.
• Benaderde Discretisatie: Een methode wordt geïntroduceerd om exponentiële termen in het gediscretiseerde model af te handelen via Taylor-expansie, wat het gebruik van op rationale functies gebaseerde synthesetools mogelijk maakt.
• Implementatie: De aanpak is geïmplementeerd met de Storm model checker (via de Stormpy-interface) en ondersteunt zowel pMA's als parametrische CTMC's.

Experimentele Resultaten
De auteurs hebben hun implementatie geëvalueerd op een suite van benchmarks uit de QCOMP benchmark set, waaronder modellen zoals flexible-manufacturing, polling, en kanban.

• Verificatie: Voor de verificatie van verzadiging leverde de tool succesvol concludente antwoorden voor alle geteste benchmarks, vaak binnen enkele seconden.
• Synthese: Voor parametersynthese slaagde de tool erin om de parameterruimtes te partitioneren voor kleinere modellen. Echter, voor grotere of complexere modellen bereikte het proces regelmatig de 15-minuten timeout.
• Prestatieknelpunten: De experimentele analyse identificeert discretisatie als het primaire prestatieknelpunt. De computationele kosten nemen significant toe naarmate de discretisatiestap $\delta$ kleiner wordt (om de fout te verminderen) of naarmate de maximale verblijfsrate (sojourn rate) in het model toeneemt.
• Vergelijking: Wanneer vergeleken met PRISM-PSY op parametrische CTMC's (waar PRISM-PSY geen discretisatie vereist), was de voorgestelde methode langzamer. De methode slaagt echter daar waar PRISM-PSY faalt: het kan pMA's en modellen met parametrische transitiekansen (niet alleen raten) analyseren, zoals de tandem benchmark.

Betekenis en Claims
Het artikel beweert een gat in de formele verificatie te overbruggen door de analyse van onzekerheid in Markov-automaten mogelijk te maken, een modelklasse die breed wordt gebruikt in reliability engineering maar voorheen beperkt was tot volledig gespecificeerde instanties. De auteurs benadrukken dat hun aanpak de verificatie- en syntheseproblemen oplost tot een willekeurige precisie, mits de discretisatiestap voldoende klein is.

De auteurs blijven bescheiden over de schaalbaarheid en erkennen dat de huidige implementatie wordt beperkt door de kosten van discretisatie. Zij stellen expliciet dat de belangrijkste prestatieknelpunten voortkomen uit de discretisatie van de pMA. Bijgevolg suggereren zij dat toekomstig werk onderzoek moet doen naar benaderingen die discretisatie volledig vermijden, zoals het direct analyseren van continuous-time stochastic games of het gebruik van uniformisatietechnieken, hoewel zij opmerken dat deze alternatieven hun eigen computationele uitdagingen met zich mee kunnen brengen. Het werk legt een fundamenteel kader vast voor de parametrische analyse van continuous-time niet-deterministische systemen, waarmee de mogelijkheden van bestaande tools zoals Storm wordt uitgebreid naar het hanteren van parametrische onzekerheid in een bredere klasse van modellen.