Stel je voor dat je een robot probeert te leren hoe hij een spelletje moet spelen, zoals het in de lucht houden van een bal, of het rijden van een auto door een storm. Je wilt dat de robot zo goed mogelijk is, maar je wilt er ook voor zorgen dat hij nooit iets gevaarlijks doet, zoals tegen een muur aanrijden of de bal laten vallen. In de wereld van de informatica wordt dit "shield synthesis" genoemd. Denk aan een schild niet als een stuk metaal, maar als een strikte veiligheidscoach die naast de robot staat. Als de robot een zet wil doen die tot een ramp kan leiden, grijpt de coach in en zegt: "Nee, niet die! Probeer deze veilige zet eens." Dit is cruciaal voor complexe systemen waarbij de regels constant veranderen, zoals een stuiterende bal die reageert op de wind of een circuit dat met elektriciteit werkt. De uitdaging is dat deze systemen een oneindig aantal mogelijkheden hebben, wat het ongelooflijk moeilijk maakt om voor elke situatie een perfecte lijst van "veilige" en "onveilige" zetten op te stellen.

Dit is waar het paper "Uppaal Coshy: Automatic Synthesis of Compact Shields for Hybrid Systems" om de hoek komt kijken. De onderzoekers, een team uit Denemarken, hebben een nieuwe tool gebouwd genaamd Uppaal Coshy die fungeert als een super-slimme veiligheidscoach voor deze lastige, gemengde systemen (die ze "hybride systemen" noemen omdat ze een mix zijn van vloeiende, continue veranderingen zoals snelheid en plotselinge, digitale sprongen zoals het aan- of uitzetten van een schakelaar). Hun grote idee is om eerst het hele universum van mogelijke situaties te verdelen in een gigantisch rooster van kleine vakjes. Vervolgens draaien ze duizenden simulaties om te achterhalen welke vakjes veilig zijn en welke gevaarlijk, waardoor ze een enorme kaart van toegestane zetten maken. Echter, deze kaart kan zo groot worden dat het onmogelijk is om deze op te slaan of te gebruiken. Om dit op te lossen, hebben ze een slim algoritme uitgevonden genaamd "Caap" (wat klinkt als een vriendelijke robotnaam), dat deze gigantische, rommelige kaart samenperst tot een net en compacte beslissingsboom—zoals het veranderen van een instructiehandleiding van 100 pagina's in een eenvoudig stroomdiagram. Ze testten dit op een model van een stuiterende bal en ontdekten dat hun methode de veiligheidsregels duizenden keren kon verkleinen zonder de veiligheid te verliezen, waardoor het mogelijk is om deze veiligheidscoaches op echte apparaten te plaatsen.

Het verhaal van de stuiterende bal en de veiligheidscoach

Laten we naar de kern van het verhaal duiken met een personage dat we allemaal kennen: een stuiterende bal. Stel je een bal voor die op en neer stuitert. Een menselijke speler kan er tegenaan slaan om hem in beweging te houden, maar als de speler te hard of op het verkeerde moment slaat, kan de bal de lucht in vliegen of volledig stoppen met stuiteren. Het doel is om de bal eeuwig te laten stuiteren zonder dat hij ooit stopt of wegvliegt.

In de oude dagen was het uitzoeken van precies wanneer je de bal moest raken om het veilig te houden een nachtmerrie. De positie en snelheid van de bal veranderen vloeiend en continu, wat betekent dat er op elk moment een oneindig aantal plekken zijn waar de bal zich kan bevinden. De onderzoekers gebruikten een tool genaamd Uppaal Coshy om dit op te lossen. Ze behandelden de wereld van de bal als een gigantisch schaakbord. Ze verdeelden de ruimte waar de bal zich kon bevinden in miljoenen kleine, rechthoekige vakjes. Voor elk vakje stelde de tool een simpele vraag: "Als de bal in dit vakje zit, welke zetten zijn dan veilig?"

Om dit te beantwoorden, gokte de tool niet zomaar; hij speelde het spel keer op keer. Hij koos een plek binnen een vakje, simuleerde het stuiteren van de bal en keek waar de bal terechtkwam. Als de bal in een "veilig" vakje landde, was die zet goed. Als de bal in een "gevaarlijk" vakje landde (zoals het vakje waar de bal stopt), werd die zet verboden. Omdat het gedrag van de bal een beetje willekeurig kan zijn (misschien is de vloer hobbelig, of is de klap niet perfect), draaide de tool deze simulaties vele malen om er zeker van te zijn. Ze moesten zelfs rekening houden met het feit dat de bal zo hoog zou kunnen stuiteren dat hij het "bord" volledig verlaat. De tool handelde dit af door een speciale "out-of-bounds" zone te creëren en te beslissen of het verlaten van het bord veilig was of niet, op basis van wat er in de simulaties gebeurde.

