💻 computer science

Sort-Stratified Semantics for Temporal Conflict Detection in ODRL Policies

Cet article traite de l'invalidité de la détection de conflits temporels dans les politiques ODRL causée par l'ambiguïté des opérateurs de comparaison entre instants et durées en introduisant une sémantique stratifiée par types qui typifie les opérandes, réduit la vérification de conflit à une comparaison d'intervalles avec un verdict à trois valeurs, et prouve sa décidabilité et sa correction par des évaluations statiques et dynamiques.

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

Publié 2026-06-23

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

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

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous essayez de louer un film numérique, mais que le propriétaire (le Fournisseur) et le locataire (le Consommateur) parlent deux dialectes légèrement différents du « temps ».

Dans le monde des droits numériques (ODRL), les règles sont écrites comme : « Vous pouvez regarder ceci avant le 31 décembre » ou « Vous pouvez regarder ceci pendant 30 jours ».

Le problème que ce document résout est que le langage informatique utilisé pour écrire ces règles traite « une date spécifique » et « une durée » comme s'il s'agissait de la même chose. C'est comme un chef qui utiliserait la même cuillère pour mesurer à la fois « 15h00 » (un moment précis) et « 30 minutes » (une durée). Si vous demandez à l'ordinateur : « Est-ce que 30 minutes est inférieur à 15h00 ? », il est confus. Il ne sait pas si vous voulez dire « Est-ce qu'une durée de 30 minutes est plus courte que le temps restant jusqu'à 15h00 ? » ou « Est-ce que 30 minutes arrive avant 15h00 ? ».

À cause de cette confusion, les ordinateurs peuvent manquer des conflits. Ils peuvent dire que deux règles sont compatibles alors qu'elles ne le sont pas, ou inversement.

Voici comment les auteurs ont résolu cela, en utilisant des analogies simples :

1. La « Stratification par Tri » (Trier les chaussettes)

Les auteurs ont introduit un système de tri strict. Ils ont décidé que chaque règle liée au temps doit être typée soit comme :

Un Instant (Un Point) : Comme une épingle sur une carte (ex. : « 31 décembre »).
Une Durée (Une Longueur) : Comme une règle (ex. : « 30 jours »).

En forçant l'ordinateur à savoir quel « type de chaussette » est quoi avant d'essayer de les comparer, l'ambiguïté disparaît. Une règle ne peut être comparée qu'à une autre règle, et une épingle ne peut être comparée qu'à une autre épingle.

2. Le « Verdict à Trois Valeurs » (Le Feu de Signalisation)

Lorsque l'ordinateur vérifie si l'offre d'un Fournisseur et la requête d'un Consommateur correspondent, il ne se contente pas de dire « Oui » ou « Non ». Il utilise un feu de signalisation à trois voies :

Vert (Compatible) : Les règles s'ajustent parfaitement.
Rouge (Conflit) : Les règles se contredisent.
Jaune (Inconnu) : Un côté n'a pas fourni assez d'informations. (ex. : Le fournisseur dit « Vous pouvez regarder pendant 30 jours », mais le consommateur n'a pas précisé combien de temps il souhaite regarder. Nous ne savons pas encore s'ils entrent en conflit.)

