Riepilogo Tecnico: Semantica Stratificata per Sort in base alla Rilevazione di Conflitti Temporali nelle Policy ODRL

1. Definizione del Problema

L'Open Digital Rights Language (ODRL) 2.2 è ampiamente adottato negli spazi di dati per definire le policy di utilizzo per gli asset digitali. Queste policy includono frequentemente vincoli temporali che coinvolgono due distinti sort di operandi: istanti (punti nel tempo, ad es. dateTime) e durate (quantità di tempo, ad es. elapsedTime, meteredTime, delayPeriod, timeInterval).

Il problema centrale identificato è che gli operatori di confronto di ODRL (ad es. lt, lteq, gteq) non distinguono tra questi sort. Di conseguenza, un operatore come lt è ambiguo: implica "precedente a" per gli istanti ma "più breve di" per le durate. Questa mancanza di stratificazione dei sort porta a due criticità fondamentali:

1. Rilevazione dei Conflitti Non Sound (Non Fondata): Le formalizzazioni e i motori esistenti spesso trattano gli attributi temporali come privi di sort, permettendo confronti non validi (ad es. confrontare una data con una durata) o fallendo nel rilevare conflitti derivanti dall'interazione tra diversi operandi temporali.
2. Conflitti tra Operandi Mancati: I vincoli sono spesso interdipendenti. Ad esempio, il meteredTime (utilizzo effettivo) non può superare l' elapsedTime (tempo trascorso dall'inizio dell'accesso). Una policy che offre 30 giorni di utilizzo misurato e una richiesta che limita il tempo trascorso totale a 10 giorni sono singolarmente soddisfacibili ma congiuntamente insoddisfacibili. I controlli standard per singolo operando perdono questo conflitto.

Inoltre, i lavori esistenti (ad es. Salas et al., Bonatti et al.) si concentrano principalmente sul solo dateTime, ignorando l'aritmetica delle durate, la ricorrenza (timeInterval) e le sequenze ordinate (andSequence).

2. Metodologia

Gli autori propongono una semantica denotazionale stratificata per sort per i vincoli temporali di ODRL. La metodologia procede attraverso le seguenti fasi:

2.1 Stratificazione dei Sort e Semantica degli Intervalli

Il framework assegna un sort unico a ogni operando temporale:

• Sort Istante (Inst): Interpretato su una linea temporale lineare $T$ (isomorfa a $\mathbb{Q}$).
• Sort Durata (Dur): Interpretato su un monoide commutativo cancellativo totalmente ordinato $D$ (isomorfo a $\mathbb{Q}_{\geq 0}$).

Gli operatori sono limitati agli operatori di intervallo (eq, lt, lteq, gt, gteq), garantendo che l'insieme delle soluzioni per qualsiasi vincolo sia un sottoinsieme ordine-convesso (un intervallo) del dominio dell'operando.

• Vincoli Periodici: L'operando timeInterval è trattato come un insieme periodico di istanti $Per(a, p) = \{a + kp \mid k \in \mathbb{Z}\}$, dove $a$ è un'ancora e $p$ è un periodo.

2.2 Denotazione Prodotto e Teoria di Sfondo

Il significato di una policy è definito come il prodotto delle denotazioni dei suoi singoli vincoli.

• Asse degli Istanti: dateTime e timeInterval sono combinati in una singola denotazione di "asse degli istanti", che rappresenta l'intersezione tra una finestra temporale e un pattern di ricorrenza.
• Assi delle Durate: Altri operandi (elapsedTime, meteredTime, delayPeriod) formano assi indipendenti.
• Teoria di Sfondo ($\Phi$): Per catturare le relazioni tra operandi, la semantica include una teoria di sfondo $\Phi$ che impone:
  • Le durate sono non negative.
  • meteredTime $\le$ elapsedTime.
  • delayPeriod $\le$ elapsedTime.
  • L'ordinamento temporale degli eventi di accesso.

Il conflitto è definito come l'insoddisfacibilità della congiunzione di due policy ($C_1 \land C_2$) sotto la teoria di sfondo $\Phi$.

2.3 Procedura Decisionale a Livelli (Tiered)

La complessità del controllo di soddisfacibilità varia in base ai vincoli coinvolti. Gli autori classificano il problema in tre livelli (tier), ciascuno con una specifica procedura decisionale:

