💻 computer science

Event Calculus Meets Hybrid ASP

Dieses Paper führt den Hybrid Event Calculus ein, eine erweiterte Axiomatisierung, die in hybriden ASP-Systemen (clingo-lp, clingo-lp) implementiert ist und die Skalierbarkeits- und Genauigkeitsbeschränkungen traditioneller grundungsbasierter und Top-Down-Ansätze überwindet, indem sie kontinuierliche Veränderungen und dichte Domänen als lineare Constraints darstellt und dadurch eine präzise sowie skalierbare Modellierung sicherheitskritischer Systeme ermöglicht.

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

Veröffentlicht 2026-06-04

📖 4 Min. Lesezeit☕ Kaffeepausen-Lektüre

CC BY 4.0

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

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie möchten eine Geschichte über eine komplexe Maschine schreiben, wie etwa ein selbstfahrendes Auto oder einen intelligenten Thermostaten. Sie möchten beschreiben, wie sie sich im Laufe der Zeit verhält: Was passiert, wenn ein Knopf gedrückt wird, wie sich die Temperatur verändert und wann das System einen Alarm auslösen sollte.

In der Welt der Informatik gibt es eine Sprache namens Event Calculus (Ereigniskalkül), die hervorragend geeignet ist, um solche Geschichten zu schreiben, da sie sich sehr nah an der menschlichen Sprache orientiert. Jedoch stößt die Technik auf eine Wand, wenn Computer versuchen, diese Geschichten zu lesen, sofern die Geschichte kontinuierliche Veränderungen (wie eine langsam sinkende Temperatur) oder riesige Zahlenbereiche (wie eine Zeitmessung in Millisekunden über Jahre hinweg) beinhaltet.

Dieses Paper stellt eine neue Art vor, solche Geschichten zu erzählen, den Hybrid Event Calculus. Er fungiert als eine Art „supergeladener“ Übersetzer für Computer. So funktioniert er, erklärt anhand alltäglicher Analogien:

1. Das Problem: Die „pixelierte“ Karte

Traditionelle Computermethoden zur Überprüfung dieser Geschichten (genannt Discrete Event Calculus) funktionieren wie eine niedrig aufgelöste, pixelierte Karte.

Das Problem: Wenn man einen fallenden Ball verfolgen möchte, kann eine pixelierte Karte den Ball nur an bestimmten Gitternetzpunkten anzeigen (z. B. 1 Meter, 2 Meter, 3 Meter). Sie übersieht das, was zwischen den Gittern passiert.
Die Explosion: Um die Karte genauer zu machen, muss man mehr Pixel hinzufügen. Aber wenn man die Zeit bis auf die Millisekunde für einen ganzen Tag verfolgen möchte, wird die Anzahl der Pixel so gewaltig, dass der Speicher des Computers explodiert und abstürzt. Es ist, als würde man jedes einzelne Sandkorn an einem Strand zählen wollen, um eine ganz bestimmte Muschel zu finden.

2. Die Lösung: Die „intelligente Skizze“ (Hybrid ASP)

Die Autoren haben eine neue Methode entwickelt, die Hybrid Event Calculus genannt wird. Anstatt jeden einzelnen Pixel zu zeichnen, nutzt diese Methode einen „Smart Sketch“-Ansatz (eine intelligente Skizze).

Funktionale Fluenzen (Die variable Farbe): Anstatt zu sagen „Die Temperatur ist 20“ oder „Die Temperatur ist 21“, behandelt der Computer die Temperatur als eine flexible Variable, vergleichbar mit einem Pinselstrich, der überall auf der Leinwand sein kann. Er nutzt mathematische Bedingungen (wie ein Lineal), um den Bereich zu definieren, anstatt jede einzelne Zahl aufzulisten.
Abstrakte Schritte (Die Story-Beats): Anstatt den Computer zu zwingen, die Geschichte in jedem einzelnen Moment (1:00, 1:01, 1:02) durchzugehen, betrachtet der Computer nur die wichtigen Momente (die „Beats“ der Geschichte).
- Beispiel: Wenn ein Ball fallen gelassen wird, interessiert sich der Computer nur für den Moment, in dem er losgelassen wird, und den Moment, in dem er auf dem Boden aufschlägt. Er ignoriert die Millionen winzigen Momente dazwischen und berechnet stattdessen den Pfad mathematisch.

