TY - JOUR
T1 - Satisfiability and Containment of Recursive SHACL
AU - Pareti, Paolo
AU - Konstantinidis, George
AU - Mogavero, Fabio
N1 - Funding Information:
G. Konstantinidis was partially supported by The Alan Turing Institute under the EPSRC grant EP/N510129/1 , and a Turing Enhancement Project. F. Mogavero has been partially supported by the GNCS 2020 project “Ragionamento Strategico e Sintesi Automatica di Sistemi Multi-Agente”. The authors thank the anonymous reviewers for insightful comments that helped improve the quality of the article, e.g., for proposing a proof approach that directly led to the undecidability result for the fragment.
Publisher Copyright:
© 2022 The Author(s)
PY - 2022/10/1
Y1 - 2022/10/1
N2 - The Shapes Constraint Language (SHACL) is the recent W3C recommendation language for validating RDF data, by verifying certain shapes on graphs. Previous work has largely focused on the validation problem, while the standard decision problems of satisfiability and containment, crucial for design and optimisation purposes, have only been investigated for simplified versions of SHACL. Moreover, the SHACL specification does not define the semantics of recursively-defined constraints, which led to several alternative recursive semantics being proposed in the literature. The interaction between these different semantics and important decision problems has not been investigated yet. In this article we provide a comprehensive study of the different features of SHACL, by providing a translation to a new first-order language, called SCL, that precisely captures the semantics of SHACL. We also present MSCL, a second-order extension of SCL, which allows us to define, in a single formal logic framework, the main recursive semantics of SHACL. Within this language we also provide an effective treatment of filter constraints which are often neglected in the related literature. Using this logic we provide a detailed map of (un)decidability and complexity results for the satisfiability and containment decision problems for different SHACL fragments. Notably, we prove that both problems are undecidable for the full language, but we present decidable combinations of interesting features, even in the face of recursion.
AB - The Shapes Constraint Language (SHACL) is the recent W3C recommendation language for validating RDF data, by verifying certain shapes on graphs. Previous work has largely focused on the validation problem, while the standard decision problems of satisfiability and containment, crucial for design and optimisation purposes, have only been investigated for simplified versions of SHACL. Moreover, the SHACL specification does not define the semantics of recursively-defined constraints, which led to several alternative recursive semantics being proposed in the literature. The interaction between these different semantics and important decision problems has not been investigated yet. In this article we provide a comprehensive study of the different features of SHACL, by providing a translation to a new first-order language, called SCL, that precisely captures the semantics of SHACL. We also present MSCL, a second-order extension of SCL, which allows us to define, in a single formal logic framework, the main recursive semantics of SHACL. Within this language we also provide an effective treatment of filter constraints which are often neglected in the related literature. Using this logic we provide a detailed map of (un)decidability and complexity results for the satisfiability and containment decision problems for different SHACL fragments. Notably, we prove that both problems are undecidable for the full language, but we present decidable combinations of interesting features, even in the face of recursion.
KW - Containment
KW - Data validation
KW - FOL
KW - Logic
KW - SHACL
KW - Satisfiability
UR - http://www.scopus.com/inward/record.url?scp=85132931053&partnerID=8YFLogxK
UR - https://www.mendeley.com/catalogue/a428f1a6-1e55-3ea5-b132-6a455ad58ca1/
U2 - 10.1016/j.websem.2022.100721
DO - 10.1016/j.websem.2022.100721
M3 - Article
VL - 74
JO - Journal of Web Semantics
JF - Journal of Web Semantics
SN - 1570-8268
M1 - 100721
ER -