3. Le « Piège Caché » (Le Conflit de l'Opérande Croisé)

C'est la découverte la plus importante du document. Parfois, deux règles semblent correctes individuellement, mais elles se brisent lorsqu'on observe leur interaction.

L'analogie : Imaginez un seau d'eau.

Règle A (Le Fournisseur) : « Vous pouvez verser exactement 30 litres d'eau dans ce seau. »
Règle B (Le Consommateur) : « Vous pouvez seulement verser de l'eau pendant 10 minutes . »

Si vous regardez la Règle A seule, elle est correcte. Si vous regardez la Règle B seule, elle est correcte. Mais si vous essayez de faire les deux en même temps, vous avez un problème. Vous ne pouvez pas verser 30 litres en 10 minutes si votre tuyau a un certain débit (ou si les règles impliquent que le « temps passé à utiliser » ne peut pas excéder le « temps écoulé »).

Le système des auteurs détecte ces « pièges cachés » où la quantité de temps utilisée entre en conflit avec la longueur de temps autorisée, même si les dates spécifiques semblent correctes.

4. Le « Détective à Trois Niveaux » (Les Échelons)

Pour résoudre ces énigmes, les auteurs ont construit un système de détection qui fonctionne sur trois niveaux de difficulté, comme un jeu vidéo :

Niveau 1 (Ordre) : Comparaisons simples. « Est-ce que 2026 est avant 2027 ? » ou « Est-ce que 10 jours est moins que 30 jours ? ». C'est facile et rapide.
Niveau 2 (Arithmétique) : Un peu plus difficile. « Si je commence au Jour 1 et que j'attends 5 jours, est-ce avant le Jour 3 ? ». Cela nécessite des calculs simples.
Niveau 3 (Modulaire/Répétitif) : Le niveau le plus difficile. « Cet événement se produit-il tous les 30 jours, et cet événement se produit-il tous les 45 jours ? Tombent-ils jamais le même jour ? ». Cela nécessite de vérifier des motifs (comme trouver le dénominateur commun en mathématiques).

Le système choisit automatiquement le bon « niveau de détective » pour le problème, garantissant qu'il puisse le résoudre rapidement sans rester bloqué.

5. La Vérification « Statique vs Exécution »

Le document explique également la différence entre vérifier les règles avant de signer un contrat et vérifier les règles pendant l'utilisation du service.

Vérification Statique (Négociation) : « Ces deux ensembles de règles peuvent-ils un jour fonctionner ensemble ? » Si la réponse est « Non » (Feu Rouge), on ne signe jamais le contrat.
Vérification à l'Exécution (Application) : « Avez-vous réellement enfreint les règles pendant l'utilisation ? » Même si les règles pourraient fonctionner ensemble, vous pourriez quand même les transgresser si vous utilisez le service trop longtemps.

L'essentiel

Les auteurs ont créé une nouvelle manière plus claire pour les ordinateurs de comprendre le temps dans les contrats numériques. Ils ont prouvé qu'en séparant strictement les « dates » des « durées », ils peuvent détecter des conflits que les systèmes précédents ignoraient. Ils ont testé cela avec 72 scénarios différents (comme un immense livre de logique) et ont montré que leur méthode fonctionne parfaitement, capturant chaque conflit et évitant les fausses alertes.

En bref : Ils ont corrigé la confusion de l'ordinateur entre « quand » et « combien de temps », lui permettant de repérer les points de rupture cachés dans les accords numériques qu'il ne parvenait auparavant pas à voir.

Résumé technique : Sémantique à stratification de types pour la détection de conflits temporels dans les politiques ODRL

1. Énoncé du problème

L'ODRL 2.2 (Open Digital Rights Language) est largement adopté dans les espaces de données pour définir les politiques d'usage des actifs numériques. Ces politiques incluent fréquemment des contraintes temporelles impliquant deux sortes d'opérandes distinctes : les instants (points dans le temps, ex: dateTime) et les durées (quantités de temps, ex: elapsedTime, meteredTime, delayPeriod, timeInterval).

Le problème central identifié est que les opérateurs de comparaison d'ODRL (ex: lt, lteq, gteq) ne distinguent pas ces types. Par conséquent, un opérateur comme lt est ambigu : il implique « antérieur à » pour les instants mais « plus court que » pour les durations. Ce manque de stratification des types entraîne deux problèmes critiques :

Détection de conflits non saine : Les formalisations et moteurs existants traitent souvent les attributs temporels comme étant sans type, permettant des comparaisons invalides (ex: comparer une date à une durée) ou échouant à détecter des conflits découlant de l'interaction entre différents opérandes temporels.
Conflits entre opérandes manqués : Les contraintes sont souvent interdépendantes. Par exemple, le meteredTime (usage réel) ne peut excéder l'elapsedTime (temps écoulé depuis le début de l'accès). Une politique offrant 30 jours d'usage mesuré et une requête limitant le temps écoulé total à 10 jours sont individuellement satisfaisables mais conjointement insatisfaisables. Les vérifications par opérande standard manquent ce conflit.

