💻 computer science

Monitoring Data-aware Temporal Properties (Extended Version)

Dit artikel presenteert een nieuw, formeel geverifieerd raamwerk voor anticiperend toezicht op eigenschappen in lineaire tijd verrijkt met SMT-theorieën (LTLfMT) door automaten-theoretische methoden te combineren met geautomatiseerd redeneren, waardoor beslisbare fragmenten die relevant zijn voor datagestuurde systemen worden geïdentificeerd en de haalbaarheid wordt aangetoond via een prototype-implementatie.

Oorspronkelijke auteurs: Alessandro Gianola, Marco Montali, Sarah Winkler

Gepubliceerd 2026-05-15

📖 6 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Alessandro Gianola, Marco Montali, Sarah Winkler

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 complexe, black-box machine (zoals een geavanceerde AI-agent) een taak ziet uitvoeren. Je kunt niet naar binnen kijken om de blauwdrukken of de code te controleren, maar je kunt wel de stroom van acties die het onderneemt, volgen. Je taak is om op te treden als een waakhond om ervoor te zorgen dat de machine de regels volgt.

Dit artikel introduceert een nieuw, superslim type waakhond voor AI-systemen die omgaan met data (zoals getallen, lijsten of database-recorden) over tijd.

Hier is de uiteenzetting van hun werk met behulp van eenvoudige analogieën:

1. Het Probleem: De "Kristallen Bol"-Uitdaging

De meeste traditionele waakhonden zijn als bewakingscamera's die alleen kijken naar wat er reeds is gebeurd. Als een machine een regel breekt, ziet de camera het en slaat het alarm.

De auteurs betogen echter dat je in complexe AI-systemen een Kristallen Bol nodig hebt. Je moet niet alleen weten of de machine een regel heeft gebroken, maar ook of het gedoemd is om een regel te breken, ongeacht wat het als volgende doet.

De Analogie: Stel je een wandelaar voor die op een klifrand loopt.
- Oude Waakhond: "Je bent nog niet gevallen, dus je bent veilig." (Het controleert alleen het verleden).
- Nieuwe "Anticiperende" Waakhond: "Hoewel je nog niet bent gevallen, is het pad vooruit een doodlopende weg. Wat je ook doet, je valt. Ik verklaar je nu, voordat je daadwerkelijk de rand opstapt, 'permanent geschonden'."

Dit heet Anticiperend Monitoring. Het kijkt naar de geschiedenis en alle mogelijke toekomstige scenario's om direct een oordeel te vellen.

2. De Complexiteit: Data + Tijd

De machine beweegt niet alleen; het neemt beslissingen op basis van data.

Het Voorbeeld: Denk aan een bot voor concerttickets. Elke seconde ziet het een nieuw ticketaanbod. Het moet beslissen: "Moet ik mijn huidige genoteerde ticket houden, of overstappen naar deze nieuwe?"
De Regel: "Kies altijd het goedkoopste ticket voor het specifieke concert dat ik wil."
De Uitdaging: De bot moet bij elke stap prijzen vergelijken (wiskunde) en concertnamen controleren (data). Als de bot een ticket kiest dat $100 kost, maar er verschijnt later een ticket van $50 voor hetzelfde concert, moet de bot overstappen. Als dat niet gebeurt, is het kapot.

De auteurs hebben een taal (een reeks regels) ontwikkeld om deze complexe, datavolle regels te beschrijven. Ze noemen het LTLMTf.

3. De Oplossing: De "Terugwaartse Kaart"

De auteurs stonden voor een enorm probleem: het voorspellen van de toekomst voor een machine met oneindige mogelijkheden is meestal onmogelijk (wiskundig "onbeslisbaar"). Het is alsof je probeert elke mogelijke zet te voorspellen in een schaakspel dat nooit eindigt.

Om dit op te lossen, bouwden ze een Terugwaartse Kaart (een technisch hulpmiddel genaamd een Coreachability Graph).

De Analogie: In plaats van te proberen elke weg te raden die de wandelaar vooruit zou kunnen nemen, stel je voor dat je bij de finishlijn (het doel) begint en achteruit werkt.
1. Je markeert de plekken waar de wandelaar de wandeling succesvol afrondt.
2. Je vraagt: "Welke voorwaarden moeten nu waar zijn om die goede plekken te bereiken?"
3. Je blijft achteruit lopen en maakt een kaart van "Veilige Zones" en "Gevarenzones".

Door deze kaart achteruit te bouwen, kunnen ze naar de huidige positie van de wandelaar kijken en direct weten: "Is er een pad vooruit dat leidt tot succes?"

