StochasticBarrier.jl: A Toolbox for Stochastic Barrier Function Synthesis

Dit artikel introduceert StochasticBarrier.jl, een open-source Julia-toolbox die Sum-of-Squares- en piecewise-constant-methoden gebruikt om stochastische barrièrefuncties te synthetiseren voor de veiligheidsverificatie van discrete tijd-stochastische systemen, en die in benchmarks aanzienlijk sneller en schaalbaarder blijkt dan bestaande tools.

De kern

Stel je voor dat je een zelfrijdende auto of een drone bestuurt in een wereld vol met onvoorspelbare factoren: een plotselinge windvlaag, een glazige weg, of een sensor die even mist. De grote vraag is: Hoe kunnen we met 100% zekerheid weten dat deze machine veilig blijft, zonder ooit een ongeluk te veroorzaken?

Dit is precies waar het nieuwe computerprogramma StochasticBarrier.jl voor is ontwikkeld. In dit artikel leggen we uit wat het doet, waarom het zo speciaal is, en hoe het werkt, maar dan in gewone mensentaal.

1. Het Probleem: De "Onzichtbare Muur"

In de wereld van robotica en autonome systemen willen we een veiligheidsgebied hebben (bijvoorbeeld: "blijf binnen de weg"). Omdat er altijd ruis is (zoals wind of meetfouten), kunnen we niet zeker weten waar de robot precies zal zijn.

Wetenschappers gebruiken iets genaamd een "Stochastische Barrièrefunctie".

• De analogie: Denk aan een onzichtbare, magische muur rondom het veilige gebied.
• Hoe het werkt: Als de robot deze muur probeert te raken, zegt de wiskunde: "Nee, de kans dat je erdoorheen breekt is zo klein dat we het als veilig kunnen beschouwen."
• Het doel: Een wiskundig bewijs vinden dat deze muur onbreekbaar is, zelfs als de robot door de wind wordt geduwd.

2. De Oplossing: StochasticBarrier.jl

De onderzoekers (van universiteiten in de VS en Nederland) hebben een nieuw gereedschap gemaakt, geschreven in de programmeertaal Julia.

Stel je voor dat je eerder moest bouwen met zware, trage stenen (oude software in MATLAB of Python). StochasticBarrier.jl is als een lichtgewicht, supersnel 3D-printer. Het kan in een flits berekenen of die "magische muur" bestaat.

Wat maakt dit gereedschap uniek?

1. Het is razendsnel: Het is tot 1000 keer sneller dan de beste bestaande tools. Wat voorheen een uur duurde, doet dit programma in seconden.
2. Het is slim: Het kan niet alleen met simpele, rechte lijnen werken, maar ook met complexe, gebogen paden (niet-lineaire systemen).
3. Het is flexibel: Het heeft drie verschillende "motoren" om de muur te bouwen:
   • De wiskundige perfectionist (SOS): Bouwt een zeer nauwkeurige, gladde muur.
   • De bouwkundige (PWC): Bouwt de muur van blokken (zoals lego). Dit is vaak sneller en werkt goed bij complexe systemen.

3. Hoe werkt het? (Met een Analogie)

Stel je voor dat je een veiligheidscontroleur bent voor een vliegtuig dat door een storm vliegt. Je moet een route plannen die nooit in de onweersbuien terechtkomt.

• De oude methode: Je tekende elke mogelijke route op papier. Omdat er oneindig veel routes zijn, duurde het eeuwen om te controleren of er geen enkele route door de storm ging. Soms gaf je op omdat het papier te vol zat (het computergeheugen liep vol).
• De nieuwe methode (StochasticBarrier.jl): In plaats van elke route te tekenen, bouwt het programma direct een onzichtbaar schild om het vliegtuig.
  • Het gebruikt wiskundige trucs (zoals "Som van Kwadraten" of "Stuksgewijs Constante functies") om te bewijzen: "Zelfs als de wind het hardst waait, kan het vliegtuig dit schild niet doorbreken."
  • Omdat het programma zo efficiënt is, kan het zelfs vliegtuigen controleren die veel complexer zijn dan wat andere programma's aankunnen.

4. Waarom is dit belangrijk?

Vroeger waren deze berekeningen te traag of te onnauwkeurig voor echte toepassingen. Met StochasticBarrier.jl kunnen we nu:

• Veiligere robots bouwen: Van zelfrijdende auto's tot drones die pakketjes bezorgen.
• Complexere situaties aan: Systemen met meer bewegingsvrijheid (meer dimensies) kunnen nu veilig worden getest.
• Sneller innoveren: Omdat de tests zo snel gaan, kunnen ingenieurs hun ontwerpen sneller verbeteren.

Samenvatting

StochasticBarrier.jl is als een super-snel, slimme veiligheidscontroleur die in een handomdraai kan bewijzen dat een robot of auto veilig blijft, zelfs in een chaotische wereld. Het is niet alleen sneller dan alles wat er voorheen was, maar het kan ook veel moeilijkere problemen oplossen, waardoor de weg vrijkomt voor veiligere en slimmere autonome technologie in de toekomst.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het paper "StochasticBarrier.jl: A Toolbox for Stochastic Barrier Function Synthesis" in het Nederlands.

Probleemstelling

Het paper richt zich op de formele verificatie van discrete-tijd stochastische systemen met additief Gaussisch ruis. Het doel is om een ondergrens te garanderen voor de waarschijnlijkheid dat het systeem binnen een veiligheidsset ($X_s$) blijft gedurende een bepaalde tijdsperiode, gegeven een startset ($X_0$).

