💻 computer science

Monitoring Data-aware Temporal Properties (Extended Version)

Dieser Beitrag stellt ein neuartiges, formal verifiziertes Framework für die anticipative Überwachung von Linear-Time-Eigenschaften, die mit SMT-Theorien angereichert sind (LTLfMT), vor, indem automaten-theoretische Methoden mit automatischem Schließen kombiniert werden, wodurch entscheidbare Fragmente identifiziert werden, die für datenbewusste Systeme relevant sind, und die Machbarkeit durch eine Prototyp-Implementierung demonstriert wird.

Ursprüngliche Autoren: Alessandro Gianola, Marco Montali, Sarah Winkler

Veröffentlicht 2026-05-15

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Alessandro Gianola, Marco Montali, Sarah Winkler

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 beobachten eine komplexe Black-Box-Maschine (wie einen hochentwickelten KI-Agenten), die eine Aufgabe erfüllt. Sie können nicht in die Maschine hineinsehen, um ihre Baupläne oder ihren Code zu überprüfen, aber Sie können den Strom der Aktionen beobachten, die sie ausführt. Ihre Aufgabe ist es, als Wachhund zu fungieren, um sicherzustellen, dass die Maschine die Regeln einhält.

Dieser Artikel stellt eine neue, superintelligente Art von Wachhund für KI-Systeme vor, die sich mit Daten (wie Zahlen, Listen oder Datenbankdatensätzen) über die Zeit hinweg befassen.

Hier ist die Aufschlüsselung ihrer Arbeit mit einfachen Analogien:

1. Das Problem: Die „Glaskugel"-Herausforderung

Die meisten traditionellen Wachhunde sind wie Überwachungskameras, die nur auf das schauen, was bereits passiert ist. Wenn eine Maschine eine Regel bricht, sieht die Kamera es und löst den Alarm aus.

Die Autoren argumentieren jedoch, dass Sie in komplexen KI-Systemen eine Glaskugel benötigen. Sie müssen nicht nur wissen, ob die Maschine eine Regel gebrochen hat, sondern ob sie verurteilt ist, eine Regel zu brechen, egal was sie als Nächstes tut.

Die Analogie: Stellen Sie sich einen Wanderer vor, der am Rand einer Klippe entlanggeht.
- Alter Wachhund: „Sie sind noch nicht heruntergefallen, also sind Sie sicher." (Er prüft nur die Vergangenheit).
- Neuer „Antizipierender" Wachhund: „Obwohl Sie noch nicht heruntergefallen sind, führt der Weg vor Ihnen in eine Sackgasse. Egal, in welche Richtung Sie sich wenden, Sie werden herunterfallen. Ich erkläre Sie jetzt, bevor Sie tatsächlich den Schritt machen, für ‚dauerhaft verletzt'."

Dies wird als Antizipatorisches Monitoring bezeichnet. Es betrachtet die Geschichte und alle möglichen Zukünfte, um sofort ein Urteil zu fällen.

2. Die Komplexität: Daten + Zeit

Die Maschine bewegt sich nicht nur; sie trifft Entscheidungen basierend auf Daten.

Das Beispiel: Denken Sie an einen Konzertticket-Bot. Jede Sekunde sieht er ein neues Ticketangebot. Er muss entscheiden: „Soll ich mein aktuell markiertes Ticket behalten oder auf dieses neue wechseln?"
Die Regel: „Wählen Sie immer das günstigste Ticket für das spezifische Konzert, das ich möchte."
Die Herausforderung: Der Bot muss bei jedem Schritt Preise vergleichen (Mathematik) und Konzertnamen prüfen (Daten). Wenn der Bot ein Ticket für 100 $ auswählt, aber später ein Ticket für 50 $ für dasselbe Konzert erscheint, muss der Bot wechseln. Tut er es nicht, ist er defekt.

Die Autoren schufen eine Sprache (eine Reihe von Regeln), um diese komplexen, datenintensiven Regeln zu beschreiben. Sie nennen sie LTLMTf.

3. Die Lösung: Die „Rückwärtskarte"

