💻 computer science

Sort-Stratified Semantics for Temporal Conflict Detection in ODRL Policies

Dit artikel behandelt de onjuistheid van temporele conflictdetectie in ODRL-policies veroorzaakt door ambigue vergelijkingsoperatoren tussen instanties en duur door een soort-gestratificeerde semantiek te introduceren die operanden typeert, conflictcontrole reduceert tot intervalvergelijking met een driewaardig oordeel, en de beslisbaarheid en correctheid ervan bewijst via statische en runtime-evaluaties.

Oorspronkelijke auteurs: Daham M. Mustafa, Diego Collarana, Sabrina Kirrane, Christoph Lange, Christoph Quix, Sandra Geisler, Stefan Decker, Rafiqul Haque

Gepubliceerd 2026-06-23

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Daham M. Mustafa, Diego Collarana, Sabrina Kirrane, Christoph Lange, Christoph Quix, Sandra Geisler, Stefan Decker, Rafiqul Haque

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 digitale film probeert te huren, maar de eigenaar (de Provider) en de huurder (de Consumer) spreken twee licht verschillende dialecten van "tijd".

In de wereld van digitale rechten (ODRL) worden regels geschreven als: "Je mag dit kijken vóór 31 december" of "Je mag dit kijken voor 30 dagen."

Het probleem dat dit artikel oplost, is dat de computertaal die wordt gebruikt om deze regels te schrijven, "een specifieke datum" en "een tijdsduur" behandelt alsof het hetzelfde is. Het is alsof een chefkok dezelfde lepel gebruikt om zowel "15:00 uur" (een specifiek moment) als "30 minuten" (een duur) te meten. Als je de computer vraagt: "Is 30 minuten minder dan 15:00 uur?", raakt de computer in de war. De computer weet niet of je bedoelt: "Is 30 minuten een kortere duur dan de tijd tot 15:00 uur?" of "Gebeurt 30 minuten vóór 15:00 uur?".

Vanwege deze verwarring missen computers vaak conflicten. Ze kunnen zeggen dat twee regels compatibel zijn terwijl dat eigenlijk niet zo is, of andersom.

Hier is hoe de auteurs dit hebben opgelost, met eenvoudige analogieën:

1. De "Sort Stratification" (De sokken sorteren)

De auteurs hebben een strikt sorteersysteem geïntroduceerd. Ze hebben besloten dat elke tijdgerelateerde regel getypeerd moet worden als ofwel:

Een Instantie (Een punt): Zoals een pin op een kaart (bijv. "31 december").
Een Duur (Een lengte): Zoals een liniaal (bijv. "30 dagen").

Door de computer te dwingen te weten welke "sok" wat is voordat hij ze probeert te vergelijken, verdwijnt de ambiguïteit. Een liniaal kan alleen vergeleken worden met een andere liniaal, en een pin alleen met een andere pin.

2. De "Three-Valued Verdict" (Het verkeerslicht)

Wanneer de computer controleert of een aanbod van een Provider en een verzoek van een Consumer overeenkomen, zegt hij niet alleen "Ja" of "Nee". Hij gebruikt een driestapsverdict:

Groen (Compatibel): De regels passen perfect bij elkaar.
Rood (Conflict): De regels spreken elkaar tegen.
Geel (Onbekend): De ene partij heeft niet genoeg informatie gegeven. (Bijv. de provider zegt "Je kunt 30 dagen lang kijken", maar de consument heeft niet aangegeven hoe lang hij wil kijken. We weten nog niet of ze botsen.)

3. De "Hidden Trap" (Het Cross-Operand Conflict)

Dit is de belangrijkste ontdekking van het artikel. Soms zien twee regels er op zichzelf prima uit, maar gaan ze mis wanneer ze met elkaar interageren.

De Analogie: Stel je een wateremmer voor.

Regel A (De Provider): "Je mag precies 30 liter water in deze emmer gieten."
Regel B (De Consumer): "Je mag alleen water gieten gedurende 10 minuten."

