💻 computer science

Event Calculus Meets Hybrid ASP

Dit artikel introduceert Hybrid Event Calculus, een uitgebreide axiomatisering geïmplementeerd in hybride ASP-systemen (clingcon en clingo-lpx) die de schaalbaarheids- en nauwkeurigheidsbeperkingen van traditionele grondingsgebaseerde en top-down benaderingen overwint door continue veranderingen en dichte domeinen te representeren als lineaire restricties, waardoor nauwkeurige en schaalbare modellering van veiligheidskritische systemen mogelijk wordt.

Oorspronkelijke auteurs: Ondřej Vašíček, Joaquín Arias, Jan Fiedor, Gopal Gupta, Bohuslav Křena, Jakub Němec, Javier Romero, Tomáš Vojnar

Gepubliceerd 2026-06-04

📖 4 min leestijd☕ Koffiepauze-leesvoer

CC BY 4.0

Oorspronkelijke auteurs: Ondřej Vašíček, Joaquín Arias, Jan Fiedor, Gopal Gupta, Bohuslav Křena, Jakub Němec, Javier Romero, Tomáš Vojnar

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een verhaal wilt schrijven over een complexe machine, zoals een zelfrijdende auto of een slimme thermostaat. Je wilt beschrijven hoe het gedrag verandert over de tijd: wat er gebeurt als er op een knop wordt gedrukt, hoe de temperatuur verandert en wanneer het systeem een alarm moet laten afgaan.

In de wereld van de informatica is er een taal genaamd Event Calculus die erg goed is in het schrijven van dit soort verhalen, omdat het heel dicht bij de manier waarop mensen spreken staat. Echter, wanneer computers proberen deze verhalen te lezen, lopen ze tegen een muur aan als het verhaal gaat over continue verandering (zoals een temperatuur die langzaam daalt) of enorme bereiken van getallen (zoals tijd gemeten in milliseconden over jaren heen).

Dit artikel introduceert een nieuwe manier om deze verhalen te vertellen, genaamd Hybrid Event Calculus, die werkt als een "supergeladen" vertaler voor computers. Hier is hoe het werkt, met behulp van enkele alledaagse analogieën:

1. Het Probleem: De "Gepixelde" Kaart

Traditionele computermethoden voor het controleren van deze verhalen (Discrete Event Calculus) werken als een laag-resolutie, gepixelde kaart.

Het Probleem: Als je een vallende bal wilt volgen, kan een gepixelde kaart de bal alleen tonen op specifieke rasterpunten (bijv. 1 meter, 2 meter, 3 meter). Het mist wat er tussen de rasters gebeurt.
De Explosie: Om de kaart nauwkeuriger te maken, moet je meer pixels toevoegen. Maar als je de tijd wilt volgen tot op de milliseconde over een hele dag, wordt het aantal pixels zo enorm dat het geheugen van de computer explodeert en vastloopt. Het is alsof je elk individueel zandkorreltje op een strand probeert te tellen om één specifieke schelp te vinden.

2. De Oplossing: De "Slimme Schets" (Hybrid ASP)

De auteurs hebben een nieuwe methode ontwikkeld die Hybrid Event Calculus wordt genoemd. In plaats van elke afzonderlijke pixel te tekenen, gebruikt deze methode een "Slimme Schets"-aanpak.

Functionele Fluents (De Variabele Verf): In plaats van te zeggen "De temperatuur is 20" of "De temperatuur is 21", behandelt de computer de temperatuur als een flexibele variabele, zoals een penseel die overal op het canvas kan zijn. Het gebruikt wiskundige beperkingen (zoals een liniaal) om het bereik te definiëren, in plaats van elk getal afzonderlijk op te sommen.
Abstracte Stappen (De Verhaalritmes): In plaats van de computer te dwingen om bij elke seconde te kijken (1:00, 1:01, 1:02), kijkt de computer alleen naar de belangrijke momenten (de "beats" van het verhaal).
- Voorbeeld: Als een bal wordt losgelaten, geeft de computer alleen om het moment dat de bal wordt losgelaten en het moment dat hij de grond raakt. Het negeert de miljoenen kleine momenten daartussenin door het pad wiskundig te berekenen in plaats van ze één voor één op te sommen.

