arxiv: 2605.02787 · v1 · submitted 2026-05-04 · 💻 cs.LO · cs.AI

Recognition: unknown

Static Analysis of Recursive SHACL

Anouk Oudshoorn, Magdalena Ortiz, Mantas Simkus

Authors on Pith no claims yet

Pith reviewed 2026-05-08 17:36 UTC · model grok-4.3

classification 💻 cs.LO cs.AI

keywords SHACLimplicationcontainmentwell-founded semanticshybrid mu-calculusrecursive shapesundecidabilitystatic analysis

0 comments

The pith

Implication between recursive SHACL documents is undecidable under supported and stable model semantics but decidable in single exponential time under well-founded semantics.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper tries to establish whether one can decide if one SHACL document is implied by another, that is, if every graph validating the first also validates the second. A sympathetic reader would care because this static analysis would let users compare and optimize constraint documents without inspecting actual data graphs. The results show that this is undecidable under supported and stable model semantics even for limited shape expressions, but decidable in single exponential time under well-founded semantics by translating to hybrid mu-calculus.

Core claim

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.

What carries the argument

The translation of SHACL under the well-founded semantics into the full hybrid mu-calculus that preserves satisfiability and validity exactly and reduces implication to automata-based procedures.

If this is right

Implication can be decided in single exponential time for well-founded semantics using existing automata techniques for the hybrid mu-calculus.
No algorithm decides implication for arbitrary recursive SHACL documents under supported or stable model semantics.
The decidability result holds even when shape expressions are restricted to the ALCIO description logic.
The translation links well-founded SHACL models directly to fixed-point modal logic.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Well-founded semantics may be preferable in settings where automated comparison of SHACL documents is needed.
Tools based on supported or stable semantics may need to forbid recursion or restrict targets to regain decidability of containment.
The reduction technique might extend to other graph constraint languages that admit well-founded fixed-point semantics.

Load-bearing premise

The translation from SHACL documents under well-founded semantics into hybrid mu-calculus formulas preserves satisfiability and validity exactly.

What would settle it

A concrete pair of recursive SHACL documents for which the mu-calculus translation disagrees with the actual implication relation under well-founded semantics, or a finite procedure that decides implication for all cases under stable model semantics.

Figures

Figures reproduced from arXiv: 2605.02787 by Anouk Oudshoorn, Magdalena Ortiz, Mantas Simkus.

**Figure 1.** Figure 1: Evaluating shape expressions: upper and lower bounds. view at source ↗

**Figure 2.** Figure 2: Infinite grid that, after adding s as label to every node, shows undecidability of shape implication w.r.t. constraints under the supported model semantics. The grey dashed arrows indicate the extension of the role l. above consider both finite and unrestricted models; others focus on finite ones. In some cases, the finite model property is inferred by establishing a connection to logics that enjoy it. We … view at source ↗

**Figure 3.** Figure 3: Semantics of µ-calculus formulas. tr + S,C (s ∧ s ′ ) := tr + S,C (s) ∧ tr + S,C (s ′ ) tr − S,C (s ∧ s ′ ) := tr − S,C (s) ∨ tr − S,C (s ′ ) tr + S,C (s ∨ s ′ ) := tr + S,C (s) ∨ tr + S,C (s ′ ) tr − S,C (s ∨ s ′ ) := tr − S,C (s) ∧ tr − S,C (s ′ ) tr + S,C (∃r.s) := ⟨r⟩tr + S,C (s) tr − S,C (∃r.s) := [r]tr − S,C (s) tr + S,C (∀r.s) := [r]tr + S,C (s) tr − S,C (∀r.s) := ⟨r⟩tr − S,C (s) tr + S,C (A) := A t… view at source ↗

**Figure 4.** Figure 4: Translation functions, note the negated translation of negation, view at source ↗

**Figure 5.** Figure 5: Cleaning function. B Proofs for Section 5 (Translating SHACL into µ-calculus) Note that the constraint definitions that are not reachable from a target are irrelevant to its validation, and hence to test s we can just use Cs, defined in the following way. Definition 4. Given a constraint set C, let clC(s), the closure of a shape name s w.r.t. C, be defined as the smallest set of shape names s ′ ∈ NS such t… view at source ↗

read the 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

SHACL implication is undecidable under supported and stable semantics but EXPTIME decidable under well-founded semantics via a reduction to hybrid mu-calculus.

read the letter

