Resumo Técnico: Semântica Estratificada por Tipos para Detecção de Conflitos Temporais em Políticas ODRL

1. Definição do Problema

O ODRL 2.2 é amplamente adotado em espaços de dados para definir políticas de uso de ativos digitais. Essas políticas frequentemente incluem restrições temporais envolvendo dois tipos distintos de operandos: instantes (pontos no tempo, ex: dateTime) e durações (quantidades de tempo, ex: elapsedTime, meteredTime, delayPeriod, timeInterval).

O problema central identificado é que os operadores de comparação do ODRL (ex: lt, lteq, gteq) não distinguem entre esses tipos. Consequentemente, um operador como lt é ambíguo: implica "anterior a" para instantes, mas "mais curto que" para durações. Essa falta de estratificação de tipos leva a dois problemas críticos:

1. Detecção de Conflito Não Confiável (Unsound): As formalizações e mecanismos existentes frequentemente tratam atributos temporais como sem tipo, permitindo comparações inválidas (ex: comparar uma data com uma duração) ou falhando em detectar conflitos decorrentes da interação entre diferentes operandos temporais.
2. Conflitos Perdidos entre Diferentes Operandos: As restrições são frequentemente interdependentes. Por exemplo, o meteredTime (uso real) não pode exceder o elapsedTime (tempo decorrido desde o início do acesso). Uma política que oferece 30 dias de uso medido e uma requisição que limita o tempo decorrido total a 10 dias são, individualmente, satisfatórias, mas conjuntamente insatisfatórias. Verificações por operando padrão perdem esse conflito.

Além disso, trabalhos existentes (ex: Salas et al., Bonatti et al.) focam primariamente em dateTime isoladamente, ignorando aritmética de duração, recorrência (timeInterval) e sequências ordenadas (andSequence).

2. Metodologia

Os autores propõem uma semântica denotacional estratificada por tipos para as restrições temporais do ODRL. A metodologia avança através das seguintes etapas:

2.1 Estratificação de Tipos e Semântica de Intervalo

O framework atribui um tipo único a cada operando temporal:

• Tipo de Instante (Inst): Interpretado sobre uma linha do tempo linear $T$ (isomorfa a $\mathbb{Q}$).
• Tipo de Duração (Dur): Interpretado sobre um monoide comutativo cancelativo totalmente ordenado $D$ (isomorfo a $\mathbb{Q}_{\geq 0}$).

Os operadores são restritos a operadores de intervalo (eq, lt, lteq, gt, gteq), garantindo que o conjunto solução para qualquer restrição seja um subconjunto ordem-convexo (um intervalo) do domínio do operando.

• Restrições Periódicas: O operando timeInterval é tratado como um conjunto periódico de instantes $Per(a, p) = \{a + kp \mid k \in \mathbb{Z}\}$, onde $a$ é uma âncora e $p$ é um período.

2.2 Denotação de Produto e Teoria de Fundo

O significado de uma política é definido como o produto das denotações de suas restrições individuais.

• Eixo de Instantes: dateTime e timeInterval são combinados em uma única denotação de "eixo de instantes", representando a interseção de uma janela de tempo e um padrão de recorrência.
• Eixos de Duração: Outros operandos (elapsedTime, meteredTime, delayPeriod) formam eixos independentes.
• Teoria de Fundo ($\Phi$): Para capturar relações entre operandos, a semântica inclui uma teoria de fundo $\Phi$ que impõe:
  • Durações são não-negativas.
  • meteredTime $\le$ elapsedTime.
  • delayPeriod $\le$ elapsedTime.
  • Ordenação temporal de eventos de acesso.

O conflito é definido como a insatisfatibilidade da conjunção de duas políticas ($C_1 \land C_2$) sob a teoria de fundo $\Phi$.

2.3 Procedimento de Decisão em Camadas

A complexidade da verificação de satisfatibilidade varia conforme as restrições envolvidas. Os autores classificam o problema em três camadas (tiers), cada uma com um procedimento de decisão específico:

1. Camada de Ordem (Ord): Aplica-se quando as restrições apenas limitam operandos por literais sem relações entre operandos. Decidida por comparação simples de limites (EPR/lógica de primeira ordem).
2. Camada de Diferença (Diff): Aplica-se quando as restrições envolvem diferenças entre instantes ou relações entre operandos (ex: meteredTime vs. elapsedTime). Decidida pela verificação de ciclos negativos em um grafo de diferença (PTIME).
3. Camada Modular (Mod): Aplica-se quando restrições periódicas (timeInterval) estão envolvidas. Decidida usando aritmética de Presburger (testes de divisibilidade em períodos e âncoras).

2.4 Veredictos de Três Valores

O framework retorna um de três veredictos para um par de políticas:

• Conflito: As políticas são conjuntamente insatisfatórias.
• Compatível: Existe pelo menos uma execução válida que satisfaz ambas.
• Desconhecido: Apenas uma política restringe um operando específico, deixando a satisfatibilidade conjunta indeterminada sem informações adicionais.

Esta lógica se estende a operadores lógicos (and, or, xone) e sequências (andSequence), onde andSequence é modelado como um sistema de restrição baseado em traço.

3. Principais Contribuições

• Semântica Formal: A primeira formalização das restrições temporais do ODRL que distingue explicitamente entre instantes e durações, resolvendo a ambiguidade dos operadores.
• Detecção de Conflito entre Diferentes Operandos: Um mecanismo para detectar conflitos decorrentes da interação de diferentes operandos temporais (ex: limites de uso vs. tempo decorrido), que abordagens anteriores sem distinção de tipos perderam.
• Caracterização de Decidibilidade: Uma prova de que a detecção de conflitos para o conjunto completo de restrições temporais do ODRL (incluindo recorrência e sequências) é decidível ao reduzir o problema a três fragmentos específicos e solucionáveis (Ordem, Diferença, Modular).
• Ponte Estático-Tempo de Execução: Uma prova teórica de que um conflito estático detectado no momento da negociação é sólido (garantido que se manterá em tempo de execução), enquanto uma compatibilidade estática não garante conformidade em tempo de execução (devido ao uso real exceder os limites).
• Benchmarking: A criação de um benchmark de 72 problemas de detecção de conflito codificados em TPTP e SMT-LIB, cobrindo várias categorias (operando único, entre operandos, periódico, sequências).

4. Resultados

Os autores avaliaram o framework utilizando quatro raciocinadores automatizados: Vampire, E, Z3 e cvc5.

• Completude: Todos os 72 problemas do benchmark foram decididos por pelo menos um raciocinador.
• Corretude: Nenhum raciocinador retornou um veredito incorreto. O acordo entre diferentes codificações (TPTP vs. SMT-LIB) e solvers confirma que os veredictos são propriedades da semântica, não da codificação.
• Desempenho dos Solvers:
  • E resolveu todos os 48 problemas da camada "Ordem".
  • Vampire resolveu 62 problemas (Ordem + 14 problemas da camada "Diferença").
  • Z3 e cvc5 resolveram todos os 72 problemas, incluindo os 10 problemas da camada "Modular" que envolvem periodicidade e viabilidade de traço, que exigem capacidades de SMT.
• Descobertas Específicas: A avaliação demonstrou que leituras sem distinção de tipos produzem conflitos espúrios, enquanto a abordagem estratificada por tipos identifica corretamente acordos válidos. Também confirmou que restrições andSequence requerem a camada de Diferença para resolução.

5. Significância e Alegações

O artigo alega que sua principal contribuição é a caracterização de decidibilidade e a redução em camadas da detecção de conflitos temporais do ODRL. Ao separar instantes de durações e modelar explicitamente suas interações, o framework fornece uma base sólida para a negociação de políticas em espaços de dados.

Os autores enfatizam que seu trabalho é de escopo modesto:

• Foca estritamente nos aspectos temporais do ODRL, excluindo restrições não temporais e outras construções de regras (deveres, remédios).
• Evita os fragmentos indecidíveis da lógica temporal métrica sobre tempo denso ao restringir a semântica a subfragmentos decidíveis (Lógica de Diferença e Aritmética de Presburger).
• Fornece uma fundação teórica e um benchmark, em vez de um motor de aplicação completo para produção, embora sugira que a semântica possa impulsionar tal motor.

O trabalho estabelece que a detecção de conflitos para o conjunto completo de operandos temporais do ODRL não é apenas possível, mas pode ser categorizada e resolvida eficientemente usando ferramentas de raciocínio automatizado existentes.