This article introduces a restriction on the usage of negation in SHACL “core constraint components” constraints, called strict stratification, which guarantees tractability of graph validation. SHACL Specification and Formal Semantics
One of the challenges of recent RDF-based applications is managing data quality [
The SHACL specification however leaves explicitly undefined the validation of
recursive constraints. In a previous article [
Our previous work identified a tractable fragment of SHACL’s core components. In this paper, we propose an alternative approach to gain tractability, retaining all SHACL operators, but strengthening the stratification condition traditionally used in logic programming. More exactly, we introduce a syntactic condition on shape constraints called “strict stratification”, which guarantees that graph validation is in PTIME in combined (i.e. graph and constraints) complexity. We also describe a procedure to perform such validation.
The current paper is not self-contained, due to space limitations, but all definitions
can be found in our previous article [
According to this syntax, a shape can reference another. But the SHACL specification
leaves open the recursive case, i.e. when a shape references itself, either directly, or via a
reference cycle. As a solution, we proposed a semantics based on the notion of assignment,
that maps (positive and negative) shape labels to sets of nodes, and we defined constraint
evaluation given an assignment. Formally, a shape assignment for G and S is a total
function from pairs hs; vi of shape name and node to f0(false); 0:5(unknown); 1(true)g
(the “unknown” value is used to deal with cases when recursion and negation can be
arbitrarily combined). The evaluation of formula at node v given assignment is
written J Kv;G; (for a formal definition we refer to [
This section defines strict stratification of a set of SHACL shapes, and proposes a PTIME validation algorithm (combined complexity) for this case. We chose to convey the general intuition behind stratification from a procedural perspective, as follows: if there is a satisfying assignment for a given input, then it may be built stratum by stratum, starting from the lowest stratum, and assigning shapes in a greedy fashion, without the need to backtrack from a higher to a lower stratum. However, adopting the classical definition of stratified negation (borrowed from Datalog) is not sufficient to avoid such backtracking. This is why we define the stronger notion of strict stratification.
Let S be a set of shapes. We say that shape s1 references shape s2 if s2 appears in the definition of s1. Further, we define the dependency graph of S as the directed graph with all shape names defined in S as nodes, and an edge from s1 to s2 iff s1 references s2. If the reference is in the scope of negation, then the edge is labeled with a negation symbol (as in Fig. 1), and we call it a negative edge. A path between two nodes is called negative if it contains at least one negative edge, and positive otherwise. S is stratified iff its dependency graph has no negative cycle. Finally, we define the contracted dependency graph of S as the graph obtained from its dependency graph by contracting all positive strongly connected components.
Definition 1 (strict stratification). A set S of shapes is strictly stratified if, for any pair (s1; s2) of nodes in its contracted dependency graph, either: – there is at most one path from s1 to s2, or – all paths from s1 to s2 are positive. s1 s0 v2
P P : s2 In this definition, using the contracted dependency graph (rather than the dependency graph) allows us to capture a more expressive fragment of SHACL. We also note that from this definition, a strictly stratified set of shapes must be stratified. Example 1. Consider the three shape definitions and their contracted dependency graph in Figure 1. This set of shape is stratified, but not strictly stratified, since there are more than one paths from s0 to s2, and one of them is negative.
s2 =: ( 1 P:s2) s0 =: ( 1 P:s1) ^ ( 1 P:s2)
: s1 = :( 1 P:s2) Example 2. Consider again the shapes from Example 1, together with the graph in Figure 2. Assume now that one tries to build a validating assignment for the target hv0; s0i in a greedy fashion, taking advantage of stratification, thus starting from the lowest stratum fs2g. Then s2 can be assigned to v0; v2 and v3. Moving up to the next stratum fs0; s1g, s0 cannot be assigned to v0, because the definition of s1 is violated by v1, and therefore the conjunct ( 1 P:s1) is not verified by v0. In order to find a validating assignment, one would need to backtrack, reverting the decision to assign s2 to v2. But the decision to assign s2 to v3 on the other hand should not be reverted, otherwise the conjunct ( 1 P:s2) would not be verified by v0 anymore. It can be easily seen that such pattern can lead to a blowup of backtracking alternatives, exponential in the size of the graph under validation.
The intuition for intractability is illustrated by Example 2 (in terms of backtracking),
and was made more formal in [
Let G;S be the family of all (3-valued) assignments for G and S. The operator TG;S : eaGch;Ssh!ape cGo;nSsttarakienst adnefiasnsiitgionnmaetnetac,hannoddreetguirvnesnthe, ai.ses.ig(TnmGe;Snt(ob))ta(isn;evd)b=y eJvaslKuva;tGin;g for each s and v. So from the definition of graph validation given in Section 2, hG; S; s0; v0i is valid iff TG;S admits a fixed-point verifying (s; v) = 1. We also need the Algorithm 1 VALIDATION PROCEDURE FOR STRICTLY STRATIFIED SHAPES Input: G; S; s0; v0 1: Initiate with (s; v) = 0:5, for each shape s and node v 2: repeat 3: 0 4: TG;S( ) 5: until = 0 6: if (s0; v0) = 0 then return Invalid 7: else return Valid partial order over G;S , defined by 1 2 iff 1(s; v) = 0 implies 2(s; v) = 0, and 1(s; v) = 1 implies 2(s; v) = 1, for any s and v.
Next, it is shown in [
We are also currently developing implementation techniques for validation based on logic programming. More exactly, since validation is based on the the existence of a fixed-point evaluation/assignment, we are investigating an encoding into Datalog for the strictly stratified case, and into to more expressive logic formalisms for non-strictly stratified constraints.
Acknowledgments. This work was supported by the QUEST, QUADRO and ADVANCE4KG projects at the Free University of Bozen-Bolzano.