Als Ja: Het systeem is nu veilig, maar kan later falen (Huidige Voldoening).
Als Nee: Het systeem is nu veilig, maar zal zeker falen, ongeacht wat er gebeurt (Permanente Voldoening - wacht, dit betekent eigenlijk dat het permanent veilig is? Nee, laten we de analogie corrigeren op basis van de logica van het artikel).

Correctie op de Oordelen:
Het artikel definieert vier toestanden voor de waakhond:

Huidige Voldoening (CS): Je bent nu goed, maar je kunt later in de fout gaan.
Permanente Voldoening (PS): Je bent nu goed, en je bent gewaarborgd om goed te blijven, ongeacht wat er als volgende gebeurt.
Huidige Schending (CV): Je hebt een fout gemaakt, maar je kunt het later misschien herstellen.
Permanente Schending (PV): Je hebt een fout gemaakt en er is geen enkele manier om het te herstellen. Het spel is voorbij.

Het "Anticiperende" deel is het vermogen om PV (Permanente Schending) direct op te sporen, in plaats van te wachten tot het systeem crasht.

4. De Magische Truc: "Model Voltooiing"

Hoe hebben ze deze terugwaartse kaart mogelijk gemaakt zonder verdwaald te raken in oneindige wiskunde? Ze gebruikten een wiskundige truc genaamd Model Voltooiing.

De Analogie: Stel je voor dat je probeert een doolhof op te lossen, maar het doolhof blijft nieuwe muren toevoegen.
- De auteurs vonden een manier om het doolhof "glad te strijken". Ze bewezen dat voor bepaalde soorten regels (specifiek die welke databases en rekenkunde zoals optellen/aftrekken betreffen), je het groeiende doolhof kunt behandelen alsof het een vaste, beheersbare grootte heeft.
- Ze identificeerden specifieke "veilige zones" van regels (zoals DB-LTLf-MC) waar de wiskunde zich netjes gedraagt. In deze zones is de "Terugwaartse Kaart" gegarandeerd eindig en oplosbaar.

5. Het Resultaat: Een Werkend Prototype

Ze schreven niet alleen theorie; ze bouwden een prototype-tool genaamd MONTHE.

Ze testten het op het voorbeeld van de concertticket-bot.
De tool observeerde succesvol de "ticket-bot" en kon direct zeggen: "Hé, die bot heeft een ticket van $100 gekozen, maar het concert kost $50. Het is nu Permanente Schending omdat het de $50-ticket nooit zal vinden als het de data blijft negeren."

Samenvatting

Dit artikel gaat over het bouwen van een superwaakzame bewaker voor AI-systemen.

Oude Bewaker: "Je hebt de regel nog niet gebroken."
Nieuwe Bewaker: "Ik zie de toekomst. Je breekt nu de regel en er is geen manier voor je om het te herstellen. Ik markeer je direct als 'Permanente Schending'."

Ze hebben dit bereikt door tijdreisl-logic (kijken naar het verleden en de toekomst) te combineren met database-wiskunde, maar alleen voor specifieke soorten regels waar de wiskunde niet te gek wordt om op te lossen. Ze hebben bewezen dat het werkt en een tool gebouwd om het te doen.

Technische Samenvatting: Monitoring van datagerelateerde temporele eigenschappen

Probleemdefinitie

Het artikel behandelt de uitdaging van anticiperende runtime-verificatie voor complexe, dynamische AI-systemen waarbij interne specificaties ontoegankelijk zijn (black-box systemen). Traditionele verificatiemethoden op ontwerptijd, zoals modelchecking, zijn in deze scenario's vaak niet toepasbaar. Hoewel Runtime Verification (RV) een oplossing biedt door uitvoeringstraces te monitoren, lopen bestaande benaderingen tegen twee primaire beperkingen aan:

Propositionele aard: Standaard Lineaire Tijdslogica over eindige traces ( $LTL_f$ ) kan geen eigenschappen uitdrukken die gestructureerde data betreffen (bijvoorbeeld rekenkunde, verzamelingen, niet-geïnterpreteerde functies), die alomtegenwoordig zijn in moderne AI-agenten en bedrijfsprocessen.
Gebrek aan anticipatie: De meeste monitors evalueren alleen het tot nu toe waargenomen trace-voorvoegsel. Ze slagen er niet in om schendingen te detecteren die onvermijdelijk zijn, ongeacht hoe de trace verder verloopt (bijvoorbeeld als een systeem zich al heeft vastgelegd op een staat die een toekomstig doel onmogelijk maakt).