3. De Motor: De "Wiskundige Bibliothecaris"

Om dit werkend te krijgen, hebben de auteurs speciale computertools gebruikt (genaamd clingcon en clingo-lpx) die fungeren als een biblicaris die ook een wiskundige is.

De Oude Manier: De computer zou proberen elk boek in de bibliotheek te lezen (elke mogelijkheid "grounden") voordat hij een vraag beantwoordt.
De Nieuwe Manier: De computer vraat aan de wiskundige biblicaris: "Als de bal valt met snelheid X, waar is hij dan op tijdstip Y?" De biblicaris lost de wiskunde direct op zonder dat hij elk enkelvoudig seconde in een boek hoeft op te zoeken. Dit stelt het systeem in staat om dense domeinen (oneindige mogelijkheden tussen getallen) te verwerken zonder overweldigd te raken.

4. Waarom het ertoe doet: Nauwkeurigheid zonder de Crash

Het artikel laat zien dat deze nieuwe methode twee superkrachten heeft:

Het geeft niet om de grootte: Of je nu de tijd volgt voor 10 seconden of 10 jaar, de werklast van de computer blijft hetzelfde omdat het alleen de "verhaalritmes" telt, niet de seconden.
Het handelt het "tussenin" af: Omdat het wiskundige beperkingen gebruikt (specifiek rationale getallen), kan het continue veranderingen nauwkeurig modelleren. Het kan je precies vertellen wanneer een vallend object de grond raakt, zelfs als dat op een tijdstip gebeurt dat geen heel getal is (zoals 10,5 seconden), wat de oude "gepixelde" methoden vaak missen of foutief weergeven.

Samenvatting

Denk aan de oude methode als het kijken naar een film via een flipboekje waarbij je elke frame handmatig moet tekenen. Als de film lang is, raak je aan papier uit.

De nieuwe Hybrid Event Calculus is als het kijken naar de film op een high-definition scherm. Je pauzeert alleen bij de sleutelscènes (de gebeurtenissen), en de computer vult de vloeiende beweging tussen deze scènes in met behulp van wiskunde. Dit stelt je in staat om complexe, echte systemen (zoals veiligheidskritische machines) nauwkeurig te analyseren, zonder dat de computer traag wordt door de enorme hoeveelheid data.

Technische Samenvatting: Event Calculus ontmoet Hybride ASP

Probleemstelling

Event Calculus (EC) is een logisch formalisme dat zeer geschikt is voor het specificeren van veiligheidskritische cyber-fysieke systemen (CPS), vanwege de semantische nabijheid tot natuurlijke taal en het vermogen om zowel discrete als continue veranderingen te modelleren. Het toepassen van EC op real-world CPS-specificaties staat echter voor aanzienlijke uitdagingen wanneer men te maken krijgt met continue veranderingen en grote of dichte domeinen van waarden voor tijd en systeemeigenschappen (fluents).

De huidige state-of-the-art redeneertools gebaseerd op Answer Set Programming (ASP) worstelen met deze vereisten:

Grounding-gebaseerde solvers (bijv. clingo): Deze vereisen de discretisering van dichte domeinen. Hoewel het verhogen van de precisie (bijv. van seconden naar milliseconden) de representatiefouten kan beperken, leidt dit tot een combinatorische explosie in de grootte van het gegrounde programma, waardoor solvers tekort aan geheugen of tijd komen te staan.
Grounding-vrije solvers (bijv. s(CASP)): Hoewel deze de discretisering vermijden en de grounding-explosie voorkomen, vertrouwen ze op top-down executie, wat kan leiden tot problemen met niet-terminatie en het gebrek aan de geoptimaliseerde prestaties van moderne grounding-gebaseerde solvers.

