Query Reasoning on Data Trees with Counting

Abstract

Regular path expressions represent the navigation core of the XPath query language for semi-structured data (XML), and it has been characterized as the First Order Logic with Two Variables (FO2). Data tests refers to (dis)equality comparisons on data tree models, which are unranked trees with two kinds of labels, propositions from a nite alphabet, and data values from a possibly in nite alphabet. Node occurrences on tree models can be constrained by counting/arithmetic constructors. In this paper, we identify an EXPTIME extension of regular paths with data tests and counting operators. This extension is characterized in terms of a closed under negation Presburger tree logic. As a consequence, the EXPTIME bound also applies for standard query reasoning (emptiness, containment and equivalence).

Introduction

XPath is a W3C standard query language for semi-structured data (XML), and it also takes an important role in many XML technologies, such as, XProc, XSLT, and XQuery [ 1, 2 ]. The navigation core of XPath, also known as regular path queries, has been recently characterized by the First Order Logic of Two Variables (FO2) [ 1 ]. Models for this logic are unranked trees, where nodes are labeled by propositions from a nite alphabet. Data tests, also known as data joins in databases community, on XPath queries are expressions of the forms 1 2 and 1 6 2. These expressions hold whenever data values (propositions from an in nite alphabet) contained in path 1 are (dis)equal to data values contained in path 2, respectively. Another important constructors on XPath queries concerns counting: 1 # 2, where # 2 f ; >; =; 6=g. These expressions hold whenever the number of nodes denoted by 1 and 2 satis es constraint #. There are several recent works studying regular path extensions with either data tests or counting [3{6, 2]. However, as far as we know, the current work represent the rst study on regular path extensions concerning both constructors, data tests and counting. More precisely, we give a characterization of a regular paths with data test with respect to constants k ( 6 k) and with counting operators on children paths. For this characterization we use a modal tree logic equipped with a xed point operator, converse modalities and Presburger arithimetic constraints [ 7 ]. Due to this characterization, the EXPTIME bound from the logic is imported to standard query reasoning (emptiness, containment, and equivalence) with counting and data tests.