The key result here is that implication for full recursive SHACL documents is undecidable under the supported and stable model semantics, even when restricted to ALCIO shape expressions, while under well-founded semantics it is decidable in EXPTIME. The paper achieves this by translating SHACL under well-founded semantics into hybrid mu-calculus, which has known decision procedures. What stands out is how the paper handles full documents including targets and recursive definitions, going beyond earlier work that looked only at shape expressions. The contrast between the semantics is presented clearly, and the link to mu-calculus provides both the decidability and the complexity bound. This seems like a useful connection that could open doors for other analyses. The potential weak point is the translation itself. It needs to preserve satisfiability and validity exactly, and while the abstract outlines it, the full proof would be the place to check for any gaps in handling recursion or the well-founded models. The undecidability parts are likely shown by reduction from known undecidable problems, which is standard but should be verified for the specific setting. Overall, this paper is for researchers in semantic web technologies, description logics, and modal logics who are interested in static analysis and decidability for constraint languages like SHACL. It provides concrete bounds that prior work lacked. I think it deserves a serious referee because the results are non-trivial and the technical approach is interesting enough to warrant detailed review. The authors engage honestly with the literature on SHACL semantics. My recommendation is to send it to peer review.

Referee Report

1 major / 2 minor

Summary. The paper studies the implication (containment) problem for recursive SHACL documents comprising shape definitions and targets. It proves undecidability under supported and stable model semantics, even when shape expressions are restricted to the ALCIO fragment of description logic. In contrast, under well-founded semantics the problem is decidable in single-exponential time; the key technical step is a translation of SHACL documents under well-founded semantics into formulas of the full hybrid mu-calculus, which then inherits an automata-based decision procedure.

Significance. If the translation is semantics-preserving, the work establishes the first decidability and complexity results for implication of full recursive SHACL documents (including targets) and reveals a novel, non-obvious connection between well-founded models and hybrid fixed-point modal logic. This supplies both a theoretical foundation for static analysis tools and an optimal EXPTIME procedure that leverages pre-existing automata techniques for the target logic.

major comments (1)

[Translation section (around the definition of the mapping from SHACL to hybrid mu-calculus)] The central decidability claim rests on the translation from well-founded SHACL to hybrid mu-calculus preserving satisfiability and validity exactly. The manuscript must supply an explicit lemma (or set of lemmas) in the translation section showing that every well-founded model of a SHACL document corresponds to a model of the resulting mu-calculus formula and conversely, with particular attention to the encoding of recursive shape references and the fixed-point operators that capture well-foundedness.

minor comments (2)

[Abstract and complexity discussion] The abstract asserts single-exponential time without citing the known complexity of the hybrid mu-calculus decision procedure or stating whether the bound is tight; the main text should make this explicit.
[Preliminaries] Notation for the three semantics (supported, stable, well-founded) and for the implication relation should be introduced once in a dedicated preliminaries section and used consistently thereafter.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive evaluation and the recommendation of minor revision. We address the single major comment below.

read point-by-point responses

Referee: [Translation section (around the definition of the mapping from SHACL to hybrid mu-calculus)] The central decidability claim rests on the translation from well-founded SHACL to hybrid mu-calculus preserving satisfiability and validity exactly. The manuscript must supply an explicit lemma (or set of lemmas) in the translation section showing that every well-founded model of a SHACL document corresponds to a model of the resulting mu-calculus formula and conversely, with particular attention to the encoding of recursive shape references and the fixed-point operators that capture well-foundedness.

Authors: We agree that an explicit lemma (or set of lemmas) is required to rigorously establish that the translation preserves models in both directions. The current manuscript defines the mapping and invokes the known EXPTIME decision procedure for hybrid mu-calculus, but the precise correspondence—especially the treatment of recursive shape references via greatest and least fixed-point operators and the encoding of well-foundedness—is only described informally. In the revised version we will add, in the translation section, a lemma stating that a graph is a well-founded model of a SHACL document if and only if the corresponding hybrid mu-calculus formula is satisfied in the induced Kripke structure. The proof will explicitly address the recursive case by induction on the fixed-point unfolding and the well-foundedness condition. This addition does not change any technical result but improves the clarity and self-containedness of the argument. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation reduces to independent prior results

full rationale

