Static Analysis of Recursive SHACL
Provides the first static analysis for comparing SHACL documents, addressing a fundamental problem for practitioners and researchers working with RDF constraints.
The paper studies the implication problem for SHACL documents (whether all graphs validating one document also validate another) and shows it is undecidable under supported and stable model semantics but decidable in single exponential time under well-founded semantics, via a translation to the hybrid mu-calculus.
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.