Static Analysis of Recursive SHACL
Anouk Oudshoorn, Magdalena Ortiz, Mantas Simkus
TLDR
This paper explores static analysis for recursive SHACL documents, finding implication undecidable under some semantics but decidable under well-founded semantics.
Key contributions
- Studies implication (containment) of recursive SHACL documents, including shape definitions and targets.
- Shows implication is undecidable under supported and stable model semantics, even for ALCIO fragment.
- Proves implication is decidable in single exponential time under well-founded semantics.
- Translates SHACL (well-founded semantics) into full hybrid mu-calculus, providing an optimal decision procedure.
Why it matters
This work introduces the first static analysis for comparing recursive SHACL documents, a crucial step for managing and evolving complex RDF data constraints. By identifying decidable fragments, it opens avenues for practical tools to ensure consistency and correctness in data validation.
Original Abstract
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.
📬 Weekly AI Paper Digest
Get the top 10 AI/ML arXiv papers from the week — summarized, scored, and delivered to your inbox every Monday.