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可满足性问题。