Als gevolg hiervan is er een gat in de tools die in staat zijn om nauwkeurig over continue verandering te redeneren binnen EC zonder op te offeren aan schaalbaarheid of garanties op terminatie.

Methodologie: Hybride Event Calculus (HEC)

De auteurs introduceren Hybride EC, een uitgebreide axiomatisering van Discrete Event Calculus (DEC), ontworpen om deze beperkingen aan te pakken. De aanpak maakt gebruik van Hybride ASP, een paradigma dat standaard ASP combineert met lineaire restricties over gehele getallen en rationale getallen.

De kern van de technische innovaties van Hybride EC omvat:

1. Functionele Fluents

In tegenstelling tot standaard DEC, dat relationele fluents gebruikt (waar/onwaar op een tijdstip), introduceert Hybride EC functionele fluents. De waarden van deze fluents worden gerepresenteerd als symbolische termen (bijv. (F, S)) waarvan de waarden worden bepaald door lineaire restricties in plaats van expliciete grounding. Dit stelt fluents in staat om dichte waarden te bevatten zonder dat er een ground-atoom nodig is voor elke mogelijke waarde.

2. Hybride Representatie van Tijd

DEC werkt met discrete tijdstappen ( $T, T+1$ ). Hybride EC vervangt dit door abstracte stap-indices ( $S, S+1$ ) die de sequentie van de systeemevolutie vertegenwoordigen.

Discrete Stappen: Alleen de sequentie van gebeurtenissen wordt geground als discrete stappen.
Dense Tijd: De werkelijke tijd die aan elke stap is gekoppeld, wordt afgehandeld door een constraint solver via theory atoms (bijv. (time, S)).
Mapping: Observaties van gebeurtenissen op specifieke tijdstippen $T$ worden via restricties gemapt naar abstracte stappen $S$ , waardoor de grootte van de grounding afhankelijk is van het aantal gebeurtenissen, niet van de grootte van het tijdsdomein.

3. Axiomatisering (HEC)

De auteurs breiden de DEC-axioma's uit (specifiek die van Lee en Palla, 2012) om rekening te houden met functionele fluents en de hybride tijdsrepresentatie. Belangrijke aanpassingen zijn:

Inertia en Event Effects: Regels worden aangepast om waarden aan functionele fluents toe te wijzen met behulp van lineaire expressies (bijv. &sum{(F,S)} = (F,S+1)), tenzij een gebeurtenis een nieuwe waarde initieert of de fluent bevrijdt van inertia.
Continue Verandering: Trajecten worden hergedefinieerd om de waarden van fluents te berekenen op basis van het werkelijke tijdsverschil tussen stappen ( $R \times ((time, S_1+S_2) - (time, S_1))$ ), in plaats van discrete stap-aantallen, wat nauwkeurige modellering van monotone lineaire continue verandering mogelijk maakt.
Getriggerde Gebeurtenissen: Om gebeurtenissen te behandelen die getriggerd worden door continue verandering (bijv. het raken van de grond), gebruikt het systeem no_jump restricties. Deze voorkomen dat stappen cruciale waarden (zoals nul hoogte) "overslaan" tijdens monotone veranderingen, waardoor wordt gewaarborgd dat de triggerconditie exact wordt voldaan.

4. Implementatie en Oplossen

De implementatie maakt gebruik van twee Hybride ASP solvers:

clingcon: Ondersteunt lineaire restricties over gehele getallen.
clingo-lpx: Ondersteunt lineaire restricties over rationale getallen.

Het systeem maakt gebruik van een incrementele oplossingsmethode. Het begint met een minimaal aantal stappen en verhoogt iteratief het aantal stappen totdat een model wordt gevonden. Dit voorkomt dat de gebruiker het juiste aantal stappen moet raden. De aanpak garandeert terminatie wanneer een oplossing bestaat binnen de gedefinieerde stapgrenzen.

