Reducing Arbitrary Metric Temporal Formulas into Logic Programs under Answer Set Semantics

Problema
La Logica dell'Equilibrio Temporale Metrico (MEL) estende la Logica dell'Equilibrio Temporale (TEL) incorporando vincoli temporali quantitativi, consentendo la specifica di scadenze e durate in sistemi dinamici come i sistemi embedded e cyber-fisici. Sebbene la MEL permetta espressioni precise come "un evento deve verificarsi entro 5 millisecondi", le implementazioni esistenti affrontano diverse sfide. Le precedenti riduzioni della MEL in programmazione ASP proposizionale (ad esempio, da Becker et al.) portano spesso a programmi logici contenenti atomi del futuro puro nelle teste delle regole, creando dipendenze future. Queste dipendenze ostacolano l'efficienza dei solver incrementali e multi-shot, che operano meglio quando le derivazioni dello stato corrente si basano esclusivamente su informazioni provenienti da stati precedentemente computati piuttosto che su stati futuri non ancora computati. Inoltre, le traduzioni esistenti non gestiscono appieno gli operatori temporali metrici binari come l'until metrico o il release metrico.

Metodologia
Gli autori propongono una traduzione di tipo Tseitin-like che mappa formule temporali metriche arbitrarie in un frammento specifico di programmi di logica temporale metrica. La metodologia centrale prevede:

1. Restrizione a Tracce Rigide: L'approccio assume tracce rigide in cui i punti temporali aumentano strettamente ($\tau(i) < \tau(i+1)$). Ciò consente di srotolare ricorsivamente gli operatori metrici binari con intervalli $[0..n]$ utilizzando equivalenze che collassano gli operatori nei loro argomenti di destra o in costanti di verità quando l'intervallo è $[0..0]$.
2. Definizione di Chiusura: Ispirandosi alla chiusura di Fisher-Ladner nelle logiche dinamiche, gli autori definiscono un insieme di chiusura $cl(\phi)$ per una formula $\phi$. Questo insieme include non solo le sottoformule, ma anche le espansioni ricorsive degli operatori metrici binari (ad esempio, $\phi U_{\le n} \psi$ genera $\bigcirc^i(\phi U_{\le n-i} \psi)$).
3. Semantica a Tre Valori: Per dimostrare la correttezza della traduzione, l'articolo utilizza una caratterizzazione a tre valori della logica Metric Here-and-There (MHT). Questa semantica, equivalente a MHT, semplifica la verifica delle equivalenze logiche necessarie per la riduzione.
4. Regole di Traduzione: La traduzione introduce atomi ausiliari (etichette) per ogni formula nella chiusura. Genera regole in cui gli operatori del futuro influenzano solo le implicazioni, mentre i corpi e le teste di queste implicazioni contengono solo riferimenti al passato e al presente. La traduzione distingue tra regole dinamiche (che coinvolgono operatori next/previous) e regole iniziali/finali.
5. Ordine Ben Fondato: Per gestire la natura non strutturale della chiusura (dove le formule srotolate non sono vere e proprie sottoformule), gli autori definiscono una misura di complessità $u(\phi)$ basata sullo srotolamento degli operatori, stabilendo un ordine parziale stretto ben fondato per supportare le prove induttive.

Contributi Chiave

• Riduzione di tipo Tseitin: Una riduzione formale da formule temporali metriche arbitrarie a programmi di logica temporale metrica limitati agli operatori del passato nei corpi delle regole.
• Gestione degli Operatori Binari: La traduzione gestisce esplicitamente gli operatori metrici binari ($U_{\le n}, R_{\le n}, S_{\le n}, T_{\le n}$) con intervalli della forma $[0..n]$, un limite nelle precedenti codifiche ASP proposizionali.
• Eliminazione delle Dipendenze Future: Garantendo che i corpi delle regole si basino solo su informazioni passate e presenti, i programmi logici risultanti sono compatibili con le tecniche di solving incrementale utilizzate in solver come telingo.
• Correttezza Formale: L'articolo dimostra che la traduzione preserva l'insieme dei Modelli di Equilibrio Metrico (equivalenza forte modulo atomi ausiliari) e stabilisce un limite polinomiale sulla dimensione del programma generato rispetto alla dimensione della formula di input e al valore massimo dell'intervallo $n$.

Risultati
L'articolo dimostra che per ogni formula temporale metrica $\phi$, esiste un programma di logica temporale metrica $\Gamma$ tale che i modelli di equilibrio metrico di $\phi$ corrispondono esattamente alla proiezione dei modelli di equilibrio metrico di $\Gamma$ sull'alfabeto originale. La dimensione del programma generato è limitata da una funzione polinomiale della dimensione della formula e del valore massimo dell'intervallo $n$. La correttezza della traduzione è dimostrata sotto l'assunto di tracce rigide e intervalli della forma $[0..n]$.

Significatività
L'articolo sostiene di fornire una "forma normale" per interpretare teorie temporali metriche sotto la semantica dell'answer set. Collegando le formule temporali metriche con i programmi di logica che sono limitati agli operatori del passato, il lavoro permette di sfruttare i già esistenti ed efficienti solver ASP (specificamente quelli che supportano il multi-shot e lo solving incrementale) per il ragionamento su vincoli temporali metrici. Ciò facilita l'implementazione pratica della MEL in domini che richiedono una temporizzazione precisa, come i software real-time e i sistemi embedded, senza le inefficienze associate alle dipendenze future. Gli autori osservano che, sebbene l'attuale lavoro sia limitato agli intervalli $[0..n]$, esso pone le basi per estendere queste riduzioni ad intervalli arbitrari e integrarle nel solver telingo.