Static Analysis of Graph Database Transformations

TL;DR

This paper studies static analysis problems for graph transformations defined by Datalog-like rules, focusing on type checking, equivalence, and schema elicitation, with complexity results in EXPTIME.

Contribution

It introduces a formal framework for analyzing graph transformations with acyclic C2RPQs and establishes complexity bounds for key static analysis problems.

Findings

Type checking and equivalence are in EXPTIME.

Schema elicitation can be effectively reduced to C2RPQ containment.

Cycle reversing technique links query containment to satisfiability in description logic.

Abstract

We investigate graph transformations, defined using Datalog-like rules based on acyclic conjunctive two-way regular path queries (acyclic C2RPQs), and we study two fundamental static analysis problems: type checking and equivalence of transformations in the presence of graph schemas. Additionally, we investigate the problem of target schema elicitation, which aims to construct a schema that closely captures all outputs of a transformation over graphs conforming to the input schema. We show all these problems are in EXPTIME by reducing them to C2RPQ containment modulo schema; we also provide matching lower bounds. We use cycle reversing to reduce query containment to the problem of unrestricted (finite or infinite) satisfiability of C2RPQs modulo a theory expressed in a description logic.