Als je naar Regel A kijkt, is het prima. Als je naar Regel B kijkt, is het ook prima. Maar als je beide tegelijk probeert uit te voeren, heb je een probleem. Je kunt niet 30 liter water gieten in 10 minuten als de stroomsnelheid van je slang een bepaalde snelheid heeft (of als de regels impliceren dat de "gebruikte tijd" niet groter kan zijn dan de "verstreken tijd").

Het systeem van de auteurs vangt deze "verborgen vallen" op, waarbij de hoeveelheid tijd die wordt gebruikt conflicteert met de lengte van de toegestane tijd, zelfs als de specifieke data er op zich goed uitzien.

4. De "Three-Layer Detective" (De lagen)

Om deze puzzels op te lossen, hebben de auteurs een detectivesysteem gebouwd dat werkt op drie moeilijkheidsgraden, zoals in een videogame:

Niveau 1 (Orde): Eenvoudige vergelijkingen. "Is 2026 vóór 2027?" of "Is 10 dagen minder dan 30 dagen?" Dit is makkelijk en snel.
Niveau 2 (Rekenkunde): Iets moeilijker. "Als ik op Dag 1 begin en 5 dagen wacht, is dat dan vóór Dag 3?" Dit vereist eenvoudige wiskunde.
Niveau 3 (Modulair/Herhalend): Het moeilijkste niveau. "Gebeurt deze gebeurtenis elke 30 dagen, en gebeurt die andere gebeurtenis elke 45 dagen? Landen ze ooit op dezelfde dag?" Dit vereist het controleren van patronen (zoals het vinden van de kleinste gemene deler in de wiskunde).

Het systeem kiest automatisch het juiste "detectieniveau" voor het probleem, zodat het de puzzel snel kan oplossen zonder vast te lopen.

5. De "Static vs. Runtime" Check

Het artikel legt ook het verschil uit tussen het controleren van regels voordat je een contract tekent en het controleren terwijl je de dienst gebruikt.

Statische Check (Onderhandeling): "Kunnen deze twee sets regels ooit samenwerken?" Als het antwoord "Nee" is (Rood Licht), teken je het contract nooit.
Runtime Check (Handhaving): "Heb je de regels daadwerkelijk overtreden tijdens het gebruik?" Zelfs als de regels samen zouden kunnen werken, kun je alsnog de regels overtreden als je de dienst te lang gebruikt.

De Kern van het Verhaal

De auteurs hebben een nieuwe, duidelijkere manier gecreëerd voor computers om tijd te begrijpen in digitale contracten. Ze hebben bewezen dat door "data" strikt te scheiden van "duur", ze conflicten kunnen vangen die eerdere systemen misten. Ze hebben dit getest met 72 verschillende scenario's (zoals een gigantisch logisch puzzelboek) en aangetoond dat hun methode perfect werkt: het vangt elk conflict en vermijdt valse alarmen.

Kortom: Ze hebben de verwarring van de computer tussen "wanneer" en "hoe lang" opgelost, waardoor de computer verborgen deal-breakers in digitale overeenkomsten kan opsporen die hij voorheen miste.

Technische Samenvatting: Sort-Gestreifieerde Semantiek voor Temporele Conflictdetectie in ODRL-policies

1. Probleemstelling

De Open Digital Rights Language (ODRL) 2.2 wordt breed geadopteerd in dataruimtes om gebruikscriteria voor digitale activa te definiëren. Deze policies bevatten frequent temporele beperkingen waarbij twee verschillende soorten operanden worden gebruikt: instanten (momenten in de tijd, bijv. dateTime) en duur (hoeveelheden tijd, bijv. elapsedTime, meteredTime, delayPeriod, timeInterval).

Het kernproblein dat wordt geïdentificeerd, is dat de vergelijkingsoperatoren van ODRL (bijv. lt, lteq, gteq) geen onderscheid maken tussen deze soorten. Bijgevolg is een operator zoals lt ambigu: het impliceert "eerder dan" voor instanten, maar "korter dan" voor duur. Dit gebrek aan sort-stratificatie leidt tot twee kritieke problemen:

Onzuivere Conflictdetectie: Bestaande formalisaties en engines behandelen temporele attributen vaak als soortloos, waardoor ongeldige vergelijkingen mogelijk zijn (bijv. een datum vergelijken met een duur) of het falen van de detectie van conflicten die voortvloeien uit de interactie tussen verschillende temporele operanden.
Gemiste Cross-Operand Conflicten: Constraints zijn vaak onderling afhankelijk. Bijvoorbeeld, meteredTime (werkelijk gebruik) kan bijvoorbeeld niet groter zijn dan elapsedTime (verstreken tijd sinds het begin van de toegang). Een policy die 30 dagen aan meteredTime biedt en een verzoek dat de totale elapsedTime beperkt tot 10 dagen, zijn afzonderlijk bevredigbaar, maar gezamenlijk onbevredigbaar. Standaard controles per operand missen dit conflict.

Bovendien richten bestaande werken (bijv. Salas et al., Bonatti et al.) zich primair op dateTime alleen, en negeren ze duur-arithmetiek, periodiciteit (timeInterval) en geordende sequenties (andSequence).

2. Methodologie

De auteurs stellen een sort-gestreifieerde denotatieve semantiek voor voor ODRL-temporele constraints. De methodologie verloopt via de volgende fasen:

2.1 Sort Stratificatie en Interval Semantiek

Het framework wijst een unieke sort toe aan elke temporele operand:

Instant Sort (Inst): Geïnterpreteerd over een lineaire tijdlijn $T$ (isomorf met $\mathbb{Q}$ ).
Duration Sort (Dur): Geïnterpreteerd over een totaal geordende, commutatieve en associatieve monoïde $D$ (isomorf met $\mathbb{Q}_{\geq 0}$ ).

Operatoren worden beperkt tot interval-operatoren (eq, lt, lteq, gt, gteq), wat garandeert dat de oplossingsverzameling voor elke constraint een orde-convexe deelverzameling (een interval) is van het domein van de operand.

Periodieke Constraints: De timeInterval-operand wordt behandeld als een periodieke verzameling instanten $Per(a, p) = \{a + kp \mid k \in \mathbb{Z}\}$ , waarbij $a$ een anker is en $p$ een periode.

2.2 Product Denotatie en Achtergrondtheorie

De betekenis van een policy wordt gedefinieerd als het product van de denotaties van de individuele constraints.

Instant Axis: dateTime en timeInterval worden gecombineerd in een enkele "instant axis" denotatie, die de intersectie representeert van een tijdsvenster en een periodiciteitspatroon.
Duration Axes: Andere operanden (elapsedTime, meteredTime, delayPeriod) vormen onafhankelijke assen.
Achtergrondtheorie ( $\Phi$ ): Om cross-operand relaties te vangen, bevat de semantiek een achtergrondtheorie $\Phi$ $Φ$ die het volgende afdwingt:
- Duurwaarden zijn niet-negatief.
- meteredTime $\le$ elapsedTime.
- delayPeriod $\le$ elapsedTime.
- Temporele ordening van toegangsgebeurtenissen.

Conflict wordt gedefinieerd als de onbevredigbaarheid van de conjunctie van twee policies ( $C_1 \land C_2$ ) onder de achtergrondtheorie $\Phi$ .

2.3 Gelaagde Beslissingsprocedure

De complexiteit van het controleren van de bevredigbaarheid varieert afhankelijk van de betrokken constraints. De auteurs classificeren het probleem in drie tiers, elk met een specifieke beslissingsprocedure:

Order Tier (Ord): Geldt wanneer constraints enkel operanden begrenzen door literalen zonder cross-operand relaties. Wordt beslist door eenvoudige grensvergelijking (EPR/Eerste-orde logica).
Difference Tier (Diff): Geldt wanneer constraints verschillen tussen instanten of cross-operand relaties bevatten (bijv. meteredTime versus elapsedTime). Wordt beslist door te controleren op negatieve cycli in een verschil-graaf (PTIME).
Modular Tier (Mod): Geldt wanneer periodieke constraints (timeInterval) betrokken zijn. Wordt beslist met behulp van Presburger-arithmetiek (deelbaarheidstests op perioden en ankers).

2.4 Driedelige Verdicten

Het framework geeft één van drie conclusies terug voor een paar policies:

Conflict: De policies zijn gezamenlijk onbevredigbaar.
Compatible (Compatibel): Er bestaat ten minste één geldige executie die aan beide voldoet.
Unknown (Onbekend): Slechts één policy beperkt een specifieke operand, waardoor de gezamenlijke bevredigbaarheid onbepaald blijft zonder verdere informatie.

Deze logica strekt zich uit naar logische operatoren (and, or, xone) en sequenties (andSequence), waarbij andSequence wordt gemodelleerd als een trace-gebaseerd constraint systeem.

3. Belangrijkste Bijdragen

Formele Semantiek: De eerste formalisering van ODRL-temporele constraints die expliciet onderscheid maakt tussen instanten en duur, waarmee de ambiguïteit van operatoren wordt opgelost.
Cross-Operand Conflictdetectie: Een mechanisme om conflicten te detecteren die voortvloeien uit de interactie tussen verschillende temporele operanden (bijv. gebruikslimieten versus verstreken tijd), wat eerdere sortloze benaderingen misten.
Beslisbaarheid Karakterisering: Een bewijs dat conflictdetectie voor de volledige set ODRL-temporele constraints (inclusclusief periodiciteit en sequenties) beslisbaar is door het probleem te reduceren tot drie specifieke, oplosbare fragmenten (Order, Difference, Modular).
Static-Runtime Bridge: Een theoretisch bewijs dat een statisch gedetecteerd conflict tijdens onderhandeling solide is (gegarandeerd standhoudt tijdens runtime), terwijl een statische compatibiliteit geen runtime-compliance garandeert (vanwege werkelijk gebruik dat limieten overschrijdt).
Benchmarking: De creatie van een benchmark met 72 conflict-detectieproblemen gecodeerd in TPTP en SMT-LIB, die diverse categorieën bestrijkt (single-operand, cross-operand, periodiek, sequenties).

4. Resultaten

De auteurs hebben het framework geëvalueerd met behulp van vier automatische reasoners: Vampire, E, Z3 en cvc5.

Volledigheid: Alle 72 benchmark-problemen werden beslist door ten minste één reasoner.
Correctheid: Geen enkele reasoner gaf een onjuist verdict terug. De overeenkomst tussen verschillende encodings (TPTP versus SMT-LIB) en solvers bevestigt dat de verdicts eigenschappen zijn van de semantiek, en niet van de encoding.
Solver Prestaties:
- E loste alle 48 "Order" tier problemen op.
- Vampire loste 62 problemen op (Order + 14 "Difference" tier problemen).
- Z3 en cvc5 losten alle 72 problemen op, inclusief de 10 "Modular" tier problemen met betrekking tot periodiciteit en trace-haalbaarheid, die SMT-capaciteiten vereisen.
Specifieke Bevindingen: De evaluatie toonde aan dat ongesorteerde interpretaties spuriële (valse) conflicten produceren, terwijl de sort-gestreifieerde aanpak correcte overeenkomsten identificeert. Het bevestigde ook dat andSequence constraints de Difference tier vereisen voor resolutie.

5. Betekenis en Claims

Het artikel claimt dat de primaire bijdrage de beslisbaarheid karakterisering en de tiered reductie is van ODRL-temporele conflictdetectie. Door instanten van duur te scheiden en hun interacties expliciet te modelleren, biedt het framework een solide basis voor policy-onderhandelingen in dataruimtes.

De auteurs benadrukken dat hun werk een bescheiden reikwijdte heeft:

Het richt zich strikt op de temporele aspecten van ODRL, en sluit niet-temporele constraints en andere regelconstructies (duties, remedies) uit.
Het vermijdt de onbeslisbare fragmenten van metrische temporele logica over dense tijd door de semantiek te beperken tot beslisbare subfragmenten (Difference Logic en Presburger Arithmetic).
Het biedt een theoretische fundering en een benchmark, in plaats van een volledige productie-grade enforcement engine, hoewel het suggereert dat de semantiek een dergelijke engine kan aansturen.

Het werk vestigt dat conflictdetectie voor de volledige set temporele operanden van ODRL niet alleen mogelijk is, maar ook efficiënt gecategoriseerd en opgelost kan worden met behulp van bestaande automatische redeneertools.