为ODRL策略冲突检测构建基于知识库的语义框架,解决跨数据空间互操作难题。
Denotational Semantics for ODRL: Knowledge-Based Constraint Conflict Detection
- 将ODRL约束映射到满足它的知识库概念集,实现冲突检测的精确化
- 在不完整知识下仍能保证结果正确,154个测试用例全部通过验证
- 适用于分类、整体部分和命名三类实际语义场景,特别适合合规性系统
ODRL的六种集合运算符(isA, isPartOf, hasPart, isAnyOf, isAllOf, isNoneOf)依赖于外部领域知识,而W3C规范未明确说明。缺乏该知识时,所有跨数据空间策略比较默认为未知。本文提出一种记号语义,将每个ODRL约束映射为满足它的知识库概念集合。冲突检测转化为三值判断下的记号交集——冲突、兼容或未知,且在知识不完整时仍具可靠性。框架涵盖所有三种ODRL组合模式(and, or, xone)和实践中出现的三类语义域:分类(类包含)、整体部分(整体-部分包含)、命名(身份)。针对跨数据空间互操作,定义了保序对齐,并证明两项保障:冲突在不同知识库标准间保持不变;未映射概念退化为未知而非错误冲突。运行时保真定理确保设计时结论适用于所有执行上下文。编码保持在可判定的一阶逻辑EPR片段内。我们在六个知识库家族(GeoNames、ISO 3166、W3C DPV、GDPR派生分类、BCP 47、ISO 639-3)和四种结构化知识库上进行154个基准测试,覆盖对抗性边缘案例。Vampire自动推理机与Z3 SMT求解器对所有154个结论达成一致。关键发现:排他组合(xone)需要比合取或析取更强的知识库公理;开放世界语义即使存在单一正证据也阻止排他性成立。
原文摘要 · Abstract (English)
ODRL's six set-based operators -- isA, isPartOf, hasPart, isAnyOf, isAllOf, isNoneOf -- depend on external domain knowledge that the W3C specification leaves unspecified. Without it, every cross-dataspace policy comparison defaults to Unknown. We present a denotational semantics that maps each ODRL constraint to the set of knowledge-base concepts satisfying it. Conflict detection reduces to denotation intersection under a three-valued verdict -- Conflict, Compatible, or Unknown -- that is sound under incomplete knowledge. The framework covers all three ODRL composition modes (and, or, xone) and all three semantic domains arising in practice: taxonomic (class subsumption), mereological (part-whole containment), and nominal (identity). For cross-dataspace interoperability, we define order-preserving alignments between knowledge bases and prove two guarantees: conflicts are preserved across different KB standards, and unmapped concepts degrade gracefully to Unknown -- never to false conflicts. A runtime soundness theorem ensures that design-time verdicts hold for all execution contexts. The encoding stays within the decidable EPR fragment of first-order logic. We validate it with 154 benchmarks across six knowledge base families (GeoNames, ISO 3166, W3C DPV, a GDPR-derived taxonomy, BCP 47, and ISO 639-3) and four structural KBs targeting adversarial edge cases. Both the Vampire theorem prover and the Z3 SMT solver agree on all 154 verdicts. A key finding is that exclusive composition (xone) requires strictly stronger KB axioms than conjunction or disjunction: open-world semantics blocks exclusivity even when positive evidence appears to satisfy exactly one branch.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。