There are several extensions of FO2 with data tests [8{11]. In [ 8 ], FO2(< ; +1; ) for data trees is introduced: < stands for descendants and following sibling relations, +1 refers to child and next sibling relations, and is a binary predicate for data tests. Decidability, without any complexity analysis, for FO2(<; +1; ) in data trees is rst shown by a reduction to the reachability problem of a counter tree automata model. Previously in [ 10 ], the same result was obtained for data words (one branched tree). Even earlier in [ 11 ], FO2(+1; ) for trees was introduced and shown decidable in 3NEXPTIME. In another direction, regarding regular paths (XPath navigation core), it is well know data test on full navigation regular paths is undecidable [ 5 ]. Several fragments (downward, forward, transitive) of regular path expressions with data tests are studied [ 12, 13, 6, 5, 3 ]. With their corresponding complexity ranging from EXPTIME to non elementary. Contrastingly, in this paper, instead of restricting navigation on queries, we study the full navigation (children, parents, following and previous sibling, descendants and ancestros) regular path expressions, but we restrict data tests to constants only.

Regarding regular paths with counting, there are several recent studies [ 1, 2, 4 ]. In [ 1 ], it was show the extension of regular paths with counting is in general undecidable. EXPTIME fragments (counting with respect to constants) were later identi ed in [ 2, 4 ]. Several other logics with counting have been proposed in the setting of unranked trees [14{16, 7, 17]. In [ 17 ], the EXPTIME bound was further developed for a set of coalegebraic modal logics via a type elimination algorithm. Excepting [ 18 ], where the emptiness problem for ranked tree automaton with equality and counting constraints was shown decidable without a further complexity analysis, all the above works study separately data tests and counting. In the current work, we identify an EXPTIME extension of regular paths with both, data tests and counting.

We describe a counting and data tests extension of regular paths in Section 2. In Section 3, we describe a modal tree logic with a xed point, converse modalities and Presburger arithmetic constructors. The main result of this paper, which is a characterization of the regular path extension with counting and data tests in terms of the logic, is described in Section 4. We conclude with a summary of this work, together with a brief discussion of further research perspectives in Section 5. 2

Regular Path Queries with Counting and Data Tests

For the languages described in the current work, unless otherwise stated, we use a xed alphabet composed by set of propositions P ROP S and a a set of modalities M ODS = f ; ; ; g. Intuitively, propositions are used in tree models to label nodes, and modalities are interpreted as the children , parent , right siblings , and left siblings relations.

We now introduce the notion of a tree, which can be seen as a tree-shaped Kripke structure (transition system).

De nition 1 (Tree). A tree T is de ned as a tuple (N; R; L), such that: N is a nite set of nodes; R : N M ODS N is a transition relation among nodes and modalities forming a tree (we often write n 2 R(n0; m) instead of (n0; m; n) 2 R); and L : N P ROP S is a left-total labeling relation (we often write p 2 L(n) instead of (n; p) 2 L).

The set of data values are the set of natural numbers N. Data trees can be seen as an extension of trees (De nition 1), where nodes are labeled with data values and propositions.

De nition 2 (Data tree). A data tree is de ned as a tuple (N; R; L; D), such that: (N; R; L) is a tree; and D : N 7! N is a total function.

We now give a precise syntax of regular paths with counting and data tests. De nition 3 (Syntax). We de ne the RPQCD expressions (queries) by the following grammar: :=> j j p j := j # k j : p j = j [ ] k j : j _ where p 2 P ROP S, k 2 N, # 2 f>; ; =g and 2 f ; ; ; ; ?; ?g.

In the case of 1 2 # k, both i (i = 1; 2) are restricted to be children paths, that is, they have one of the following forms: , : p, [ ] or : p[ ].

RPQCD expressions are interpreted over data trees: > selects the entire set of nodes; : p navigates through and selects the p nodes; 1= 2 is the compositions of paths; and [ ] selects the nodes denoted by satisfying condition . In particular, when is k, it holds whenever there is a node denoted by whose data value is equal to k. 1 2 # k is true if and only if the number of nodes selected by 1 minus the number of nodes selected by 2, satis es constraint #k. Notice some syntactic sugar (notation) as 1# 2 instead of 1 2#0 can also be de ned. Negation and disjunction are interpreted as expected.

We now give a precise description on how RPQCD expressions are interpreted over data trees. De nition 4 (Semantics). Given a data tree pressions are interpreted as follows: = (N; R; L; D), RPQCD ex[[ ]] = n(n1; n2) j n1 ! n2o [[ : p]] = n(n1; n2) 2 [[ ]] j p 2 L(n2) o [[ [ ]]] = n(n1; n2) 2 [[ ]] j n2 2 [[[ ]]]

o [[[ ]]] = nn j (n; n0) 2 [[ ]]

o

k]]] = nn j (n0; n) 2 [[[ ]]] ; D(n) = ko [[[: ]]] =N n [[[ ]]] [[ 1 _ 2]] = [[[ 1 ]]] [ [[[ 2 ]]] where n1 ! n2 holds, if and only if, n1 is related to n2 through in .

We also interpret RPQCD expressions with respect to a context, more precisely, the interpretation of a RPQCD expression on a data tree from a subset of o nodes N 0 (of ) is de ned as follows: [[ ]]N0 = nn0 j (n; n0) 2 [[ ]] ; n 2 N 0

We now de ne the standard query reasoning problems for RPQCD: emptiness, containment and equivalence.

De nition 5 (Reasoning).

{ We say a RPQCD expression is empty, if and only if, for any data tree , we have that [[ ]] 6= ;. { Given two RPQCD expressions 1 and 2, we say 1 is contained in 2, written 1 2, if and only if, for any data tree , we have that [[ 1 ]] [[ 2 ]] . { Given two RPQCD expressions 1 and 2, we say 1 is equivalent to 2, if and only if, 1 2 and 2 1. 3

A Presburger Tree Logic

We now describe a modal tree logic, as originally introduced in [ 7 ], with a xed point, converse modalities and Presburger arithmetic operators. De nition 6 (Syntax). We inductively de ne the set of TLIC formulas by the following grammar: := p j : j _ j hmi j x: j # k, where p 2 P ROP S, m 2 M ODS, # 2 f>; ; =g, and k 2 N coded in binary form.

TLIC expressions are interpreted as subset tree nodes: propositions are used as node labels; negation is interpreted as set complement; disjunction as set union; modal formulas hmi holds in nodes where there is at least one m transition to a node supporting ; the xed point operator x: is interpreted as a recursion operator; and Presburger formulas # k selects nodes whose children minus children satisfy constraint # k.

Before formally introduce the interpretation of TLIC formulas, we rst dene a valuation function V : X 7! N of set of variables x over a set of nodes of a given tree.

De nition 7 (Semantics). Given a tree T = (N; R; L) and a valuation V , TLIC formulas are interpreted as follows:

[[p]]TV = fn j p 2 L(n)g [[: ]]TV =N n [[ ]]T

V [[ _ ]]TV = [[ ]]TV [ [[ ]]T

V [[hmi ]]TV = nn j R(n; m) \ [[ ]]TV o [[ x: ]]TV = \ nM j [[ ]]TV [M =x]

M o n [[ # k]]TV = n j R(n; ) \ [[ ]]T

V

R(n; ) \ [[ ]]T

V # ko

Without loss of generality, we assume variables can only occur bounded, and in the scope of modal or counting formulas [ 7 ]. Furthermore equivalent negated normal forms can also be achieved by traditional De Morgan's and modal rules: : hmi := [m] : , :( _ ) := : ^ : , : x: := x:: [x=:x], :( > k) := k, :( k) := > k, :( = k) := 6= k, and :( 6= k) := = k.

We conclude this Section recalling the complexity of TLIC.

Theorem 1 ([ 7 ]).

TLIC is in EXPTIME-complete.

4

Logic characterization

In this Section we give a characterization of RPQCD expressions in terms of TLIC formulas.

First we de ne a non-data version of data trees. Intuitively, data values in data trees are represented by children nodes labeled by a fresh proposition . For instance, if a node has value k, then its non-data version has k children labeled by . Then, Presburger formulas can be used to test values in non-data trees.

De nition 8. Provided a data tree

(N 0; R0; L0) as follows:

= (N; R; L; D), we de ne the tree T ( ) = { let Ni be a set of ki new nodes (N \ Ni = ;) induced by data values of nodes in N , that is, for each ni 2 N , D(ni) = ki, then N 0 = N [ SjiN=1j Ni; { let Ri = fnig f g { and let Li : Ni f g be left total, then L0 = L [ SjiN=1j Li; provided is a proposition not occurring in L, that is, for each n 2 N , if (n; p) 2 L, then 6= p.

We now give a precise translation of regular paths with counting and data tests in terms of the logic.

De nition 9. We de ne a translation function F of RPQCD expressions in terms of the logic as follows:

F (>; C) := C ^ : F ( ; C) := : ^ h i C F ( ; C) := : ^ h i C F ( ?; C) := : ^ x: h i (C _ x) F ( : p; C) := F ( ; C) ^ F (p; >) F ( [ ]; C) := F ( ; C) ^ G( ; >)

F (p; C) := p ^ : ^ C F ( ; C) := : ^ h i C F ( ; C) := : ^ h i C F ( ?; C) := : ^ x: h i (C _ x) F ( 1= 2; C) := F ( 2; F ( 1; C)) where is a fresh proposition and G is a translation of quali ers (De nition 10). De nition 10. We de ne a translation of quali ers in terms of the logic as follows: G(>; C) := C ^ : G(p; C) := p ^ : ^ C G( 1= 2; C) := G( 1; G( 2; C)) G(: ; C) := :G( ; C) G( k; C) := G (

G( ; C) := F ( ; C) G( : p; C) := F ( ; C ^ p ^ : ) G( [ ]; C) := G( ; G( ; >) ^ C)

G( 1 _ 2; C) := G( 1; C) _ G( 2; C) k; C)

G( 1

2 # k; C) := G #( 1; C) G #( 2; C) # k G (> G (p

G ( G ( : p G ( 1= 2

G ( [ ] k; C) := ( k; C) := ( k; C) := G( ; ( k; C) := G( ; ( k; C) := G( 1; G ( 2 k; C) := G ( ^ h i G(>; C) = k ^ h i G(p; C)) = k ^ h i C) = k) ^ h i (C ^ p)) = k)

k; C)) k; G( ; >) ^ C) :=

^ :p0 ^ : h i > G # ( ; C) := C ^ :

G # ( : p; C) := p ^ : ^ C G # ( [ ]; C) := G( ; >) ^ C

G # ( : p[ ]; C) := p ^ : ^ G( ; >) ^ C provided that is the dual relation of , more precisely, = , and = ; and where p0 represents all other propositions distinct to the set of propositions is nite). = , ? = ?,

(recall

Since translation of paths consider a context represented by formulas, we now give a non-data version of formulas. Intuitively, context formulas are indistinguishably interpreted over data and non-data trees.

De nition 11 (Context formula). Given a formula in negated normal form, its corresponding context formula C is inductively de ned as follows: pC := p ( _ )C :=

C _

C (hmi )C := : ^ hmi C ( x: )C := ( # k)C := x: =x

C

C C # k (:p)C := : ^ :p

C )C := ( ^

^ ([m] )C := : ^ [m] C

C ( x: )C := x: =x

C Lemma 1. Given any data tree , for any formula and any valuation V , we have that C V = C TV ( ).

We now describe the main result of this paper: a characterization of regular paths with counting and data tests in terms of Presburger formulas. Theorem 2 (Logic characterization of data queries). For any RPQCD expression, data tree , TLIC context formula C , and any valuation V , we have the following: { [[ ]][ C] TV ( ) = F ; C TV ( ); and { F ; C is of polynomial size with respect to q and C .

An immediate consequence of Theorems 1 and 2 is an EXPTIME bound for RPQCD reasoning.

Corollary 1. Reasoning (emptiness, containment and equivalence) on regular path queries with counting and data tests (RPQCD) is in EXPTIME. 5

Discussion

We introduced an extension of regular path expressions with counting and data tests. Counting operators express occurrence restrictions on children path expressions, whereas data tests express (dis)equality relations among paths with respect to their data values. We give a characterization of the extension of regular paths in terms of a Presburger logic originally introduced in [ 7 ]. Since the characterization is polynomial and the logic is closed under negation, the EXPTIME bound of the logic is then imported for the emptiness, containment and equivalence of paths with counting and data tests. As a rst further research perspective we propose the study of the model checking problem of the Presburger logic (it is known a quadratic-time model checking algorithm for the logic without converse modalities [ 19 ]). This would imply complexity bound for the query evaluation of paths with counting and data tests. As another future work, we propose the study of further data test extensions of regular paths, in the setting of expressive modal logics with e cient reasoning Fischer-Ladner algorithms as in [ 7 ]. Acknowledgment. This work was partially developed under the support of the Mexican National Science Council (CONACYT) in the scope of the Catedras CONACYT project \Infraestructura para Agilizar el Desarrollo de Sistemas Centrados en el Usuario" (Ref 3053).

References

1. ten Cate, B. , Litak , T. , Marx , M. : Complete axiomatizations for xpath fragments . J. Applied Logic 8 ( 2 ) ( 2010 ) 153 { 172

2. Barcenas , E. , Geneves , P. , Layada, N., Schmitt , A. : Query reasoning on trees with types, interleaving, and counting . In: IJCAI, International Joint Conference on Arti cial Intelligence . ( 2011 )

3. Figueira , D. , Figueira , S. , Areces , C. : Model theory of xpath on data trees. part I: bisimulation and characterization . J. Artif. Intell. Res. (JAIR) 53 ( 2015 ) 271 { 314

4. Barcenas , E. , Lavalle , J.: Global numerical constraints on trees . Logical Methods in Computer Science 10 ( 2 ) ( 2014 )

5. Figueira , D. : On xpath with transitive axes and data tests . In: Symposium on Principles of Database Systems , PODS. ( 2013 ) 249 { 260

6. Figueira , D. : Decidability of downward xpath . ACM Trans. Comput. Log . 13 ( 4 ) ( 2012 ) 34

7. Barcenas , E. , Lavalle , J.: Expressive reasoning on tree structures: Recursion, inverse programs, Presburger constraints and nominals . In: Mexican International Conference on Arti cial Intelligence , MICAI. ( 2013 ) 80 { 91

8. Jacquemard , F. , Segou n , L., Dimino , J.: Fo2(<, +1, ~) on data trees, data tree automata and branching vector addition systems . Logical Methods in Computer Science 12 ( 2 ) ( 2016 )

9. Bojanczyk , M. , Place , T. : Toward model theory with data values . In: Automata, Languages, and Programming - International Colloquium , ICALP. ( 2012 )

10. Bojanczyk , M. , David , C. , Muscholl , A. , Schwentick , T. , Segou n , L.: Two-variable logic on data words . ACM Trans. Comput. Log . 12 ( 4 ) ( 2011 ) 27

11. Bojanczyk , M. , Muscholl , A. , Schwentick , T. , Segou n , L.: Two-variable logic on data trees and XML reasoning . J. ACM 56 ( 3 ) ( 2009 )

12. Figueira , D. : Forward-xpath and extended register automata on data-trees . In: Database Theory - ICDT , International Conference. ( 2010 )

13. Figueira , D. , Segou n , L.: Bottom-up automata on data trees and vertical xpath . In: Symposium on Theoretical Aspects of Computer Science , STACS. ( 2011 )

14. Dal-Zilio , S. , Lugiez , D. , Meyssonnier , C. : A logic you can count on . In: Symposium on Principles of Programming Languages, POPL . ( 2004 )

15. Seidl , H. , Schwentick , T. , Muscholl , A. : Counting in trees . In: Logic and Automata . ( 2008 )

16. Demri , S. , Lugiez , D. : Complexity of modal logics with presburger constraints . J. Applied Logic 8 ( 3 ) ( 2010 ) 233 { 252

17. Kupke , C. , Pattinson , D. , Schroder, L. : Reasoning with global assumptions in arithmetic modal logics . In: Fundamentals of Computation Theory, FCT . ( 2015 )

18. Bargun~o, L. , Creus , C. , Godoy , G. , Jacquemard , F. , Vacher , C. : Decidable classes of tree automata mixing local and global constraints modulo at theories . Logical Methods in Computer Science 9 ( 2 ) ( 2013 )

19. Barcenas , E. , Ben tez-Guerrero, E. , Lavalle , J.: On the model checking of the graded -calculus on trees . In: Mexican International Conference on Arti cial Intelligence , MICAI. ( 2015 )