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.

翻译：我们研究基于无环合取双向正则路径查询（acyclic C2RPQs）的Datalog风格规则所定义的图变换，并探讨两个基本静态分析问题：存在图模式情况下的类型检查与变换等价性。此外，我们研究目标模式抽取问题，旨在构建能够精确表征输入模式约束下所有变换输出图的模式。通过将这些归约为模式约束下的C2RPQ包含判定问题，我们证明所有这些问题均处于EXPTIME复杂度类，并提供匹配的下界。我们采用循环反转技术将查询包含问题归约为描述逻辑理论约束下C2RPQ的无限制（有限或无限）可满足性问题。