3. Der Motor: Der „mathematische Bibliothekar“

Um dies umzusetzen, haben die Autoren spezielle Computerwerkzeuge (genannt clingcon und clingo-lpx) verwendet, die wie ein Bibliothekar fungieren, der gleichzeitig ein Mathematiker ist.

Der alte Weg: Der Computer würde versuchen, jedes einzelne Buch in der Bibliothek zu lesen (jede Möglichkeit „grounden“), bevor er eine Frage beantwortet.
Der neue Weg: Der Computer fragt den Mathematiker-Bibliothekar: „Wenn der Ball mit Geschwindigkeit X fällt, wo wird er zum Zeitpunkt Y sein?“ Der Bibliothekar löst die Mathematik sofort, ohne die Zeit in jedem einzelnen Sekundentakt nachschlagen zu müssen. Dies ermöglicht es dem System, dichte Domänen (unendliche Möglichkeiten zwischen Zahlen) zu handhaben, ohne überfordert zu werden.

4. Warum es wichtig ist: Genauigkeit ohne Absturz

Das Paper zeigt, dass diese neue Methode zwei Superkräfte besitzt:

Es ist unempfindlich gegenüber der Größe: Ob man die Zeit für 10 Sekunden oder 10 Jahre verfolgt, die Arbeitslast des Computers bleibt gleich, da er nur die „Story-Beats“ zählt, nicht die Sekunden.
Es handhabt das „Dazwischen“: Da es mathematische Bedingungen (speziell rationale Zahlen) nutzt, kann es kontinuierliche Veränderungen präzise modellieren. Es kann genau bestimmen, wann ein fallendes Objekt den Boden berührt, selbst wenn dies zu einem Zeitpunkt geschieht, der keine ganze Zahl ist (wie 10,5 Sekunden), was die alten „pixelierten“ Methoden oft übersehen oder falsch darstellen würden.

Zusammenfassung

Stellen Sie sich die alte Methode wie das Anschauen eines Films über ein Daumenkino vor, bei dem man jedes einzelne Bild manuell zeichnen muss. Wenn der Film lang ist, geht das Papier aus.

Der neue Hybrid Event Calculus ist wie das Anschauen des Films auf einem hochauflösenden Bildschirm. Man hält nur bei den Schlüsselszenen (den Ereignissen) an, und der Computer füllt die fließenden Bewegungen dazwischen mithilfe von Mathematik aus. Dies ermöglicht es, komplexe, reale Systeme (wie sicherheitskritische Maschinen) präzise zu analysieren, ohne dass der Computer durch die schiere Menge an Daten überlastet wird.

Technisches Resümee: Event Calculus trifft Hybrid ASP

Problemstellung

Das Event Calculus (EC) ist ein logisches Formalismusmodell, das aufgrund seiner semantischen Nähe zur natürlichen Sprache und seiner Fähigkeit, sowohl diskrete als auch kontinuierliche Änderungen zu modellieren, besonders gut für die Spezifikation sicherheitskritischer cyber-physischer Systeme (CPS) geeignet ist. Die Anwendung von EC auf reale CPS-Spezifikationen stößt jedoch auf erhebliche Herausforderungen beim Umgang mit kontinuierlichen Änderungen und großen oder dichten Wertebereichen für Zeit und Systemeigenschaften (Fluents).

Aktuelle State-of-the-Art-Reasoning-Tools auf Basis von Answer Set Programming (ASP) haben Schwierigkeiten mit diesen Anforderungen:

Grundungsbasierte Solver (z. B. clingo): Diese erfordern eine Diskretisierung dichter Domänen. Während eine Erhöhung der Präzision (z. B. von Sekunden auf Millisekunden) Repräsentationsungenauigkeiten mildern kann, führt dies zu einer kombinatorischen Explosion in der Größe des gegroundeten Programms, was dazu führt, dass Solver an Speicherplatz oder Zeitmangel scheitern.
Grundungsfreie Solver (z. B. s(CASP)): Während diese die Diskretisierung und die Grundungs-Explosion vermeiden, verlassen sie sich auf eine Top-Down-Ausführung, die unter Problemen der Nicht-Terminierung leiden kann und nicht die optimierte Performance moderner grundungsbasierter ASP-Solver erreichen.