De plus, les travaux existants (ex: Salas et al., Bonatti et al.) se concentrent principalement sur dateTime seul, ignorant l'arithmétique des durées, la récurrence (timeInterval) et les séquences ordonnées (andSequence).

2. Méthodologie

Les auteurs proposent une sémantique dénotationnelle à stratification de types pour les contraintes temporelles d'ODRL. La méthodologie suit les étapes suivantes :

2.1 Stratification des types et sémantique d'intervalle

Le cadre assigne un type unique à chaque opérande temporel :

Type Instant (Inst) : Interprété sur une chronologie linéaire $T$ (isomorphe à $\mathbb{Q}$ ).
Type Durée (Dur) : Interprété sur un monoïde commutatif cancellatif totalement ordonné $D$ (isomorphe à $\mathbb{Q}_{\geq 0}$ ).
Les opérateurs sont restreints aux opérateurs d'intervalle (eq, lt, lteq, gt, gteq), garantissant que l'ensemble des solutions pour toute contrainte est un sous-ensemble d'ordre convexe (un intervalle) du domaine de l'opérande.
Contraintes périodiques : L'opérande timeInterval est traité comme un ensemble périodique d'instants $Per(a, p) = \{a + kp \mid k \in \mathbb{Z}\}$ , où $a$ est une ancre et $p$ une période.

2.2 Dénotation produit et théorie de fond

La signification d'une politique est définie comme le produit des dénotations de ses contraintes individuelles.

Axe des instants : dateTime et timeInterval sont combinés en une dénotation unique d'« axe d'instants », représentant l'intersection d'une fenêtre temporelle et d'un motif de récurrence.
Axes de durée : Les autres opérandes (elapsedTime, meteredTime, delayPeriod) forment des axes indépendants.
Théorie de fond ( $\Phi$ ) : Pour capturer les relations entre opérandes, la sémantique inclut une théorie de fond $\Phi$ $Φ$ imposant :
- Les durées sont non négatives.
- meteredTime $\le$ elapsedTime.
- delayPeriod $\le$ elapsedTime.
- L'ordre temporel des événements d'accès.
  Le conflit est défini comme l'insatisfaisabilité de la conjonction de deux politiques ( $C_1 \land C_2$ ) sous la théorie de fond $\Phi$ .

2.3 Procédure de décision à plusieurs niveaux

La complexité de la vérification de la satisfaisabilité varie selon les contraintes impliquées. Les auteurs classent le problème en trois niveaux (tiers), chacun ayant une procédure de décision spécifique :

Niveau Ordre (Ord) : S'applique lorsque les contraintes limitent uniquement les opérandes par des littéraux sans relations entre opérandes. Décidé par une simple comparaison de bornes (EPR/logique du premier ordre).
Niveau Différence (Diff) : S'applique lorsque les contraintes impliquent des différences entre instants ou des relations entre opérandes (ex: meteredTime vs elapsedTime). Décidé en vérifiant l'absence de cycles négatifs dans un graphe de différence (PTIME).
Niveau Modulaire (Mod) : S'applique lorsque des contraintes périodiques (timeInterval) sont impliquées. Décidé en utilisant l'arithmétique de Presburger (tests de divisibilité sur les périodes et les ancres).

2.4 Verdicts à trois valeurs

Le cadre retourne l'un des trois verdicts pour une paire de politiques :