Die Autoren stellten sich einem riesigen Problem: Die Zukunft für eine Maschine mit unendlichen Möglichkeiten vorherzusagen, ist normalerweise unmöglich (mathematisch „unentscheidbar"). Es ist wie der Versuch, jeden möglichen Zug in einem Schachspiel vorherzusagen, das nie endet.

Um dies zu lösen, bauten sie eine Rückwärtskarte (ein technisches Werkzeug namens Coreachability Graph).

Die Analogie: Statt zu versuchen, jeden Weg vorherzusagen, den der Wanderer vorwärts nehmen könnte, stellen Sie sich vor, Sie beginnen am Ziel (dem Ziel) und arbeiten rückwärts.
1. Sie markieren die Stellen, an denen der Wanderer die Wanderung erfolgreich abschließt.
2. Sie fragen: „Welche Bedingungen müssen jetzt gerade wahr sein, um diese guten Stellen zu erreichen?"
3. Sie gehen weiter rückwärts und erstellen eine Karte von „Sicheren Zonen" und „Gefahrenzonen".

Indem sie diese Karte rückwärts aufbauen, können sie die aktuelle Position des Wanderers betrachten und sofort wissen: „Gibt es irgendeinen Weg vorwärts, der zum Erfolg führt?"

Wenn Ja: Das System ist derzeit sicher, könnte aber später versagen (Aktuelle Zufriedenstellung).
Wenn Nein: Das System ist derzeit sicher, wird aber egal was passiert, versagen (Dauerhafte Zufriedenstellung – warten Sie, das bedeutet eigentlich, es ist dauerhaft sicher? Nein, lassen Sie uns die Analogie basierend auf der Logik des Artikels korrigieren).

Korrektur der Urteile:
Der Artikel definiert vier Zustände für den Wachhund:

Aktuelle Zufriedenstellung (CS): Es geht Ihnen jetzt gut, aber Sie könnten sich später versauen.
Dauerhafte Zufriedenstellung (PS): Es geht Ihnen jetzt gut, und Sie sind garantiert, gut zu bleiben, egal was als Nächstes passiert.
Aktuelle Verletzung (CV): Sie haben sich versaut, aber Sie könnten es später reparieren.
Dauerhafte Verletzung (PV): Sie haben sich versaut, und es gibt keinen Weg, es zu reparieren. Das Spiel ist aus.

Der „antizipierende" Teil ist die Fähigkeit, PV (Dauerhafte Verletzung) sofort zu erkennen, anstatt darauf zu warten, dass das System abstürzt.

4. Der magische Trick: „Modellvollendung"

Wie haben sie diese Rückwärtskarte möglich gemacht, ohne sich in unendlicher Mathematik zu verirren? Sie verwendeten einen mathematischen Trick namens Modellvollendung.

Die Analogie: Stellen Sie sich vor, Sie versuchen, ein Labyrinth zu lösen, aber das Labyrinth wächst ständig neue Wände.
- Die Autoren fanden einen Weg, das Labyrinth zu „glätten". Sie bewiesen, dass für bestimmte Arten von Regeln (insbesondere solche, die Datenbanken und Arithmetik wie Addition/Subtraktion beinhalten), man das wachsende Labyrinth so behandeln kann, als wäre es eine feste, handhabbare Größe.
- Sie identifizierten spezifische „sichere Zonen" von Regeln (wie DB-LTLf-MC), in denen sich die Mathematik gut verhält. In diesen Zonen ist die „Rückwärtskarte" garantiert endlich und lösbar.

5. Das Ergebnis: Ein funktionierender Prototyp

Sie haben nicht nur Theorie geschrieben; sie bauten ein Prototyp-Tool namens MONTHE.

Sie testeten es am Beispiel des Konzerttickets.
Das Tool beobachtete erfolgreich den „Ticket-Bot" und konnte sofort sagen: „Hey, dieser Bot hat ein Ticket für 100 $ gewählt, aber das Konzert kostet 50 $. Es ist dauerhaft verletzt, weil es das 50 $-Ticket nie finden wird, wenn es die Daten weiterhin ignoriert."

Zusammenfassung

Dieser Artikel handelt vom Bau eines superwachsamten Sicherheitswächters für KI-Systeme.

Alter Wächter: „Sie haben die Regel noch nicht gebrochen."
Neuer Wächter: „Ich sehe die Zukunft. Sie brechen derzeit die Regel, und es gibt keinen Weg, dies zu reparieren. Ich stufe Sie sofort als ‚dauerhaft verletzt' ein."

Sie erreichten dies, indem sie Zeitreise-Logik (Betrachtung von Vergangenheit und Zukunft) mit Datenbankmathematik kombinierten, aber nur für bestimmte Arten von Regeln, bei denen die Mathematik nicht zu verrückt wird, um sie zu lösen. Sie bewiesen, dass es funktioniert, und bauten ein Tool, um es zu tun.

Technische Zusammenfassung: Überwachung datenbewusster temporaler Eigenschaften

Problemdefinition

Der Beitrag adressiert die Herausforderung der antizipativen Laufzeitverifikation für komplexe, dynamische KI-Systeme, bei denen interne Spezifikationen nicht zugänglich sind (Black-Box-Systeme). Traditionelle Verifikationsmethoden zur Entwurfszeit, wie das Modellprüfen, sind in diesen Szenarien oft nicht anwendbar. Zwar bietet die Laufzeitverifikation (RV) eine Lösung durch die Überwachung von Ausführungsspuren, doch bestehende Ansätze stoßen auf zwei primäre Einschränkungen:

Propositionaler Charakter: Die Standard-Linear-Time-Temporal-Logik über endlichen Spuren ( $LTL_f$ ) kann keine Eigenschaften ausdrücken, die strukturierte Daten betreffen (z. B. Arithmetik, Mengen, uninterpretierte Funktionen), welche in modernen KI-Agenten und Geschäftsprozessen allgegenwärtig sind.
Fehlende Antizipation: Die meisten Überwacher bewerten lediglich den bisher gesehenen Spurpräfix. Sie versagen darin, Verletzungen zu erkennen, die unvermeidbar sind, unabhängig davon, wie die Spur weiterverläuft (z. B. wenn ein System bereits einen Zustand eingenommen hat, der ein zukünftiges Ziel unmöglich macht).

Die Autoren konzentrieren sich auf $LTLMT_f$ (Linear-Time-Temporal-Logik über endlichen Spuren modulo Theorien), welche $LTL_f$ um beliebige SMT-Theorien erweitert. Das spezifische Problem ist die antizipative Überwachung: die Bestimmung des Überwachungszustands einer Eigenschaft $\psi$ nach einer Spur $\tau$ durch Berücksichtigung von $\tau$ und allen ihren möglichen endlichen Fortsetzungen. Die Überwachungszustände sind definiert als:

Aktuelle Erfüllung (CS): $\tau$ erfüllt $\psi$ , aber eine Verletzung ist in einer Erweiterung möglich.
Dauerhafte Erfüllung (PS): $\tau$ erfüllt $\psi$ , und keine Erweiterung kann sie verletzen.
Aktuelle Verletzung (CV): $\tau$ verletzt $\psi$ , aber eine Erfüllung ist in einer Erweiterung möglich.
Dauerhafte Verletzung (PV): $\tau$ verletzt $\psi$ , und keine Erweiterung kann sie erfüllen.

Das allgemeine Überwachungsproblem für $LTLMT_f$ ist unentscheidbar, insbesondere bei Einbeziehung linearer Arithmetik über reellen Zahlen. Der Beitrag zielt darauf ab, entscheidbare, praktisch relevante Fragmente dieser Logik zu identifizieren.

Methodik

Der vorgeschlagene Rahmen kombiniert automaten-theoretische Methoden für das temporale Reasoning mit Techniken des automatischen Reasonings (SMT) für die Datendimension.

1. Logik und Semantik

Die Autoren definieren $LTLMT_f$ über eine mehrsortige Signatur $\Sigma$ , die DatenvARIABLEN, Funktionen und Prädikate enthält. Eine zentrale semantische Entscheidung betrifft die Behandlung des zugrundeliegenden Modells $M$ :

Konservative Erweiterung: Das einer Spur zugrundeliegende Modell ist nicht festgelegt; vielmehr liefert eine Fortsetzung der Spur eine Erweiterung des Modells (via Einbettungen). Fakten über zuvor gesehene Elemente bleiben fixiert, doch neue Elemente und Fakten können eingeführt werden. Dies entspricht Szenarien wie Buchungssystemen, bei denen vergangene Preise feststehen, neue Tickets jedoch hinzukommen.
Lookback-Operator: Die Logik verwendet einen „Lookback"-Operator ( $\triangleleft$ ), um auf den vorherigen Wert einer Variable zu verweisen, anstatt einen Lookahead-Operator zu nutzen.

2. Automatenkonstruktion

Für eine gegebene quantorenfreie $LTLMT_f$ -Eigenschaft (bezeichnet als dataLTLf) konstruieren die Autoren einen nichtdeterministischen endlichen Automaten (NFA), $N_\psi$ .

Das Alphabet $\Theta$ besteht aus Mengen von Formeln der Prädikatenlogik erster Stufe (FO) (und deren Negationen), die in der Eigenschaft vorkommen.
Der NFA verfolgt die zeitliche Entwicklung der Eigenschaft und akzeptiert Wörter, die Spuren entsprechen, welche die Eigenschaft erfüllen.
Eine „sichere Lookback"-Beschränkung wird auferlegt, um sicherzustellen, dass Lookback-Variablen den Anfangszustand der Spur nicht einschränken.

3. Coreachability-Graphen und Regression

Um die Datendimension zu handhaben und antizipative Zustände zu bestimmen, führen die Autoren einen Coreachability-Graphen ( $CG^+$ ) und einen dualen Non-Coreachability-Graphen ( $CG^-$ ) ein.

Regression: Der zentrale Mechanismus ist die Operation regress, die Verifikationspflichten rückwärts durch die NFA-Übergänge propagiert. Gegeben eine Zustandsformel $\phi$ und eine Übergangsbedingung $C$ , berechnet regress( $\phi$ , $C$ ) die Bedingung im vorherigen Zustand, die erforderlich ist, um $\phi$ nach Anwendung von $C$ zu erfüllen.
Modellvollendung: Um sicherzustellen, dass die Regression in quantorenfreien Formeln resultiert (essenziell für die Entscheidbarkeit), verlässt sich der Rahmen darauf, dass die Theorie $T$ eine Modellvollendung $T^*$ besitzt. Dies ermöglicht die Elimination existenzieller Quantoren, die während der Regression eingeführt werden, und deren Umwandlung in äquivalente quantorenfreie Formeln in $T^*$ .
Graphkonstruktion: Die Knoten im Graphen sind Paare $(q, \phi)$ , wobei $q$ ein NFA-Zustand und $\phi$ eine quantorenfreie Formel ist, die die Bedingung darstellt, die erforderlich ist, um von $q$ aus einen Endzustand (oder Nicht-Endzustand) zu erreichen.

4. Überwachungsalgorithmus

Das Verfahren MONITOR arbeitet wie folgt:

Berechnung des NFA $N_\psi$ und der Coreachability-Graphen $CG^+$ und $CG^-$ .
Simulation der Spur $\tau$ auf $N_\psi$ , um den aktuellen Zustand $q$ zu identifizieren.
Auswertung der letzten Zuweisung $\alpha_n$ $α_{n}$ gegen die mit Zustand $q$ $q$ verknüpften Formeln:
- Wenn $q$ akzeptierend ist: Prüfen, ob $EXTVIOL(q)$ (die Bedingung für eine zukünftige Verletzung) erfüllt ist. Wenn ja $\to$ CS; sonst $\to$ PS.
- Wenn $q$ nicht akzeptierend ist: Prüfen, ob $EXTSAT(q)$ (die Bedingung für eine zukünftige Erfüllung) erfüllt ist. Wenn ja $\to$ CV; sonst $\to$ PV.

Hauptbeiträge

Formalisierung der antizipativen Überwachung für $LTLMT_f$ : Dies ist die erste Arbeit, die das Problem der antizipativen Überwachung für lineare-temporale Eigenschaften, die mit SMT-Theorien über endlichen Spuren angereichert sind, formal definiert und angeht.
Neuartiger Rahmen: Die Autoren präsentieren einen grundlegenden Rahmen, der NFA-basiertes temporales Reasoning mit SMT-basiertem Datenreasoning kombiniert. Eine wesentliche technische Neuerung ist die Verwendung der Modellvollendung zur Handhabung der Quantorenelimination während der rückwärtigen Regression von Verifikationspflichten, was die Konstruktion endlicher Coreachability-Graphen ermöglicht.
Identifikation entscheidbarer Fragmente: Der Beitrag identifiziert spezifische, praktisch relevante Fragmente von $LTLMT_f$ $L T L M T_{f}$ , bei denen das Überwachungsproblem lösbar ist (garantierte Terminierung):
- DB-LTLf: Eigenschaften, die Datenbankreferenzen (modelliert via Gleichheit und uninterpretierten Funktionen – EUF) mit Arithmetik kombinieren, unter spezifischen strukturellen Einschränkungen.
- Azyklische Signaturen: Gewährleistet eine endliche Anzahl von Termen.
- Monotoniebeschränkungen (MCs): Beschränkt die Arithmetik auf einfache Vergleiche ( $=, \neq, \leq, <$ ) zwischen Termen, wie sie im Monitoring von Geschäftsprozessen üblich sind.
- Lokale Endlichkeit: Eine breitere Bedingung, die eine endliche Anzahl nicht-äquivalenter Formeln sicherstellt.
- Begrenzter Lookback: Eine syntaktische Beschränkung der Interaktion von Einschränkungen in der Eigenschaft, die „Feedback-Freiheit" verallgemeinert.
Prototyp-Implementierung: Die Machbarkeit des Ansatzes wird durch MONTHE demonstriert, ein Prototyp-Tool in Python, das den CVC5 SMT-Löser für Datenreasoning und Quantorenelimination nutzt.

Ergebnisse und Evaluation

Theoretische Ergebnisse: Der Beitrag liefert formale Beweise für die Korrektheit des Überwachungsalgorithmus (Satz 18) und etabliert die Entscheidbarkeit für die identifizierten Fragmente (Sätze 19–24).
Praktische Anwendung: Der Rahmen deckt datenbewusste Geschäftsprozesse und dynamische Systeme ab, die über schreibgeschützte Datenbanken operieren (z. B. das Buchungsbeispiel, bei dem ein Agent das günstigste Ticket auswählt).
Vorläufige Evaluation: Die Autoren berichten über vorläufige Experimente mit dem MONTHE-Tool. Das Tool verarbeitet Eigenschaften und Spuren erfolgreich und gibt den korrekten Überwachungszustand aus. Die Evaluation wird als vorläufig beschrieben, wobei eine umfassende empirische Evaluation zukünftigen Arbeiten vorbehalten bleibt.

Bedeutung und Behauptungen

Der Beitrag beansprucht, der erste zu sein, der die antizipative Überwachung für datenbewusste temporale Eigenschaften adressiert. Seine Bedeutung liegt in der Überbrückung der Lücke zwischen der für moderne KI-Systeme erforderlichen Ausdruckskraft (strukturierte Daten, Arithmetik) und dem Bedarf an rigorosen, Echtzeit-Sicherheitsgarantien.

Die Autoren betonen, dass zwar die allgemeine antizipative Überwachung unentscheidbar ist, ihre Identifikation von DB-LTLf (Kombination von Arithmetik mit Datenbankreferenzen) jedoch einen „Sweet Spot" aus Ausdruckskraft und Entscheidbarkeit bietet. Dies ist insbesondere relevant für:

Datenbewusste Geschäftsprozesse: Bei denen Übergänge von Datenbankwerten und arithmetischen Einschränkungen abhängen.
Dynamische Systeme: Bei denen Agenten mit schreibgeschützten Datenbanken interagieren (z. B. Ticketmärkte, Inventarsysteme).

Die Arbeit ist in ihren Behauptungen bezüglich einer unmittelbaren industriellen Einführung bescheiden und stellt fest, dass die aktuelle Implementierung ein Prototyp ist. Zukünftige Arbeiten werden dynamische Systeme untersuchen, bei denen die Datenkomponente sich über die Zeit ändert (z. B. Aktualisierung von Ticketpreisen), was die Behandlung kontrollierter Updates der Datenbank erfordert.