De auteurs richten zich op $LTLMT_f$ (Lineaire Tijdslogica over eindige traces modulo theorieën), wat $LTL_f$ verrijkt met willekeurige SMT-theorieën. Het specifieke probleem is anticiperende monitoring: het bepalen van de monitoringstaat van een eigenschap $\psi$ na een trace $\tau$ door rekening te houden met $\tau$ en alle mogelijke eindige voortzettingen ervan. De monitoringstaten worden gedefinieerd als:

Huidige Voldoening (CS): $\tau$ voldoet aan $\psi$ , maar een schending is mogelijk in sommige uitbreidingen.
Permanente Voldoening (PS): $\tau$ voldoet aan $\psi$ , en geen enkele uitbreiding kan deze schenden.
Huidige Schending (CV): $\tau$ schendt $\psi$ , maar voldoening is mogelijk in sommige uitbreidingen.
Permanente Schending (PV): $\tau$ schendt $\psi$ , en geen enkele uitbreiding kan hieraan voldoen.

Het algemene monitoringprobleem voor $LTLMT_f$ is onbeslisbaar, met name bij het betrekken van lineaire rekenkunde over reële getallen. Het artikel beoogt beslisbare, praktisch relevante fragmenten van deze logica te identificeren.

Methodologie

Het voorgestelde raamwerk combineert automata-theoretische methoden voor temporele redenering met geautomatiseerde redeneertechnieken (SMT) voor de datadimensie.

1. Logica en Semantiek

De auteurs definiëren $LTLMT_f$ over een multi-gesorteerd signatuur $\Sigma$ dat datavariabelen, functies en predicaten bevat. Een cruciale semantische keuze is de behandeling van het onderliggende model $M$ :

Conservatieve Uitbreiding: Het model dat aan een trace ten grondslag ligt, is niet vast; eerder biedt een voortzetting van de trace een uitbreiding van het model (via inbeddingen). Feiten over eerder waargenomen elementen blijven vast, maar nieuwe elementen en feiten kunnen worden geïntroduceerd. Dit sluit aan bij scenario's zoals ticketsystemen, waar oude prijzen vaststaan, maar nieuwe tickets verschijnen.
Lookback-operator: De logica gebruikt een "lookback"-operator ( $\triangleleft$ ) om te verwijzen naar de vorige waarde van een variabele, in plaats van een lookahead-operator.

2. Automata-constructie

Voor een gegeven kwantoren-vrije $LTLMT_f$ -eigenschap (verwezen als dataLTLf) construeren de auteurs een Niet-deterministische Eindige Automaat (NFA), $N_\psi$ .

Het alfabet $\Theta$ bestaat uit verzamelingen van eerste-orde (FO) formules (en hun negaties) die in de eigenschap voorkomen.
De NFA volgt de temporele evolutie van de eigenschap en accepteert woorden die overeenkomen met traces die aan de eigenschap voldoen.
Een "veilige lookback"-beperking wordt opgelegd om ervoor te zorgen dat lookback-variabelen de beginstaat van de trace niet beperken.

3. Coreachabiliteitsgrafieken en Regressie

Om de datadimensie te hanteren en anticiperende staten te bepalen, introduceren de auteurs een coreachabiliteitsgraaf ( $CG^+$ ) en een duale non-coreachabiliteitsgraaf ( $CG^-$ ).

Regressie: De kernmechanisme is de regress-operatie, die verificatieverplichtingen achterwaarts door de NFA-overgangen propageert. Gegeven een staatformule $\phi$ en een overgangsbeperking $C$ , berekent regress( $\phi$ , $C$ ) de voorwaarde in de vorige staat die nodig is om $\phi$ te voldoen na toepassing van $C$ .
Modelcompletie: Om ervoor te zorgen dat de regressie resulteert in kwantoren-vrije formules (essentieel voor beslisbaarheid), vertrouwt het raamwerk erop dat de theorie $T$ een modelcompletie $T^*$ heeft. Dit maakt het elimineren van existentiële kwantoren mogelijk die tijdens regressie worden geïntroduceerd, en converteert deze naar equivalente kwantoren-vrije formules in $T^*$ .
Gravconstructie: Knopen in de graaf zijn paren $(q, \phi)$ , waarbij $q$ een NFA-staat is en $\phi$ een kwantoren-vrije formule die de voorwaarde vertegenwoordigt die nodig is om vanuit $q$ een finale (of niet-finale) staat te bereiken.

4. Monitoringalgoritme

De procedure MONITOR werkt als volgt:

