Technische Samenvatting: Symbolisch Model Checking met Vectoren van Intervallen

1. Probleemstelling

Model checking is een robuuste formele verificatietechniek voor het waarborgen dat software- en hardwaresystemen voldoen aan specificaties. Het wordt echter ernstig gehinderd door het state space explosion problem (toestandsruimte-explosie), waarbij het aantal mogelijke toestanden en transities exponentieel groeit met de systeemgrootte. Deze uitdaging is bijzonder acuut bij global model checking, waarbij het doel is om alle toestanden te identificeren die een Computation Tree Logic (CTL) formule voldoen, in plaats van slechts één enkele configuratie te verifiëren.

Bestaande technieken, zoals Decision Diagrams (DD's), abstracties en partial order reduction, verzachten dit probleem, maar lopen tegen beperkingen aan naarmate modellen complexer worden. Specifiek: standaard interval-gebaseerde benaderingen (bijv. Interval Decision Diagrams) coderen verzamelingen van vectoren als vectoren van intervallen. Dit artikel betoogt dat een effectievere benadering voor Petri-netten het coderen van verzamelingen van markeringen is met behulp van gegeneraliseerde intervallen op vectoren (intervallen van vectoren), in plaats van vectoren van intervallen. Dit onderscheid is cruciaal omdat vectorruimten vaak niet-totale partiële orden bevatten, waardoor eenvoudige intervaldefinities ontoereikend zijn.

2. Methodologie

De auteurs stellen een nieuwe symbolische structuur voor, genaamd Symbolic Vector Sets (SVS), om verzamelingen van Petri-net markeringen te coderen. De methodologie is gebouwd op drie kernzuilen:

2.1. Symbolische Vectoren en Verzamelingen

Een Symbolische Vector wordt gedefinieerd als een paar $(a, b)$, waarbij $a$ en $b$ verzamelingen van vectoren (markeringen) zijn.

• Inclusie ($a$): Een markering $q$ behoort tot de symbolische vector als deze alle vectoren in $a$ bevat (onder een niet-strikte partiële orde $\subseteq_f$).
• Exclusie ($b$): Een markering $q$ behoort tot de symbolische vector als deze geen enkele vector in $b$ bevat.
• Generalisatie: Dit generaliseert het natuurlijke getalinterval $[a, b]$ (waarbij $a \le x \le b$) naar vectoren. Omdat vectoren niet altijd vergelijkbaar zijn, vereist de structuur een verzameling ondergrenzen ($a$) en een verzameling bovengrenzen ($b$) in plaats van enkele grenzen.

Een Symbolic Vector Set is een collectie van deze symbolische vectoren, die de unie vormt van hun onderliggende verzamelingen markeringen.

2.2. Canonieke Vorm en Operaties

Om efficiëntie te waarborgen en redundantie te voorkomen, definiëren de auteurs een canonieke vorm voor symbolische vectoren en verzamelingen. Belangrijke eigenschappen zijn:

• Uniciteit: Elke verzameling markeringen heeft precies één canonieke representatie.
• Homomorfe Operaties: Het artikel definieert homomorfe operaties (unie, doorsnede, verschil, negatie) die direct op de symbolische structuren opereren zonder ze te decoderen naar individuele markeringen.
• Mergebaarheid en Shareability: Om canoniciteit te behouden, introduceren de auteurs relaties om te bepalen wanneer twee symbolische vectoren kunnen worden samengevoegd of wanneer er een "shareable" component bestaat tussen hen. Dit omvat een lexicografische totale orde om ambiguïteiten in niet-totale partiële orden op te lossen, wat zorgt voor een deterministische afhandeling van overlappende restricties.

2.3. CTL Model Checking op Petri-netten

Het framework past deze structuren toe op Petri-netten met eindige capaciteiten.

• Pre-operatie: De kern van global model checking is de pre-operatie, die precedent-markeringen berekent. De auteurs definiëren een symbolische pre-operatie die werkt op symbolic vector sets, waarbij rekening wordt gehouden met de reversibiliteit van transities en capaciteitsrestricties.
• Fixpoint Evaluatie: CTL-formules (bijv. $EF$, $EG$, $EU$) worden geëvalueerd met behulp van fixpoint-berekeningen (kleinste en grootste fixpoints) over de symbolische vector sets. De voldoening van een formule wordt bepaald door te controleren of een markering deel uitmaakt van de resulterende symbolische vector set.

2.4. Optimalisaties

• Saturation (Verzadiging): Om het "peak effect" aan te pakken, waarbij tussenliggende oplossingen in fixpoint-berekeningen onnodig groot worden, implementeren de auteurs een saturation-strategie. Dit houdt in dat men iteratief werkt op capaciteitsgrenzen en eerdere resultaten gebruikt om daaropvolgende stappen te berekenen, wat het aantal tussenliggende symbolische vectoren aanzienlijk vermindert.
• Clustering: Het artikel vermeldt clustering als een potentiële optimalisatie voor bereikbaarheid, waarbij kleinere vectoren worden gecombineerd, hoewel dit wordt genoteerd als een concept voor toekomstige formele beschrijving.

3. Belangrijkste Bijdragen

1. Nieuwe Encoding: Introductie van Symbolic Vector Sets, een structuur die intervallen generaliseert naar vectoren, specifiek ontworpen om de niet-totale partiële orden van Petri-net markeringen te hanteren.
2. Formele Canonicalisering: Een rigoureuze definitie van een canonieke vorm voor symbolische vectoren en verzamelingen, inclus_ief bewijzen van uniciteit en de ontwikkeling van homomorfe operaties (unie, doorsnede, verschil, negatie) die deze canoniciteit behouden.
3. Global Model Checking Framework: Een volledig formalisme voor het evalueren van CTL-formules op Petri-netten met behulp van deze symbolische structuren, inclusief de definitie van de symbolische pre-operatie.
4. Saturation Algoritme: Een adaptatie van saturatieprincipes (afgeleid van andere symbolische technieken) in de context van symbolische vector sets om computationele pieken tijdens fixpoint-iteraties te mitigeren.
5. Implementatie (SVSKit): Een Swift-bibliotheek die de theorie implementeert, getest tegen benchmarks van de Model Checking Contest (MCC) 2022.

4. Resultaten

De auteurs hebben hun aanpak geëvalueerd met de SVSKit tool op voorbeelden uit de MCC 2022, specifiek het Circadian Clock model.

• Schaalbaarheid met Saturation: Experimenten op het Circadian Clock model (14 plaatsen, 16 transities) toonden aan dat saturation cruciaal is. Zonder saturation groeide de rekentijd exponentieel met de plaats-capaciteit (meer dan 5 uur voor capaciteit 6). Met saturation bleef de tijd constant (ca. 3,2s) voor capaciteiten van 2 en hoger, en bleef het aantal symbolische vectoren stabiel.
• Omgaan met Grote State Spaces: De tool kon capaciteiten tot $N=100.000$ succesvol aan, waarbij ongeveer $10^{84}$ markeringen werden gecodeerd met een uiteindelijke set van slechts 26 symbolische vectoren.
• Benchmark Prestaties: In de CTL fireability categorie van MCC 2022 slaagden bestaande tools (GreatSPN, ITS-Tools, Tapaal) er niet in om alle 16 queries binnen de limiet van 60 minuten te beantwoorden (Tapaal beantwoordde 9/16). De SVSKit-aanpak loste alle 16 queries op in ongeveer 30 minuten.
• Beperkingen: De auteurs erkennen dat de huidige implementatie te maken heeft met schaalbaarheidsproblemen door de worst-case complexiteit van canonieke operaties ($O(n!)$). De efficiëntie hangt sterk af van de implementatie van deze operaties, en de tool was beperkt tot relatief kleine Petri-netten in de benchmarks vanwege deze restricties.

5. Betekenis en Claims

Het artikel beweert een veelbelovend alternatief te bieden voor bestaande symbolische model checking technieken door te verschuiven van "vectoren van intervallen" naar "intervallen van vectoren".

• Theoretische Bijdrage: Het biedt een formeel algebraïsch framework voor het manipuleren van verzamelingen vectoren onder partiële orden, waarmee een gat in de literatuur wordt opgevuld waar dergelijke structuren voorheen stagneerden (verwijzend naar de oorspronkelijke "Predicate structures" van 30 jaar geleden).
• Praktische Haalbaarheid: De resultaten suggereren dat deze aanpak veel grotere of zelfs oneindige state spaces efficiënter kan afhandelen dan expliciete enumeratie en potentieel beter presteert dan huidige tools op specifieke globale model checking taken, met name die met grote capaciteiten.
• Toekomstige Richtingen: De auteurs suggereren bescheiden dat de huidige implementatie verfijning behoeft, met name wat betreft de optimalisatie van canonieke operaties. Ze stellen toekomstig werk voor in local model checking, het uitbreiden van de aanpak naar modellen buiten Petri-netten, en het integreren van deze methode met Decision Diagrams, waarbij zij stellen dat de twee benaderingen orthogonaal zijn en baat kunnen hebben bij hybridisatie.

Het artikel concludeert dat, hoewel de huidige implementatie beperkingen kent, de theoretische basis en de eerste experimentele resultaten het potentieel van symbolische vector sets voor globale model checking valideren.