Static Analysis of Recursive SHACL

SHACL (Shapes Constraint Language) expresses constraints on RDF data by means of so-called shapes. The central service is validation: verifying whether a data graph complies with a SHACL specification, but there are no static analysis services to compare specifications. 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 specifications comprising shape definitions and targets. We show that 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 contrast, it is decidable in single exponential time. Our key technical contributions are a translation of SHACL under well-founded semantics into the full hybrid mu-calculus, revealing a novel link between shape validation and fixed point modal logic, and a worst-case optimal automata-based decision procedure.