Static Analysis of Recursive SHACL

TL;DR

This paper investigates static analysis for SHACL shape implication, showing undecidability under certain semantics but decidability under well-founded semantics, with a translation to hybrid mu-calculus.

Contribution

It introduces a decision procedure for SHACL implication under well-founded semantics by translating it into hybrid mu-calculus, establishing a novel connection.

Findings

Implication is undecidable under supported and stable semantics.

Implication is decidable in single exponential time under well-founded semantics.

A translation to hybrid mu-calculus enables the decision procedure.

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.