Conflit : Les politiques sont conjointement insatisfaisables.
Compatible : Il existe au moins une exécution valide satisfaisant les deux.
Inconnu : Une seule politique contraint un opérande spécifique, laissant la satisfaisabilité conjointe indéterminée sans informations supplémentaires.

Cette logique s'étend aux opérateurs logiques (and, or, xone) et aux séquences (andSequence), où andSequence est modélisé comme un système de contraintes basé sur les traces.

3. Contributions clés

Sémantique formelle : La première formalisation des contraintes temporelles d'ODRL qui distingue explicitement les instants des durées, résolvant l'ambiguïté des opérateurs.
Détection de conflits entre opérandes : Un mécanisme pour détecter les conflits découlant de l'interaction de différents opérandes temporels (ex: limites d'usage vs temps écoulé), que les approches sans type précédentes ignoraient.
Caractérisation de la décidabilité : Une preuve que la détection de conflits pour l'ensemble complet des contraintes temporelles d'ODRL (incluant la récurrence et les séquences) est décidable en réduisant le problème à trois fragments spécifiques et solubles (Ordre, Différence, Modulaire).
Pont Statique-Exécution : Une preuve théorique qu'un conflit statique détecté lors de la négociation est sain (garanti de tenir au moment de l'exécution), tandis qu'une compatibilité statique ne garantit pas la conformité à l'exécution (en raison d'un usage réel dépassant les plafonds).
Évaluation comparative (Benchmarking) : La création d'un benchmark de 72 problèmes de détection de conflits encodés en TPTP et SMT-LIB, couvrant diverses catégories (opérande unique, entre opérandes, périodicité, séquences).

4. Résultats

Les auteurs ont évalué le cadre en utilisant quatre raisonneurs automatisés : Vampire, E, Z3 et cvc5.

Complétude : Les 72 problèmes du benchmark ont été décidés par au moins un raisonneur.
Correction : Aucun raisonneur n'a retourné un verdict incorrect. L'accord entre les différents encodages (TPTP vs SMT-LIB) et les solveurs confirme que les verdicts sont des propriétés de la sémantique, et non de l'encodage.
Performance des solveurs :
- E a résolu tous les 48 problèmes du niveau "Ordre".
- Vampire a résolu 62 problèmes (Ordre + 14 problèmes du niveau "Différence").
- Z3 et cvc5 ont résolu les 72 problèmes, y compris les 10 problèmes du niveau "Modulaire" impliquant la périodicité et la faisabilité des traces, qui nécessitent des capacités SMT.
Constatations spécifiques : L'évaluation a démontré que les lectures sans distinction de type produisent des conflits spécieux, tandis que l'approche à stratification de types identifie correctement les accords valides. Elle a également confirmé que les contraintes andSequence nécessitent le niveau Différence pour la résolution.

5. Signification et affirmations

L'article affirme que sa contribution principale est la caractérisation de la décidabilité et la réduction par niveaux de la détection de conflits temporels d'ODRL. En séparant les instants des durations et en modélisant explicitement leurs interactions, le cadre fournit une base saine pour la négociation de politiques dans les espaces de données.

Les auteurs soulignent que leur travail est de portée modeste :

Il se concentre strictement sur les aspects temporels d'ODRL, excluant les contraintes non temporelles et les autres constructions de règles (devoirs, remèdes).
Il évite les fragments indécidables de la logique temporelle métrique sur temps dense en restreignant la sémantique à des sous-fragments décidables (Logique de Différence et Arithmétique de Presburger).
Il fournit une fondation théorique et un benchmark, plutôt qu'un moteur d'application complet, bien qu'il suggère que la sémantique pourrait piloter un tel moteur.

Ce travail établit que la détection de conflits pour l'ensemble complet des opérandes temporels d'ODRL est non seulement possible, mais peut être efficacement catégorisée et résolue à l'aide d'outils de raisonnement automatisé existants.