研究递归SHACL文档的逻辑蕴含关系，发现其在多数语义下不可判定，但在稳健语义下可高效求解。
Static Analysis of Recursive SHACL
- 将递归SHACL文档转化为混合μ演算，建立其与固定点模态逻辑的联系
- 在稳定模型语义下蕴含关系不可判定，在有界模型语义下为单指数时间可判定
- 提出最优自动机决策算法，适用于验证SHACL文档间的逻辑包含性
SHACL（形状约束语言）通过形状表达式对RDF数据施加约束，其核心功能是验证数据图是否符合给定的SHACL文档。然而，目前尚无静态分析服务用于比较文档。本文研究：判断所有满足一个SHACL文档的图是否也满足另一个。不同于以往仅考虑形状表达式的蕴含关系，本文涵盖包含递归形状定义和目标的完整文档。我们证明，在支持模型和稳定模型语义下，蕴含关系（即包含）即使在使用描述逻辑ALCIO的形状表达式片段中也是不可判定的。然而在有界模型语义下，出人意料地存在单指数时间可判定性。关键技术贡献是将有界模型下的SHACL翻译为完整的混合μ演算，揭示了有界模型与固定点模态逻辑的新关联，并构建了最坏情况最优的基于自动机的决策过程。
原文摘要 · Abstract (English)
SHACL (Shapes Constraint Language) expresses constraints on RDF data by means of so-called shapes. Its central service is validation: verifying whether a data graph complies with a SHACL document. But so far, there are no static analysis services to compare documents. In this paper, we study the following problem: decide whether all graphs that validate one SHACL document also validate another. Unlike previous works that have considered the implication of shape expressions only, we consider documents comprising (recursive) shape definitions and targets. We show that implication (a.k.a. containment) is undecidable under the supported and the stable model semantics, even for the fragment that uses the description logic ALCIO for shape expressions. Under the well-founded semantics, in surprising contrast, it is decidable in single exponential time. Our key technical contribution is a translation of SHACL under the well-founded semantics into the full hybrid mu-calculus, revealing a novel link between well-founded models and a fixed point modal logic, and a worst-case optimal automata-based decision procedure.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。