Resumen Técnico: Semántica de Estratificación de Tipos para la Detección de Conflictos Temporales en Políticas ODRL

1. Planteamiento del Problema

El Lenguaje de Derechos Digitales Abiertos (ODRL) 2.2 es ampliamente adoptado en los espacios de datos para definir políticas de uso para activos digitales. Estas políticas incluyen frecuentemente restricciones temporales que involucran dos tipos distintos de operandos: instantes (puntos en el tiempo, ej. dateTime) y duraciones (cantidades de tiempo, ej. elapsedTime, meteredTime, delayPeriod, timeInterval).

El problema central identificado es que los operadores de comparación de ODRL (ej. lt, lteq, gteq) no distinguen entre estos tipos. En consecuencia, un operador como lt es ambiguo: implica "anterior a" para instantes, pero "más corto que" para duraciones. Esta falta de estratificación de tipos conduce a dos problemas críticos:

1. Detección de Conflictos No Sólida: Las formalizaciones y motores existentes a menudo tratan los atributos temporales como carentes de tipo, permitiendo comparaciones inválidas (ej. comparar una fecha con una duración) o fallando en la detección de conflictos derivados de la interacción entre diferentes operandos temporales.
2. Conflictos de Operandos Cruzados Perdidos: Las restricciones suelen ser interdependientes. Por ejemplo, meteredTime (uso real) no puede exceder a elapsedTime (tiempo transcurrido desde que comenzó el acceso). Una política que ofrece 30 días de uso medido (meteredTime) y una solicitud que limita el tiempo transcurrido total a 10 días son, individualmente, satisfacibles, pero conjuntamente insatisfacibles. Las verificaciones por operando estándar pasan por alto este conflicto.

Además, trabajos existentes (ej. Salas et al., Bonatti et al.) se centran principalmente en dateTime por sí solo, ignorando la aritmética de duraciones, la recurrencia (timeInterval) y las secuencias ordenadas (andSequence).

2. Metodología

Los autores proponen una semántica denotacional con estratificación de tipos para las restricciones temporales de ODRL. La metodología avanza a través de las siguientes etapas:

2.1 Estratificación de Tipos y Semántica de Intervalos

El marco asigna un tipo único a cada operando temporal:

• Tipo de Instante (Inst): Interpretado sobre una línea de tiempo lineal $T$ (isomorfa a $\mathbb{Q}$).
• Tipo de Duración (Dur): Interpretado sobre un monoide conmutativo cancelativo totalmente ordenado $D$ (isomorfo a $\mathbb{Q}_{\geq 0}$).

Los operadores se restringen a operadores de intervalo (eq, lt, lteq, gt, gteq), asegurando que el conjunto solución para cualquier restricción sea un subconjunto convexo de orden (un intervalo) del dominio del operando.

• Restricciones Periódicas: El operando timeInterval se trata como un conjunto periódico de instantes $Per(a, p) = \{a + kp \mid k \in \mathbb{Z}\}$, donde $a$ es un ancla y $p$ es un periodo.

2.2 Denotación de Producto y Teoría de Fondo

El significado de una política se define como el producto de las denotaciones de sus restricciones individuales.

• Eje de Instantes: dateTime y timeInterval se combinan en una única denotación de "eje de instantes", que representa la intersección de una ventana de tiempo y un patrón de recurrencia.
• Ejes de Duración: Otros operandos (elapsedTime, meteredTime, delayPeriod) forman ejes independientes.
• Teoría de Fondo ($\Phi$): Para capturar las relaciones entre operandos, la semántica incluye una teoría de fondo $\Phi$ que impone:
  • Las duraciones son no negativas.
  • meteredTime $\le$ elapsedTime.
  • delayPeriod $\le$ elapsedTime.
  • Orden temporal de los eventos de acceso.

El conflicto se define como la insatisfacibilidad de la conjunción de dos políticas ($C_1 \land C_2$) bajo la teoría de fondo $\Phi$.

2.3 Procedimiento de Decisión por Niveles

La complejidad de verificar la satisfacibilidad varía según las restricciones involucradas. Los autores clasifican el problema en tres niveles (tiers), cada uno con un procedimiento de decisión específico:

1. Nivel de Orden (Ord): Se aplica cuando las restricciones solo limitan los operandos mediante literales sin relaciones entre operandos. Se decide mediante la comparación de límites simples (EPR/lógica de primer orden).
2. Nivel de Diferencia (Diff): Se aplica cuando las restricciones involucran diferencias entre instantes o relaciones entre operandos (ej. meteredTime vs. elapsedTime). Se decide mediante la verificación de ciclos negativos en un grafo de diferencias (PTIME).
3. Nivel Modular (Mod): Se aplica cuando hay restricciones periódicas (timeInterval) involucradas. Se decide utilizando aritmética de Presburger (pruebas de divisibilidad sobre periodos y anclas).

2.4 Veredictos de Tres Valores

El marco devuelve uno de tres veredictos para un par de políticas:

• Conflicto: Las políticas son conjuntamente insatisfacibles.
• Compatible: Existe al menos una ejecución válida que satisface ambas.
• Desconocido: Solo una política restringe un operando específico, dejando la satisfacibilidad conjunta indeterminada sin más información.

Esta lógica se extiende a los operadores lógicos (and, or, xone) y secuencias (andSequence), donde andSequence se modela como un sistema de restricciones basado en trazas.

3. Contribuciones Clave

• Semántica Formal: La primera formalización de las restricciones temporales de ODRL que distingue explícitamente entre instantes y duraciones, resolviendo la ambigüedad de los operadores.
• Detección de Conflictos de Operandos Cruzados: Un mecanismo para detectar conflictos que surgen de la interacción de diferentes operandos temporales (ej. límites de uso frente a tiempo transcurrido), que los enfoques anteriores sin estratificación de tipos pasaron por alto.
• Caracterización de la Decidibilidad: Una prueba de que la detección de conflictos para el conjunto completo de restricciones temporales de ODRL (incluyendo recurrencia y secuencias) es decidible mediante la reducción del problema a tres fragmentos específicos y resolubles (Orden, Diferencia, Modular).
• Puente Estático-Runtime: Una prueba teórica de que un conflicto estático detectado en el momento de la negociación es sólido (garantizado que se mantendrá en tiempo de ejecución), mientras que una compatibilidad estática no garantiza el cumplimiento en tiempo de ejecución (debido a que el uso real puede exceder los topes).
• Benchmarking: La creación de un banco de pruebas de 72 problemas de detección de conflictos codificados en TPTP y SMT-LIB, que cubren diversas categorías (un solo operando, operandos cruzados, periodicidad, secuencias).

4. Resultados

Los autores evaluaron el marco utilizando cuatro razonadores automatizados: Vampire, E, Z3 y cvc5.

• Completitud: Todos los 72 problemas del banco de pruebas fueron decididos por al menos un razonador.
• Corrección: Ningún razonador devolvió un veredicto incorrecto. El acuerdo entre las diferentes codificaciones (TPTP vs. SMT-LIB) y los solvers confirma que los veredictos son propiedades de la semántica, no de la codificación.
• Rendimiento de los Solvers:
  • E resolvió todos los 48 problemas del nivel "Orden".
  • Vampire resolvió 62 problemas (Orden + 14 problemas del nivel "Diferencia").
  • Z3 y cvc5 resolvieron los 72 problemas, incluyendo los 10 problemas del nivel "Modular" que involucran periodicidad y factibilidad de traza, los cuales requieren capacidades de SMT.
• Hallazgos Específicos: La evaluación demostró que las lecturas sin estratificación de tipos producen conflictos espurios, mientras que el enfoque con estratificación de tipos identifica correctamente los acuerdos válidos. También confirmó que las restricciones de andSequence requieren el nivel de Diferencia para su resolución.

5. Significado y Reivindicaciones

El artículo afirma que su contribución principal es la caracterización de la decidibilidad y la reducción por niveles de la detección de conflictos temporales de ODRL. Al separar los instantes de las duraciones y modelar explícitamente sus interacciones, el marco proporciona una base sólida para la negociación de políticas en los espacios de datos.

Los autores enfatizan que su trabajo es de alcance modesto:

• Se centra estrictamente en los aspectos temporales de ODRL, excluyendo restricciones no temporales y otras construcciones de reglas (deberes, remedios).
• Evita los fragmentos indecidibles de la lógica temporal métrica sobre tiempo denso al restringir la semántica a subfragmentos decidibles (Lógica de Diferencia y Aritmética de Presburger).
• Proporciona una base teórica y un banco de pruebas, en lugar de un motor de ejecución completo para producción, aunque sugiere que la semántica podría impulsar tal motor.

Este trabajo establece que la detección de conflictos para el conjunto completo de operandos temporales de ODRL no solo es posible, sino que puede categorizarse y resolverse eficientemente utilizando herramientas de razonamiento automatizado existentes.