Folglich besteht eine Lücke bei Werkzeugen, die in der Lage sind, kontinuierliche Änderungen in EC genau zu modellieren, ohne die Skalierbarkeit oder die Garantien für die Terminierung zu opfern.

Methodik: Hybrid Event Calculus (HEC)

Die Autoren führen das Hybrid EC ein, eine erweiterte Axiomatisierung des Diskreten Event Calculus (DEC), die darauf ausgelegt ist, diese Einschränkungen zu adressieren. Der Ansatz nutzt Hybrid ASP, ein Paradigma, das Standard-ASP mit linearen Constraints über ganze und rationale Zahlen kombiniert.

Die zentralen technischen Innovationen von Hybrid EC umfassen:

1. Funktionale Fluents

Im Gegensatz zum Standard-DEC, das relationale Fluents verwendet (wahr/falsch zu einem Zeitpunkt), führt Hybrid EC funktionale Fluents ein. Die Werte dieser Fluents werden als symbolische Terme (z. B. (F, S)) dargestellt, deren Werte durch lineare Constraints bestimmt werden, anstatt durch explizite Grundung. Dies ermöglicht es Fluents, dichte Werte zu halten, ohne dass für jeden möglichen Wert ein Grund-Atom erforderlich ist.

2. Hybride Zeitrepräsentation

DEC operiert auf ganzzahligen Zeitschritten ( $T, T+1$ ). Hybrid EC ersetzt dies durch abstrakte Schrittindizes ( $S, S+1$ ), welche die Sequenz der Systementwicklung repräsentieren.

Diskrete Schritte: Nur die Sequenz der Ereignisse wird als diskrete Schritte gegroundet.
Dichte Zeit: Die tatsächliche Zeit, die mit jedem Schritt assoziiert ist, wird über Theorie-Atome (z. B. (time, S)) durch einen Constraint-Solver gehandhabt.
Mapping: Beobachtungen von Ereignissen zu spezifischen Zeitpunkten $T$ werden via Constraints auf abstrakte Schritte $S$ abgebildet, wodurch sichergestellt wird, dass die Größe der Grundung von der Anzahl der Ereignisse abhängt und nicht von der Größe des Zeitbereichs.

3. Axiomatisierung (HEC)

Die Autoren erweitern die DEC-Axiome (speziell die von Lee und Palla, 2012), um funktionale Fluents und die hybride Zeitrepräsentation zu berücksichtigen. Wesentliche Anpassungen sind:

Inertia und Ereigniseffekte: Regeln werden modifiziert, um Werte für funktionale Fluents mittels linearer Ausdrücke zuzuweisen (z. B. &sum{(F,S)} = (F,S+1)), sofern ein Ereignis keinen neuen Wert initiiert oder den Fluent von der Inertia löst.
Kontinuierliche Änderung: Trajektorien werden neu definiert, um Fluent-Werte basierend auf dem tatsächlichen Zeitunterschied zwischen den Schritten zu berechnen ( $R \times ((time, S_1+S_2) - (time, S_1))$ ), anstatt auf diskreten Schrittzählungen zu basieren, was eine genaue Modellierung monotoner linearer kontinuierlicher Änderung ermöglicht.
Ausgelöste Ereignisse: Um Ereignisse zu handhaben, die durch kontinuierliche Änderungen ausgelöst werden (z. B. das Aufprallen auf den Boden), verwendet das System no_jump-Constraints. Diese verhindern, dass Schritte kritische Werte (wie die Höhe Null) während monotoner Änderungen "überspringen", wodurch sichergestellt wird, dass die Trigger-Bedingung exakt erfüllt wird.

4. Implementierung und Lösung

Die Implementierung nutzt zwei Hybrid-ASP-Solver:

clingcon: Unterstützt lineare Constraints über ganze Zahlen.
clingo-lpx: Unterstützt lineare Constraints über rationale Zahlen.

Das System verwendet einen inkrementellen Lösungsansatz. Es beginnt mit einer minimalen Anzahl von Schritten und erhöht iterativ die Schrittanzahl, bis ein Modell gefunden wird. Dies vermeidet die Notwendigkeit für den Nutzer, die korrekte Anzahl an Schritten zu erraten. Der Ansatz stellt sicher, dass eine Terminierung eintritt, sobald eine Lösung innerhalb der definierten Schrittgrenzen existiert.

