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.

翻译：SHACL（形状约束语言）通过所谓的形状对RDF数据施加约束。其核心功能是验证：检查数据图是否符合SHACL文档。但迄今为止，尚无用于比较文档的静态分析服务。本文研究以下问题：判定所有验证了某个SHACL文档的图是否也验证另一个文档。与先前仅考虑形状表达式蕴含关系的工作不同，我们考虑包含（递归）形状定义与目标对象的文档。我们证明在支持语义和稳定模型语义下，蕴含关系（即包含关系）是不可判定的，即使是使用描述逻辑ALCIO作为形状表达式的片段也是如此。令人惊讶的是，在良基语义下，该问题可在单指数时间内判定。我们的关键技术贡献是将良基语义下的SHACL转换为完整的混合μ演算，揭示了良基模型与定点模态逻辑之间的新颖联系，并提出了一个最坏情况最优的基于自动机的判定过程。