Riepilogo Tecnico: Materializzazione Efficiente di Datalog Temporale per il Riconoscimento di Eventi Compositi

Enunciato del Problema

I framework per il Riconoscimento di Eventi Compositi (CER) sono essenziali per rilevare situazioni critiche (ad esempio, minacce alla sicurezza) su flussi di eventi simbolici ad alta velocità. Tali framework consistono tipicamente in un Linguaggio di Specifica degli Eventi (ESL) per definire i pattern e in un motore di ragionamento su flusso per valutarli. Tuttavia, gli ESL esistenti sono spesso studiati in isolamento, complicando i confronti riguardanti l'espressività e offuscando la portata dei loro motori di ragionamento associati. Inoltre, i pattern espressi in un ESL non possono spesso essere tradotti fedelmente o in modo ottimale in un altro, impedendo l'uso del motore di ragionamento più adatto per un problema specifico. Manca un formalismo unificante che possa incorporare ESL prominenti supportando al contempo un ragionamento efficiente e a bassa latenza su flussi illimitati.

Metodologia

Gli autori propongono un approccio unificato incentrato su Temporal Datalog$^{\rightarrow}_{\ominus}$, una variante di Temporal Datalog che presenta negazione stratificata e nessuna dipendenza dal futuro (propagazione in avanti). La metodologia coinvolge due componenti principali:

1. Incorporamento degli ESL in Temporal Datalog$^{\rightarrow}_{\ominus}$

Il documento presenta mappature da due ESL basati sulla logica prominenti verso Temporal Datalog$^{\rightarrow}_{\ominus}$, dimostrando che queste traduzioni preservano l'equivalenza rispetto alla risposta alle query:

• Plain LARS: Un frammento del linguaggio LARS (basato sulla Programmazione per Insiemi di Risposte con operatori a finestra). La traduzione (Algoritmo 2) gestisce le modalità temporali ($\diamond$, $\square$) e gli operatori a finestra ($\boxplus$) introducendo predicati ausiliari e fissando le variabili temporali. Garantisce che il programma risultante sia a propagazione in avanti e temporalmente stratificato.
• Event Calculus con Effetti Ritardati (ECDE): Una variante del Calcolo degli Eventi utilizzata nel CER su larga scala. La traduzione (Algoritmo 3) elimina i funtori (tipi di evento/fluido) introducendo predicati specifici per ogni tipo e valore. Codifica la legge dell'inerzia, gli effetti ritardati e le definizioni di fluidi statici in regole a propagazione in avanti, garantendo la stratificazione temporale.

2. Grafi di Attivazione per Flusso (STG)

Per supportare una materializzazione efficiente di Temporal Datalog$^{\rightarrow}_{\ominus}$, gli autori propongono i Grafi di Attivazione per Flusso (STG), un'estensione dei Grafi di Attivazione (TG). I TG standard sono insufficienti perché non supportano nativamente la negazione o l'infinita fissazione delle variabili temporali richiesta per lo streaming.

• Grafi di Esecuzione per Flusso (SEG): Gli STG sono costruiti su SEG, che estendono i Grafi di Esecuzione includendo:
  • Negazione: Rappresentata tramite archi-$n$ (iperarchi) che agiscono come filtri, impedendo la derivazione di fatti se sono soddisfatte specifiche condizioni negative.
  • Tempo: I nodi sono associati a istanti temporali specifici e gli archi impongono offset temporali coerenti con le regole.