Het probleem van de gigantische kaart

Hier loopt het verhaal vast. Omdat het rooster zo fijnmazig was (om zeer precies te zijn), eindigde de tool met een enorme lijst met regels. Voor hun voorbeeld van de stuiterende bal had de initiële veiligheidskaart meer dan 1,4 miljoen kleine vakjes, die elk hun eigen regel hadden over wat te doen. Het opslaan van een lijst die zo groot is, is alsof je een bibliotheek in je rugzak probeert te dragen; het is te zwaar voor een echte robot om te gebruiken.

De onderzoekers merkten iets interessants op: veel van de vakjes vlak naast elkaar hadden exact dezelfde regels. Als de bal in een vakje zit waar het veilig is om te slaan, is de bal in het vakje direct ernaast waarschijnlijk ook veilig om te slaan. Dus in plaats van miljoenen kleine regels bij te houden, waarom zouden ze ze niet groeperen?

Ontmoet Caap: De magische compressor

Hier komt hun nieuwe algoritme, Caap, in beeld. Zie Caap als een magische redacteur die naar de gigantische, rommelige kaart kijelt en zegt: "Hé, deze 500 vakjes zeggen allemaal 'Sla de bal'. Laten we ze samenvoegen tot één grote zone." Dit doet het door te zoeken naar patronen en naburige vakjes samen te voegen tot grotere, rechthoekige regio's, zolang de regels hetzelfde blijven.

Het resultaat is een beslissingsboom. Stel je een stroomdiagram voor: "Is de bal hoog? Ja? Gaat hij snel? Nee? Dan sla je erop." Deze boom is veel kleiner en makkelijker te lezen dan de oorspronkelijke kaart van een miljoen vakjes. In hun tests slaagde Caap erin om de veiligheidsregels van de stuiterende bal te verkleinen van 1.430.000 kleine cellen naar slechts 2.972 regio's. Dat is een enorme reductie! Het is alsof je een roman van 1.000 pagina's verandert in een stripboek van 20 pagina's dat exact hetzelfde verhaal vertelt.

Werkt het ook echt?

Het team heeft de kaart niet alleen kleiner gemaakt; ze hebben ook gecontroleerd of het nog steeds werkte. Ze testten hun nieuwe, compacte schild op de stuiterende bal. Ze draaiden 10.000 simulaties waarbij de bal werd gecontroleerd door deze nieuwe, gecomprimeerde veiligheidscoach. Het resultaat? In geen enkele van de 10.000 runs stopte de bal ooit met stuiteren of vloog hij weg. De veiligheid bleef perfect behouden, zelfs hoewel de regels nu klein genoeg waren om op een ansichtkaart te passen.

Ze lieten ook zien dat deze veiligheidscoach gebruikt kan worden om de robot beter te laten worden. Eerst lieten ze de robot leren hoe hij de bal efficiënt kan raken (met zo min mogelijk energie verbruiken), terwijl het schild de wacht hield om te voorkomen dat hij gevaarlijke fouten maakte. De robot leerde de bal in de lucht te houden met zeer weinig slagen, wat bewees dat je zowel veiligheid als efficiëntie tegelijkertijd kunt hebben.

Waarom dit ertoe doet

Dit paper gaat niet alleen over stuiterende ballen. Dezelfde wiskunde is van toepassing op echte zaken zoals elektrische circuits (genaamd boost converters) die de spanning stabiel moeten houden, of watertanks die niet mogen overstromen. De onderzoekers hebben hun tool ook op deze modellen getest, en in elk geval slaagde het Caap-algoritme erin de veiligheidsregels enorm te verkleinen—soms door miljoenen regels terug te brengen naar slechts een dozijn—terwijl het systeem veilig bleef.

De schoonheid van Uppaal Coshy is dat het volledig automatisch is. Je hoeft geen wiskundig genie te zijn om het te gebruiken; je beschrijft gewoon je systeem, en de tool bepaalt de veiligheidsregels, comprimeert ze en geeft je een compact schild dat klaar is voor gebruik. Het is een grote stap voorwaarts voor het zorgen dat de slimme robots en geautomatiseerde systemen van de toekomst niet alleen slim zijn, maar ook veilig, betrouwbaar en klein genoeg om te draaien op de apparaten die we dagelijks gebruiken.