The paper's undecidability results for supported and stable semantics are obtained via reductions to known undecidable problems in description logics and logic programming, without self-definitional equations or fitted inputs. The decidability result under well-founded semantics rests on an explicit translation to the hybrid mu-calculus, whose automata-based decision procedure and complexity bounds predate this work and are cited as external. No load-bearing step equates the target claim to a parameter fit, self-citation chain, or renamed ansatz within the paper; the translation itself constitutes independent technical content that preserves satisfiability exactly, allowing external procedures to decide the problem.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work rests on standard background results from description logics and fixed-point modal logics; no free parameters, ad-hoc constants, or new postulated entities are introduced in the abstract.

axioms (2)

standard math The hybrid mu-calculus admits an automata-based decision procedure for its satisfiability problem.
Invoked to obtain the single-exponential time bound for the translated SHACL problem.
domain assumption The well-founded semantics of recursive SHACL is faithfully captured by the translation into hybrid mu-calculus.
This is the load-bearing link stated as the key technical contribution.

pith-pipeline@v0.9.0 · 5473 in / 1381 out tokens · 48116 ms · 2026-05-08T17:36:36.801861+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

27 extracted references

[1]

Ahmetaj, S.; Ortiz, M.; Oudshoorn , A.; and S imkus, M. 2023. Reconciling SHACL and ontologies: Semantics and validation via rewriting. In Gal, K.; Now \' e , A.; Nalepa, G. J.; Fairstein, R.; and Radulescu, R., eds., ECAI 2023 - 26th European Conference on Artificial Intelligence , volume 372 of Frontiers in Artificial Intelligence and Applications , 27-...

2023
[2]

Ahmetaj, S.; Boneva, I.; Hidders, J.; Jakubowski, M.; Labra-Gayo, J.-E.; Martens, W.; Mogavero, F.; Murlak, F.; Okulmus, C.; Savković, O.; S imkus, M.; and Tomaszuk, D. 2026. Common foundations for recursive shape languages. In Proc.\,of 23rd International Conference on Principles of Knowledge Representation and Reasoning (KR 2026)

2026
[3]

L.; Savkovic, O.; and S imkus, M

Andresel, M.; Corman, J.; Ortiz, M.; Reutter, J. L.; Savkovic, O.; and S imkus, M. 2020. Stable model semantics for recursive SHACL . In Huang, Y.; King, I.; Liu, T.; and van Steen, M., eds., WWW '20: The Web Conference 2020, Taipei, Taiwan, April 20-24, 2020 , 1570--1580. ACM / IW3C2

2020
[4]

R.; Blair, H

Apt, K. R.; Blair, H. A.; and Walker, A. 1988. Towards a theory of declarative knowledge. In Minker, J., ed., Foundations of Deductive Databases and Logic Programming . Morgan Kaufmann. 89--148

1988
[5]

Arnold, A., and Niwinski, D. 2001. Rudiments of -calculus. Studies in Logic and the Foundations of Mathematics 146

2001
[6]

B \' a r \' a ny, V., and Bojanczyk, M. 2012. Finite satisfiability for guarded fixpoint logic. Inf. Process. Lett. 112(10):371--375

2012
[7]

Berger, R. 1966. The undecidability of the domino problem . Number 66. American Mathematical Soc

1966
[8]

Bogaerts, B.; Jakubowski, M.; and Van den Bussche, J. 2022. SHACL: A description logic in disguise. In Gottlob, G.; Inclezan, D.; and Maratea, M., eds., Logic Programming and Nonmonotonic Reasoning - 16th International Conference, LPNMR 2022, Genova, Italy, September 5-9, 2022, Proceedings , volume 13416 of Lecture Notes in Computer Science , 75--88. Springer

2022
[9]

Bojanczyk, M. 2002. Two-way alternating automata and finite models. In Widmayer, P.; Ruiz, F. T.; Bueno, R. M.; Hennessy, M.; Eidenbenz, S. J.; and Conejo, R., eds., Automata, Languages and Programming, 29th International Colloquium, ICALP 2002, Malaga, Spain, July 8-13, 2002, Proceedings , volume 2380 of Lecture Notes in Computer Science , 833--844. Springer

2002
[10]

A.; Lutz, C.; Murano, A.; and Vardi, M

Bonatti, P. A.; Lutz, C.; Murano, A.; and Vardi, M. Y. 2008. The complexity of enriched mu-calculi. Log. Methods Comput. Sci. 4(3)

2008
[11]

L.; and Savkovic, O