Bereken de NFA $N_\psi$ en de coreachabiliteitsgrafieken $CG^+$ en $CG^-$ .
Simuleer de trace $\tau$ op $N_\psi$ om de huidige staat $q$ te identificeren.
Evalueer de laatste toewijzing $\alpha_n$ $α_{n}$ tegenover de formules geassocieerd met staat $q$ $q$ :
- Als $q$ accepterend is: Controleer of EXTVIOL( $q$ ) (de voorwaarde voor een toekomstige schending) is voldaan. Zo ja $\to$ CS; anders $\to$ PS.
- Als $q$ niet-accepterend is: Controleer of EXTSAF( $q$ ) (de voorwaarde voor een toekomstige voldoening) is voldaan. Zo ja $\to$ CV; anders $\to$ PV.

Belangrijkste Bijdragen

Formalisatie van Anticiperende Monitoring voor $LTLMT_f$ : Dit is het eerste werk dat het probleem van anticiperende monitoring voor lineaire tijds-eigenschappen verrijkt met SMT-theorieën over eindige traces formeel definieert en aanpakt.
Nieuw Raamwerk: De auteurs presenteren een fundamenteel raamwerk dat NFA-gebaseerde temporele redenering combineert met SMT-gebaseerde data-redenering. Een belangrijke technische nieuwigheid is het gebruik van modelcompletie om kwantoreneliminatie te hanteren tijdens de achterwaartse regressie van verificatieverplichtingen, waardoor de constructie van eindige coreachabiliteitsgrafieken mogelijk wordt.
Identificatie van Beslisbare Fragmenten: Het artikel identificeert specifieke, praktisch relevante fragmenten van $LTLMT_f$ $L T L M T_{f}$ waar het monitoringprobleem oplosbaar is (gewaarborgde terminatie):
- DB-LTLf: Eigenschappen die database-referenties (gemodelleerd via Gelijkheid en Niet-geïnterpreteerde Functies - EUF) combineren met rekenkunde, onder specifieke structurele beperkingen.
- Acyclische Signatures: Zorgt voor een eindig aantal termen.
- Monotoniteitsbeperkingen (MC's): Beperkt rekenkunde tot eenvoudige vergelijkingen ( $=, \neq, \leq, <$ ) tussen termen, wat gebruikelijk is in monitoring van bedrijfsprocessen.
- Lokale Eindigheid: Een bredere voorwaarde die een eindig aantal niet-equivalente formules garandeert.
- Beperkte Lookback: Een syntactische beperking op de interactie van beperkingen in de eigenschap, die "feedback-vrijheid" generaliseert.
Prototype-implementatie: De haalbaarheid van de benadering wordt aangetoond via MONTHE, een prototype-tool geïmplementeerd in Python die de CVC5 SMT-oplosser gebruikt voor data-redenering en kwantoreneliminatie.

Resultaten en Evaluatie

Theoretische Resultaten: Het artikel levert formele bewijzen voor de correctheid van het monitoringalgoritme (Stelling 18) en vestigt beslisbaarheid voor de geïdentificeerde fragmenten (Stellingen 19–24).
Praktische Toepassing: Het raamwerk blijkt data-bewuste bedrijfsprocessen en dynamische systemen te dekken die werken over read-only databases (bijvoorbeeld het ticketvoorbeeld waarbij een agent het goedkoopste ticket selecteert).
Voorlopige Evaluatie: De auteurs rapporteren voorlopige experimenten met de MONTHE-tool. De tool verwerkt succesvol eigenschappen en traces en geeft de juiste monitoringstaat uit. De evaluatie wordt beschreven als voorlopig, waarbij uitgebreide empirische evaluatie wordt overgelaten aan toekomstig werk.

Betekenis en Aanspraken

Het artikel claimt het eerste te zijn dat anticiperende monitoring voor datagerelateerde temporele eigenschappen aanpakt. De betekenis ligt in het overbruggen van de kloof tussen het uitdrukkingsvermogen dat vereist is voor moderne AI-systemen (gestructureerde data, rekenkunde) en de behoefte aan rigoureuze, real-time veiligheidsgaranties.

De auteurs benadrukken dat hoewel algemene anticiperende monitoring onbeslisbaar is, hun identificatie van DB-LTLf (rekenkunde gecombineerd met database-referenties) een "sweet spot" biedt van uitdrukkingsvermogen en beslisbaarheid. Dit is bijzonder relevant voor:

Data-bewuste Bedrijfsprocessen: Waar overgangen afhangen van database-waarden en rekenkundige beperkingen.
Dynamische Systemen: Waar agenten interageren met read-only databases (bijvoorbeeld ticketmarkten, voorraadsystemen).

Het werk is bescheiden in zijn claims met betrekking tot directe industriële implementatie, en merkt op dat de huidige implementatie een prototype is en dat toekomstig werk dynamische systemen zal verkennen waarbij de data-component in de loop van de tijd verandert (bijvoorbeeld het updaten van ticketprijzen), wat het hanteren van gecontroleerde updates aan de database vereist.