Traditionele methoden vereisen vaak het doorgeven van systeemonzekerheid, wat rekenkundig zeer intensief is. Stochastische Barrière Functies (SBF's) bieden een oplossing door de tijdsontwikkeling te analyseren via een set statische constraints. Hoewel er theoretische methoden bestaan (zoals Sum-of-Squares en stuksgewijze functies), ontbreekt er tot nu toe een robuust, efficiënt en open-source hulpmiddel dat deze methoden ondersteunt voor een breed scala aan dynamica (lineair, polynoom en niet-lineair). Bestaande tools (zoals PRoTECT en StochasticBarrierFunctions) zijn vaak beperkt tot lage graden, slecht schaalbaar, of gebaseerd op langzamere talen zoals MATLAB of Python.

Methodologie

De auteurs introduceren StochasticBarrier.jl, een open-source toolbox geschreven in Julia. Julia wordt gekozen vanwege zijn combinatie van script-achtige interactiviteit en geoptimaliseerde prestaties van gecompileerde code, evenals ondersteuning voor parametrische typen voor nauwkeurige numerieke berekeningen.

De toolbox implementeert twee hoofdbenaderingen voor het synthetiseren van SBF's:

1. Sum-of-Squares (SOS) Optimalisatie:

   • Geschikt voor lineaire en polynoomsystemen.
   • Het probleem wordt geformuleerd als een convex optimalisatieprobleem (Semi-Definite Programming - SDP).
   • Voor niet-polynoomsystemen wordt gebruik gemaakt van Piecewise Affine (PWA) inclusies. Hierbij wordt de niet-lineaire dynamica benaderd door boven- en ondergrenzen (PWA-bounds) op elk segment van een rooster.
   • De toolbox gebruikt SDP-oplossers (standaard Mosek).

2. Piecewise Constant (PWC) Functies:

   • Deze methode benadert de barrière-functie als een constante waarde per cel in een ruimtelijk rooster.
   • Dit reduceert het probleem tot een Lineair Programma (LP) of een iteratief proces.
   • De toolbox biedt drie verschillende "engines" (oplossingsmethoden) voor PWC-SBF's:
     • Dual LP: Een exacte dualiteit-benadering.
     • CEGIS (Counter-Example Guided Inductive Synthesis): Een iteratieve methode die wisselt tussen het genereren van kandidaat-barrières en tegenvoorbeelden via twee LP's.
     • Gradient Descent (GD): Een methode gebaseerd op projectie-gradienten die schaalbaarheid en geheugenefficiëntie biedt, hoewel de oplossing niet altijd strikt optimaal is volgens de theorema's, maar wel geldig.

De toolbox berekent intern de overgangskern-bounds (transition kernel bounds) die nodig zijn voor de PWC-methoden, gebaseerd op de Gaussische ruisverdeling.

Belangrijkste Bijdragen

• Eerste Julia-gebaseerde toolbox: StochasticBarrier.jl is de eerste open-source implementatie in Julia voor SBF-synthese, wat aanzienlijke snelheidswinst biedt ten opzichte van MATLAB/Python-implementaties.
• Brede ondersteuning voor dynamica: Het ondersteunt lineaire, polynoom en PWA-inclusie dynamica, waardoor het ook niet-lineaire systemen kan verifiëren.
• Meerdere oplossingsmethodes: Naast de gevestigde SOS-methode, implementeert het drie geavanceerde PWC-methoden (Dual LP, CEGIS, GD), wat flexibiliteit biedt tussen nauwkeurigheid en rekentijd.
• Gebruiksgemak en Modulariteit: De toolbox biedt een uniforme interface voor het definiëren van systemen, sets (veilig/gevaarlijk) en het uitvoeren van synthese, met ondersteuning voor het opslaan van data in NetCDF-formaat.

Resultaten

De auteurs hebben de toolbox geëvalueerd aan de hand van meer dan 30 casestudies over acht verschillende systemen (variërend van 1 tot 6 dimensies), waaronder een quadrotor, thermostaat, en pendel.

• Vergelijking met State-of-the-Art:

  • StochasticBarrier.jl is tot 4 ordes van grootte (1000x) sneller dan de dichtstbijzijnde concurrenten (PRoTECT en StochasticBarrierFunctions).
  • Het kan systemen met hogere dimensies en hogere polynoomgraden (tot 30) verwerken, terwijl andere tools vaak vastlopen op geheugenbeperkingen of triviale resultaten leveren.
  • Het levert vaak strakkere ondergrenzen voor de veiligheidskans ($P_s$) op, soms verbeterend van 0 naar 1.0 in gevallen waar andere tools faalden.

• Vergelijking tussen methoden (SOS vs. PWC):

  • De PWC-methoden presteren over het algemeen beter dan SOS-methoden, vooral bij lineaire contractiekaarten en hybride niet-lineaire systemen.
  • De GD-methode is het snelst bij grote roosters.
  • De Dual LP en CEGIS-methoden leveren de strakste veiligheidsbounden, maar vereisen meer rekentijd.
  • Voor het "Unicycle"-model (4 dimensies) leverden PWC-methoden niet-triviale veiligheidsbounden, terwijl de SOS-methode faalde.

Betekenis en Impact

StochasticBarrier.jl vult een kritieke leemte in het veld van formele verificatie voor stochastische systemen. Door de rekenkracht van Julia en de efficiëntie van PWC-methoden te combineren, maakt het de toepassing van SBF's in praktische domeinen zoals robotica en autonome voertuigen veel haalbaarder.

De tool stelt onderzoekers en ingenieurs in staat om veiligheidsverificaties uit te voeren op complexe, hogere-dimensionale systemen die voorheen te zwaar waren voor bestaande software. De open-source aard en de modulaire architectuur bevorderen verdere ontwikkeling en adoptie, met toekomstige uitbreidingen gepland voor niet-Gaussisch en niet-additief ruis.