Corman, J.; Reutter, J. L.; and Savkovic, O. 2018. Semantics and validation of recursive SHACL . In Vrandecic, D.; Bontcheva, K.; Su \' a rez - Figueroa, M. C.; Presutti, V.; Celino, I.; Sabou, M.; Kaffee, L.; and Simperl, E., eds., The Semantic Web - ISWC 2018 - 17th International Semantic Web Conference, Monterey, CA, USA, October 8-12, 2018, Proceeding...

2018
[12]

Di Stefano, F., and S imkus, M. 2024. Stable model semantics for description logic terminologies. In Wooldridge, M. J.; Dy, J. G.; and Natarajan, S., eds., Thirty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2024, Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence, IAAI 2024, Fourteenth Symposium on Educational Advanc...

2024
[13]

Oudshoorn , A.; Ortiz, M.; and S imkus, M. 2024. Reasoning with the core chase: the case of SHACL validation over ELHI knowledge bases. In Giordano, L.; Jung, J. C.; and Ozaki, A., eds., Proceedings of the 37th International Workshop on Description Logics (DL 2024), Bergen, Norway, June 18-21, 2024 , volume 3739 of CEUR Workshop Proceedings . CEUR-WS.org

2024
[14]

Oudshoorn , A.; Ortiz, M.; and Šimkus, M. 2026. SHACL validation in the presence of ontologies: Semantics and rewriting techniques. Artificial Intelligence 352:104483

2026
[15]

Oudshoorn , A. 2025. SHACL satisfiability: What can we learn from dls? In Proceedings of the 38th International Workshop on Description Logics (DL 2025), Opole, Poland, September 3-6, 2025 , volume 4091 of CEUR Workshop Proceedings . CEUR-WS.org

2025
[16]

Knublauch, H., and Kontokostas, D. 2017. Shapes Constraint Language (SHACL). W3C Recommendation , W3C . https://www.w3.org/TR/shacl/

2017
[17]

Leinberger, M.; Seifer, P.; Rienstra, T.; L \" a mmel, R.; and Staab, S. 2020. Deciding SHACL shape containment through description logics reasoning. In Pan, J. Z.; Tamma, V.; d'Amato, C.; Janowicz, K.; Fu, B.; Polleres, A.; Seneviratne, O.; and Kagal, L., eds., The Semantic Web - ISWC 2020 - 19th International Semantic Web Conference, Athens, Greece, Nov...

2020
[18]

E., and Schupp, P

Muller, D. E., and Schupp, P. E. 1987. Alternating automata on infinite trees. Theor. Comput. Sci. 54:267--276

1987
[19]

Okulmus, C., and S imkus, M. 2024. SHACL validation under the well-founded semantics. In Marquis, P.; Ortiz, M.; and Pagnucco, M., eds., Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning, KR 2024, Hanoi, Vietnam. November 2-8, 2024

2024
[20]

Ortiz, M. 2023. A short introduction to SHACL for logicians. In Hansen, H. H.; Scedrov, A.; and de Queiroz, R. J. G. B., eds., Logic, Language, Information, and Computation - 29th International Workshop, WoLLIC 2023, Halifax, NS, Canada, July 11-14, 2023, Proceedings , volume 13923 of Lecture Notes in Computer Science , 19--32. Springer

2023
[21]

Pareti, P.; Konstantinidis, G.; and Mogavero, F. 2022. Satisfiability and containment of recursive SHACL . J. Web Semant. 74:100721

2022
[22]

Sattler, U., and Vardi, M. Y. 2001. The hybrid \( \) -calculus. In Gor \' e , R.; Leitsch, A.; and Nipkow, T., eds., Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings , volume 2083 of Lecture Notes in Computer Science , 76--91. Springer

2001
[23]

Tamura, K. 2015. A small model theorem for the hybrid \( \) -calculus. J. Log. Comput. 25(2):405--441

2015
[24]

Ten Cate, B., and Franceschet, M. 2005. Guarded fragments with constants. J. Log. Lang. Inf. 14(3):281--288

2005
[25]

Tobies, S. 2000. The complexity of reasoning with cardinality restrictions and nominals in expressive description logics. J. Artif. Intell. Res. 12:199--217

2000
[26]

A.; and Schlipf, J

Van Gelder, A.; Ross, K. A.; and Schlipf, J. S. 1991. The well-founded semantics for general logic programs. J. ACM 38(3):620--650

1991
[27]

Van Gelder, A. 1993. The alternating fixpoint of logic programs with negation. J. Comput. Syst. Sci. 47(1):185--221

1993