Zentrale Beiträge

Hybrid EC Axiomatisierung: Eine formale Erweiterung von DEC, die funktionale Fluents und die abstrakte schrittbasierte Zeit-Mapping integriert, was die Repräsentation dichter Domänen ohne Grundungs-Explosion ermöglicht.
Genaue kontinuierliche Modellierung: Durch die Nutzung von clingo-lpx und rationalen Zahlen ermöglicht der Ansatz präzises Reasoning über kontinuierliche Änderungen (dichte Domänen), eine Fähigkeit, die in Standard-ASP-basierten EC-Implementierungen ohne Diskretisierungsartefakte bisher nicht verfügbar war.
Skalierbarkeit: Die Größe der Grundung ist von der Größe der Zeit- und Wertebereiche entkoppelt und hängt stattdessen von der Anzahl der Ereignisse ab. Dies erlaubt es dem System, große Domänen effizient zu handhaben.
Duale Implementierung: Die Autoren stellen Implementierungen unter Verwendung sowohl von Integer- (clingcon) als auch Rational-Solvern (clingo-lpx) bereit, was die Flexibilität des Ansatzes demonstriert.

Experimentelle Ergebnisse

Die Autoren evaluierten den Ansatz anhand von über 30 Benchmark-Problemen aus der Literatur (z. B. Counter, Falling Object, Stolen Car, Hot Air Balloon).

Expressivität: Die Hybrid-EC-Implementierungen (clingcon und clingo-lpx) lösten erfolgreich alle Probleme, die auch von der Standard-clingo (DEC) Implementierung bearbeitet wurden. Darüber hinaus löste clingo-lpx erfolgreich Probleme, die kontinuierliche Änderung (dichte Domänen) erforderten, was clingo und clingcon nicht präzise handhaben konnten.
Skalierbarkeit (Domänengröße): Experimente, welche die Größe der Zeit- und Wertebereiche variierten, zeigten, dass die Ausführungszeit von clingo exponentiell anstieg (was zu Timeouts führte), während sie mit wachsender Domänengröße zunahm. Im Gegensatz dazu behielten clingcon und clingo-lpx stabile Ausführungszeiten bei, die unbeeinflusst von der Domänengröße waren.
Skalierbarkeit (Ereignisanzahl): Die Performance skalierte linear mit der Anzahl der Ereignisse, was bestätigt, dass der Ansatz durch die Anzahl der Ereignisse und nicht durch die Magnitude der Domäne getrieben wird.
Rational vs. Integer: Die Verwendung von rationalen Zahlen in clingo-lpx beeinträchtigte die Skalierbarkeit im Vergleich zum Integer-Reasoning nicht negativ, bot jedoch die notwendige Präzision für die kontinuierliche Modellierung.

Bedeutung und Ansprüche

Das Paper behauptet, dass Hybrid EC erfolgreich die Lücke zwischen der semantischen Reichhaltigkeit des Event Calculus und den computationalen Limitationen aktueller ASP-Solver schließt.

Genauigkeit: Es eliminiert Ungenauigkeiten, die durch Diskretisierung entstehen, und ermöglicht so eine getreue Modellierung kontinuierlicher physikalischer Prozesse.
Effizienz: Es vermeidet die Grundungs-Explosion, die mit großen oder dichten Domänen einhergeht, und macht die rigorose Verifizierung komplexer CPS-Spezifikationen machbar.
Terminierung: Im Gegensatz zu grundungsfreien, abfragegesteuerten Ansätzen gewährleistet der Hybrid-ASP-Ansatz die Terminierung für lösbare Instanzen.

Die Autoren merken an, dass die aktuelle Implementierung zwar monotone lineare Änderungen handhabt, das Reasoning über dichte Zeit jedoch Herausforderungen wie das Zeno-Verhalten mit sich bringt. Sie räumen ein, dass die Adressierung dieser spezifischen Phänomene im Kontext von HEC der zukünftigen Arbeit vorbehalten bleibt, stellen jedoch Encodings für verwandte Probleme bereit. Die Arbeit etabliert eine Grundlage für die Nutzung von Hybrid ASP zur Modellierung sicherheitskritischer Systeme mit kontinuierlicher Dynamik.