• Stratificazione Incrementale: Per abilitare aggiornamenti incrementali senza ricalcolare l'intero grafo, gli autori definiscono una stratificazione incrementale. Ciò permette al sistema di elaborare le regole per strati relativi a un istante temporale specifico $t$, garantendo che i fatti per il tempo $t$ siano derivati utilizzando fatti da $t$ o precedenti, ma mai dal futuro.
• Coerenza vs. $k$-compatibilità: Gli autori introducono un criterio di "coerenza" per la costruzione dei nodi. A differenza della standard $k$-compatibilità (che richiede che almeno un nodo di input provenga dall'iterazione corrente $k-1$), la coerenza permette la costruzione di nodi se sono stati costruiti in qualsiasi iterazione precedente, a condizione che le loro etichette temporali corrispondano ai requisiti della regola. Ciò impedisce al processo di materializzazione di bloccarsi quando le dipendenze si estendono su più passaggi temporali.
• Ottimizzazioni: L'approccio incorpora ottimizzazioni standard dei TG (rimozione della sussunzione, aggiornamenti basati su delta) e introduce un meccanismo di "dimenticanza". Nodi e fatti vengono rimossi dal grafo una volta che i loro timestamp superano l'offset temporale massimo richiesto da qualsiasi regola, garantendo un uso della memoria limitato.

Contributi Chiave

1. Mappature Formali: Il documento fornisce e dimostra la correttezza delle mappature da frammenti pratici di Plain LARS ed ECDE verso Temporal Datalog$^{\rightarrow}_{\ominus}$. Ciò stabilisce Temporal Datalog$^{\rightarrow}_{\ominus}$ come un formalismo naturale per incorporare e confrontare questi linguaggi.
2. Grafi di Attivazione per Flusso (STG): Un nuovo algoritmo di ragionamento e un modello computazionale specificamente progettati per Temporal Datalog$^{\rightarrow}_{\ominus}$. Gli STG supportano la negazione stratificata e gestiscono la natura infinita delle variabili temporali attraverso stratificazione incrementale e controlli di coerenza.
3. Meccanismo CER Uniforme: Unificando gli ESL sotto un singolo formalismo e motore di ragionamento, il lavoro facilita l'analisi formale e il confronto di diversi linguaggi di specifica degli eventi, allontanandosi da soluzioni ad hoc e isolate.

Risultati e Correttezza

Il documento fornisce prove teoriche piuttosto che risultati sperimentali empirici.

• Correttezza della Traduzione: Il Teorema 1 e il Teorema 2 dimostrano che le traduzioni da Plain LARS ed ECDE verso Temporal Datalog$^{\rightarrow}_{\ominus}$ preservano la semantica del modello perfetto dei programmi originali.
• Correttezza di STGmat: Il Teorema 3 dimostra che l'Algoritmo 4 (STGmat) costruisce correttamente un Grafo di Attivazione per Flusso che produce gli stessi fatti della valutazione modello-teorica standard del programma su un flusso.
• Terminazione ed Efficienza: L'uso della stratificazione incrementale e del meccanismo di "dimenticanza" (Proposizione 1) garantisce che il processo di materializzazione non rimanga intrappolato in derivazioni infinite e che l'uso della memoria sia gestito scartando i fatti che non possono più influenzare le derivazioni future.

Significato e Affermazioni

Gli autori affermano che questo lavoro affronta la frammentazione nel campo del CER fornendo un meccanismo uniforme per il riconoscimento di eventi compositi.

• Generalizzazione: L'approccio è progettato per generalizzarsi su un'ampia gamma di linguaggi pratici di specifica degli eventi che condividono le proprietà della negazione stratificata e dell'assenza di dipendenze dal futuro, requisiti comuni nel ragionamento su flusso.
• Efficienza: Estendendo le tecniche all'avanguardia di materializzazione Datalog (Grafi di Attivazione) per gestire flussi temporali con negazione, gli STG proposti offrono una via verso un ragionamento efficiente e a bassa latenza senza la necessità di ottimizzazioni ad hoc per ogni linguaggio specifico.
• Consolidamento Fondamentale: Il lavoro aiuta a consolidare le fondamenta teoriche del CER, permettendo studi di compromesso principiati tra espressività e trattabilità del ragionamento.

Il documento conclude notando che, sebbene assuma flussi di input ordinati, la gestione di flussi non ordinati e le estensioni probabilistiche sono lasciate a lavori futuri. I contributi sono inquadrati come un passo verso l'avanzamento dello stato dell'arte nel riconoscimento di eventi compositi attraverso l'unificazione e una materializzazione efficiente.