Sort-Stratified Semantics for Temporal Conflict Detection in ODRL Policies
2026-06-22 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors explain that in ODRL, a language for describing digital rights, time-related rules mix two different kinds of measurements: specific time points and durations. Because the language uses the same comparison operators for both, it can make mistakes when checking if policies conflict. They fix this by clearly separating time points from durations and treating each constraint as a time interval, which helps identify conflicts more accurately. They also show that their method works correctly and test it using standard tools for logic and verification.
ODRLtemporal constraintstime pointsdurationsconflict detectionsort stratificationinterval comparisondecidabilityTPTPSMT-LIB
Authors
Daham M. Mustafa, Diego Collarana, Sabrina Kirrane, Christoph Lange, Christoph Quix, Sandra Geisler, Stefan Decker, Rafiqul Haque
Abstract
In the Open Digital Rights Language (ODRL), temporal constraints range over two sorts, instants and durations, but the comparison operators do not distinguish them. The same operator thus means "earlier instant" or "shorter duration," leaving conflict detection between two policies unsound. We resolve this by sort stratification: each temporal operand is typed to one of two ordered domains, points in time or amounts of time. Each constraint then denotes an interval, and conflict reduces to interval comparison under a three-valued verdict (Conflict, Compatible, Unknown). We characterise the check's decidability across a static and a runtime fragment, prove it sound, and evaluate it on a benchmark of policy problems compiled to TPTP and SMT-LIB, available as an artefact.