Belangrijkste Bijdragen

Hybride EC Axiomatisering: Een formele uitbreiding van DEC die functionele fluents en abstracte stap-gebaseerde tijdsmapping integreert, waardoor de representatie van dichte domeinen mogelijk is zonder grounding-explosie.
Nauwkeurige Continue Modellering: Door gebruik te maken van clingo-lpx en rationale getallen, maakt de aanpak nauwkeurige redenering over continue verandering (dense domeinen) mogelijk, een capaciteit die voorheen onbeschikbaar was in standaard ASP-gebaseerde EC-implementaties zonder discretiseringsartefacten.
Schaalbaarheid: De grootte van de grounding is ontkoppeld van de grootte van de tijd- en waardedomijnen en hangt in plaats daarvan af van het aantal gebeurtenissen. Dit stelt het systeem in staat om grote domeinen efficiënt te verwerken.
Duale Implementatie: De auteurs bieden implementaties aan met zowel integer (clingcon) als rationale (clingo-lpx) solvers, wat de flexibiliteit van de aanpak demonstreert.

Experimentele Resultaten

De auteurs evalueerden de aanpak op meer dan 30 benchmarkproblemen uit de literatuur (bijv. teller, vallend object, gestolen auto, heteluchtballon).

Expressiviteit: De Hybride EC-implementaties (clingcon en clingo-lpx) losten succesvol alle problemen op die ook door de standaard clingo (DEC) implementatie werden afgehandeld. Bovendien loste clingo-lpx succesvol problemen op die continue verandering (dense domeinen) vereisten, wat clingo en clingcon niet nauwkeurig konden afhandelen.
Schaalbaarheid (Domeingrootte): Experimenten waarbij de grootte van de tijd- en waardedomijnen varieerden, toonden aan dat de executietijd van clingo exponentieel toenam (wat leidde tot timeouts) naarmate de domeingrootte groeide. In contrast hiermee behielden clingcon en clingo-lpx stabiele executietijden, ongeacht de domeingrootte.
Schaalbaarheid (Aantal Gebeurtenissen): De prestaties schaalden lineair met het aantal gebeurtenissen, wat bevestigt dat de aanpak wordt gedreven door het aantal gebeurtenissen in plaats van de magnitude van het domein.
Rationaal vs. Integer: Het gebruik van rationale getallen in clingo-lpx had geen negatieve impact op de schaalbaarheid vergeleken met integer-redenering, terwijl het de noodzakelijke precisie voor continue modellering bood.

Betekenis en Claims

Het artikel claimt dat Hybride EC erin slaagt de kloof te overbruggen tussen de semantische rijkdom van Event Calculus en de computationele beperkingen van huidige ASP-solvers.

Nauwkeurigheid: Het elimineert onnauwkeurigheden veroorzaakt door discretisering, waardoor een getrouwe modellering van continue fysieke processen mogelijk is.
Efficiëntie: Het vermijdt de grounding-explosie geassocieerd met grote of dichte domeinen, waardoor rigoureuze verificatie van complexe CPS-specificaties haalbaar wordt.
Terminatie: In tegen tegenstelling tot grounding-vrije query-gestuurde benaderingen, garandeert de Hybride ASP-aanpak terminatie voor oplosbare instanties.

De auteurs merken op dat hoewel de huidige implementatie monotone lineaire veranderingen afhandelt, het redeneren over dense tijd uitdagingen met zich meebrengt zoals Zeno-gedrag. Zij erkennen dat het adresseren van deze specifieke fenomenen in de context van HEC een onderwerp is voor toekomstig onderzoek, hoewel zij encodings voor gerelateerde problemen bieden. Dit werk legt een fundament voor het gebruik van Hybride ASP om te redeneren over veiligheidskritische systemen met continue dynamica.