1. Livello d'Ordine (Ord): Si applica quando i vincoli limitano solo gli operandi tramite letterali senza relazioni tra operandi diversi. È deciso tramite semplice confronto di limiti (EPR/logica del primo ordine).
2. Livello di Differenza (Diff): Si applica quando i vincoli coinvolgono differenze tra istanti o relazioni tra operandi diversi (ad es. meteredTime vs elapsedTime). È deciso controllando la presenza di cicli negativi in un grafo di differenza (PTIME).
3. Livello Modulare (Mod): Si applica quando sono coinvolti vincoli periodici (timeInterval). È deciso utilizzando l'aritmetica di Presburger (test di divisibilità su periodi e ancore).

2.4 Verdeti a Tre Valori

Il framework restituisce uno di tre verdeti per una coppia di policy:

• Conflitto (Conflict): Le policy sono congiuntamente insoddisfacibili.
• Compatibile (Compatible): Esiste almeno un'esecuzione valida che soddisfa entrambe.
• Sconosciuto (Unknown): Solo una policy vincola un operando specifico, lasciando l'insoddisfacibilità congiunta indeterminata senza ulteriori informazioni.

Questa logica si estende agli operatori logici (and, or, xone) e alle sequenze (andSequence), dove andSequence è modellata come un sistema di vincoli basato su tracce.

3. Contributi Chiave

• Semantica Formale: La prima formalizzazione dei vincoli temporali di ODRL che distingue esplicitamente tra istanti e durate, risolvendo l'ambiguità degli operatori.
• Rilevazione di Conflitti tra Operandi: Un meccanismo per rilevare conflitti derivanti dall'interazione tra diversi operandi temporali (ad es. limiti di utilizzo vs tempo trascorso), che i precedenti approcci privi di sort non riuscivano a cogliere.
• Caratterizzazione della Decidibilità: Una prova che la rilevazione dei conflitti per l'intero set di vincoli temporali di ODRL (inclusi ricorrenza e sequenze) è decidibile riducendo il problema a tre specifici frammenti risolvibili (Ordine, Differenza, Modulare).
• Ponte Statico-Runtime: Una prova teorica che un conflitto statico rilevato al momento della negoziazione è sound (garantito durante l'esecuzione), mentre una compatibilità statica non garantisce la conformità a runtime (a causa dell'utilizzo effettivo che può superare i tetti massimi).
• Benchmarking: La creazione di un benchmark di 72 problemi di rilevazione dei conflitti codificati in TPTP e SMT-LIB, che copre varie categorie (operando singolo, tra operandi, periodico, sequenze).

4. Risultati

Gli autori hanno valutato il framework utilizzando quattro ragionatori automatizzati: Vampire, E, Z3 e cvc5.

• Completezza: Tutti i 72 problemi del benchmark sono stati decisi da almeno un ragionatore.
• Correttezza: Nessun ragionatore ha restituito un verdetto errato. L'accordo tra i diversi encoding (TPTP vs SMT-LIB) e i solver conferma che i verdeti sono proprietà della semantica, non dell'encoding.
• Prestazioni dei Solver:
  • E ha risolto tutti i 48 problemi del livello "Order".
  • Vampire ha risolto 62 problemi (Livello Order + 14 problemi del livello "Difference").
  • Z3 e cvc5 hanno risolto tutti i 72 problemi, inclusi i 10 problemi del livello "Modular" che coinvolgono periodicità e fattibilità di traccia, i quali richiedono capacità SMT.
• Risultati Specifici: La valutazione ha dimostrato che le letture non sortizzate producono conflitti spuri, mentre l'approccio stratificato per sort identifica correttamente gli accordi validi. Ha inoltre confermato che i vincoli andSequence richiedono il livello Difference per la risoluzione.

5. Significato e Rivendicazioni

Il documento afferma che il suo contributo primario è la caratterizzazione della decidibilità e la riduzione a livelli della rilevazione dei conflitti temporali in ODRL. Separando istanti e durate e modellando esplicitamente le loro interazioni, il framework fornisce una base solida per la negoziazione delle policy negli spazi di dati.

Gli autori sottolineano che il loro lavoro è di portata modesta:

• Si concentra strettamente sugli aspetti temporali di ODRL, escludendo vincoli non temporali e altre costruzioni di regole (doveri, rimedi).
• Evita i frammenti indecidibili della logica temporale metrica su tempo denso, limitando la semantica a sottoframmenti decidibili (Logica della Differenza e Aritmetica di Presburger).
• Fornisce una fondazione teorica e un benchmark, piuttosto che un motore di enforcement completo per la produzione, sebbene suggerisca che la semantica possa guidare un tale motore.

Questo lavoro stabilisce che la rilevazione dei conflitti per l'intero set di operandi temporali di ODRL non è solo possibile, ma può essere efficacemente categorizzata e risolta utilizzando strumenti di ragionamento automatizzato esistenti.