Blaise Genest

Anca Muscholl

Olivier Serre

Marc Zeitoun

Tree Pattern Rewriting Systems

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Classical verification techniques often use abstraction when dealing with data. On the other hand, dynamic data-intensive applications have become pervasive, for instance with the ever growing importance of web services. The format of the data exchanged by web services is based on XML, which is nowadays the standard for semistructured data. XML documents can be seen as unranked trees, i.e. trees in which every node can have an arbitrary (but finite) number of children, not depending on its labels. Very often, the order of siblings in the document is of no importance. In this case, trees are in addition unordered. There is a rich body of results concerning the analysis of fixed XML documents (with or without data), see e.g [START_REF] Neven | Automata, Logic, and XML[END_REF][START_REF] Libkin | Logics for unranked trees: An overview[END_REF] for surveys on this topic.

The analysis of the dynamics of XML documents accessed and updated in a multi-peer environment has been considered only very recently [START_REF] Abiteboul | Positive Active XML[END_REF][START_REF] Abiteboul | Static Analysis of Active XML Services[END_REF]. Dynamically evolving XML documents are of course crucial, for instance when doing static analysis of XML-based web services. A general framework, Active XML (AXML for short), has been defined in [START_REF] Abiteboul | Positive Active XML[END_REF] to the purpose of unifying data (XML) and control (services), by allowing data to be given implicitly in form of service calls.

In this paper we propose an abstract model for dynamically evolving documents, based on guarded rewriting rules on unranked, unordered tree. We show that basic properties, such as reachability of tree patterns and termination, are decidable for a natural subclass of our rewriting systems.

A standard technique to analyze unranked trees is to encode them as binary trees [START_REF] Neven | Automata, Logic, and XML[END_REF]. However, this encoding does not preserve the depth of the tree, neither locality, nor path properties. For these reasons, we define our TPRS directly on unranked trees. The rewriting rules are based on tree patterns, occurring in two distinct contexts. First, tree patterns are used for describing how the structure of the tree changes through the rules (e.g. some subtrees might be deleted, new nodes can be added). Second, rules are guarded, and the guard condition is tested via a Tree Pattern Query (TPQ). The role of the TPQ is actually twofold: it is used in the pre-condition of the rule, and the results can enhance the information of the new tree. We call such a system Tree Pattern Rewriting System, TPRS for short. For an easier comparison with other works, we include an example of a Mail-Order System in our presentation, close to the one used in [START_REF] Abiteboul | Static Analysis of Active XML Services[END_REF].

The main tool we use to show decidability of various properties of TPRS are well-structured systems [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF]. Such systems cover several interesting classes of infinite-state systems, such as Petri nets and lossy channel systems. Our TPRS are of course not well-structured, in general. We impose two restrictions in order to obtain well-structure. First, guards must be used positively: equivalently, a rule cannot be disabled because of the existence of some tree pattern. Second, we need a uniform bound on the depth of the trees obtained by rewriting. Indeed, we show that if the depth is not uniformly bounded, then TPRS can encode Turing machines. We show that TPRS that satisfy both conditions yield well-structured transition systems, and we show how to apply forward and backward analysis of well-structured systems for obtaining the decidability of pattern reachability as well as of the termination. On the negative side, we show that exact reachability and the finite state property are undecidable for such TPRS. In the decidable cases, we also show that the complexity is at least non elementary.

Related work.

We review here other approaches where it is possible to decide interesting properties of transition systems based on unranked trees.

The systems considered in positive AXML [START_REF] Abiteboul | Positive Active XML[END_REF] are monotone: a document is modified by adding subtrees at nodes labeled by service calls. In particular, positive AXML documents can only grow. In the mail order example, it would mean that with positive AXML, one cannot delete a product from the cart. Moreover, there is no deterministic description of the semantics of a service: a service call can create any tree granted that it satisfies some DTD. Such a system is always confluent, and one can decide whether, after some finite number of steps, the system will stabilize.

Guard AXML [START_REF] Abiteboul | Static Analysis of Active XML Services[END_REF] is very similar to our model, service calls being based on tree pattern queries and the systems is non monotonous. However, the focus of [START_REF] Abiteboul | Static Analysis of Active XML Services[END_REF] is to cope with a sequence of service calls which always terminates, while we focus on modeling the whole life of the system, hence without enforcing termination. This allows [START_REF] Abiteboul | Static Analysis of Active XML Services[END_REF] to deal with potentially unbounded data (trees are labeled by symbols from an infinite alphabet and use data constraints) and unrestricted guards with negated patterns. In this paper, to keep decidability of e.g. pattern reachability in the non terminating non monotonous case, we need to define the basic steps of our model carefully, by using tree transformations in addition to tree pattern queries, instead of using general updating queries as in [START_REF] Abiteboul | Static Analysis of Active XML Services[END_REF]. Moreover, we disallow negated pattern or non upward closed guards. So the decidable fragment of Guard AXML is incomparable with our framework.

At last, term rewriting modulo associativty and commutativity has been prolific [START_REF] Dershowitz | Chapter 9 in: Handbook of Automated Reasoning[END_REF]. However, they usually treat slightly different questions: for instance, while they also use well quasi order (as Kruskal's), they focus on giving restrictions to ensure termination, while we impose restrictions only to ensure decidability of the termination. Reachability has been considered for non terminating systems, but only for ground rewriting [START_REF] Ch | Transition Graphs of Rewriting Systems over Unranked Trees[END_REF] (rules can only be applied at the deepest levels of the tree). Reachability is decidable for such systems [START_REF] Ch | Transition Graphs of Rewriting Systems over Unranked Trees[END_REF]. The rewriting used by [START_REF] Ch | Transition Graphs of Rewriting Systems over Unranked Trees[END_REF] is much more restrictive than in our framework. In the mail order example one could add and delete products inside an order but not refer to an order directly as it could contain an unbounded number of products (hence deleting the whole order in one step is not possible).

Tree Pattern Rewriting

The tree rewriting model presented in this section is inspired by the Active XML (AXML) system developped at INRIA [START_REF]Active XML[END_REF]. Active XML extends the framework of XML to describe semi-structured data by a dynamic component, describing data implicitly via service (function) calls. The evaluation of such calls is based on queries, resulting in extra data that can be added to the document tree. The abstract model is that of XML, i.e., unranked, unordered, labeled trees, together with a specification of the semantics for each service.

Trees as considered in this paper are labeled by tags from a finite set T . We will distinguish a subset T var ⊆ T of so-called tag variables. In addition, we use the special symbol $ to mark nodes where service calls insert new data. Trees are in the following unranked and unordered, with nodes labeled by T ∪ T $ , where T $ = T × {$}. We will not distinguish function/service nodes, since we consider here an abstract model for AXML documents, that is based on tree rewriting. We also do not consider multiple peers actually: their joint behavior can be described as the evolution of a unique document tree.

A tree (V, parent, root, λ) consists of a set of nodes V with a distinguished node called root, a mapping parent : V \ {root} → V associating a node with its parent, and a mapping λ : V → T ∪ T $ labeling each node by a tag. Moreover, for each node v ∈ V , there is some k ≥ 0 such that parent k (v) = root. Such a tree is called a document if its labeling satisfies λ(V ) ⊆ T \ T var , that is, if neither tag variables nor the $ sign are used as node labels. A forest is a finite multiset of trees.

Consider as an example the tree in Fig. 1. Informally, this tree represents a simplified version of the Play.com database, containing several products and information about customers. The subtrees of nodes v 5 and v 6 are not represented in the figure. The document has two customers, one of which is currently shopping on the website with one product in her cart. This customer has 3 outstanding orders, one of which was posted 2 days ago (the counter days is encoded in unary in the tree).

One represents a tree in a term-like way. For example, to denote the empty catalog with no customer, we write v 1 [Play.com](v 2 [MailOrder], v 3 [Catalog]), or if node names are irrelevant, [Play.com]([MailOrder], [Catalog]). Since trees are unordered, a tree can have several such representations.

The atomic operations in our model are from a set R of guarded tree rewriting rules, as described below. On an abstract level we view a service s as described for instance by a regular expression R(s) over the set of rewriting rules R. For example, the following expression describes an order service on play.com:

(add-product + delete-product ) * checkout
The tree resulting in the invocation of service s corresponds to the application of some sequence of rewriting rules in R(s). The atomic rewriting rules will use queries based on tree patterns (descendant relation can be used together with the son relation), as described next, standing for the union of disjoint sets .

Definition 1 (Tree-Pattern). A tree pattern (TP for short) is a tuple P = (V, parent, ancestor, root, λ), where (V, parent ancestor, root, λ) is a tree.

A tree pattern represents a set of trees that have a similar shape. As for trees, a TP can be described in a term-like way, ancestor-edges being represented by the symbol -(such edges are represented by a double line in the figures). For instance, the tree pattern LQBill shown in Fig. 2 can be written as w 1 (-w 2 (w 3 (w 4 ))), with λ(w 1 ) = Play.com, λ(w 2 ) = Ordered, λ(w 3 ) = X, λ(w 4 ) = Y , (here X and Y are tag variables: X, Y ∈ T var ). This pattern represents trees with root "Play.com", having a node "Ordered", having itself a grandchild.

Definition 2 (Matching).

A tree T = (V, parent, λ, root) matches a TP P = (V , parent , ancestor , λ , root ) if there exist two mappings f : V → V and t : T var → T \ T var such that:

-f (root ) = root, v1[Play.com] v2[MailOrder] v3[Catalog] v5[Customer] v4[Customer] v7[Product] v6[Product] v9[Ordered] v10[Ordered] v11[Posted] v12[Name] v13[Price] v15[LOTR] v16[skins] v22[£25] v19[skins] v20[£10] v23[£10] v17[day] v18[day] v8[Cart] v14[skins] v21[£10]
Fig. 1. A tree document representing a catalog of products and customers history.

-

For all v ∈ V , λ(f (v)) = λ (v) if λ (v) / ∈ T var , and else λ(f (v)) = t(λ (v)), -For all v ∈ V the following holds • If parent (v) is defined, then f (parent (v)) = parent(f (v)); • If ancestor (v) is defined, then f (ancestor (v)) is an ancestor of f (v) in T .
Mappings (f, t) as above are called a matching between T and P . Furthermore, if f is injective, then (f, t) is called an injective matching.

v1[play.com] v2[MailOrder] v3[Customer] v4[Customer] v5[Ordered] v6[LOTR] v7[£25] w1[play.com] w2[Ordered] w3[X] w4[Y] f f f f node node
T' LQBill Fig. 2. A tree T matching the TP LQBill.

Fig. 2 shows an example of an injective matching between a tree and the TP LQBill. The only possible matching is f (w 1 ) = v 1 , f (w 2 ) = v 5 , f (w 3 ) = v 6 , f (w 4 ) = v 7 and t(X) =LOTR, t(Y ) = £25. With a matching f : V → V we associate the mapping node : V \ f (V ) → f (V ) with node(v) being the lowest ancestor of v in f (V ). For instance, for the mapping f matching

T to P , node(v 2 ) = node(v 3 ) = node(v 4 ) = v 1 .
Similarly to [START_REF] Abiteboul | Positive Active XML[END_REF] we use in our model tree-pattern queries (TPQ for short, also called positive queries in [START_REF] Abiteboul | Positive Active XML[END_REF]). Such queries have the form Q ; P , with Q a TP and P a tree, and the variables used in Q are also used in P . The TP Q selects tags in the tree. The result of a query = Q ; P on T is the forest query(T ) of all instantiations of P by matchings between T and Q. That is, for each matching (f, t) between T and Q we obtain an instance of P in which each T var -label X has been replaced by the tag t(X). For instance, let RQBill be the tree Product (Name(X),Price(Y)). Then the result of the TPQ (LQBill ; RQBill) on the tree in Fig. 1 is the forest depicted in Fig. 3.

We now define a generic kind of (guarded) rewriting rules, as a model for active documents. Our rules are based on tree patterns, that occur in two distinct contexts. First, tree patterns are used for describing how the structure of the document tree changes through the rule -some subtrees might be deleted, new nodes can be added. Second, rules are guarded, and the guard condition is tested via a TPQ. The role of the query is actually twofold: it is used in the pre-condition of the rule, and the result can enhance the information of the new tree.

r1[Product] r2[Name] r3[Price] r4[LOTR] r5[£25] r6[Product] r7[Name] r8[Price] r9[skins] r10[£10]
Fig. 3. Forest produced as the result of the TPQ LQBill ; RQBill on document T .

Definition 3 (TP rules).

A TP rule is a tuple (left, query, guard, right), such that:

-left is a TP (V l , parent l , ancestor l , λ l , root l ) over T , -right is a TP (V r , parent r , ancestor r , λ r , root r ) over T ∪ T $ , -query is a TPQ, -guard is a set of forests.
We require the following additional properties:

1. all tag variables used in right appear also in left and 2. ancestor r (x) = y iff x, y ∈ V l ∩ V r and ancestor l (x) = y. The additional conditions on right ensure that the right-hand side of a TP rule determines the form of the resulting tree, as it is explained below. For instance, Bill = (left, (LQBill ; RQBill), guard, right) is a TP rule, with left, right defined as in Fig. 4. Informally, the rule says that the system will process a Bill of the current order, and will tag the order as processed. The guard guard will be usually specified as a finite set of trees. In this case, the guard is fulfilled if the result of the query covers one of the tree of guard (see the decidable section 4).

We first describe the semantics of a rule using the rule Bill as an example on the tree in Fig. 1. First, we compute an injective mapping f which maps the nodes w 1 , w 5 , w 2 of left with the nodes v 1 , v 4 , v 10 of T , respectively. We produce a new tree by rearranging and relabeling the nodes of T in the image of f , that is v 1 , v 4 , v 10 . Some nodes can be deleted and others created. The resulting tree is shown in Fig. 5. We keep all nodes of T which are matched by nodes of left

v1[Play.com] v2[MailOrder] v3[Catalog] v5[Customer] v4[Customer] v7[Product] v6[Product] v9[Ordered] w6[Processed] v11[Posted] v12[Name] v13[Price] v15[LOTR] w7[Bill] v22[£25] v19[skins] v20[£10] v17[day] v18[day] v8[Cart] v14[skins] v21[£10] r6(Product) r7(Name) r8(Price) r9(skins) r10(£10)
Fig. 5. The tree document T resulting of the application of the rule Bill. also present in right (v 1 , v 4 ), as well as their descendants by node -1 . That is, we keep all nodes labeled by v i in Fig. 5. In particular, a node matched in left which does not appear in right is deleted (as v 10 , matched to w 2 ), as well as its node -1 descendants (v 16 , v 23 ). The TP right makes it possible to create new nodes, present in right but not in left, as w 6 , w 7 . In addition, the TPQ query of the rule is used to attach a copy of the returned forest to all $-marked nodes of right. Furthermore, if the TPQ Q ; P uses in Q node name m common to left, then the results of the TPQ are restricted to those where m matches f (m). For instance, in the TP rule Bill, the TP LQBill uses names w 1 , w 2 common to left, hence the result of the TPQ (LQBill ; RQBill) are restricted to the particular order chosen by the matching f between T and left. The result is thus the subtree of node r 6 in Fig. 3, but not the subtree of node r 1 , since it would require f (w 2 ) = v 9 , while f (w 2 ) = v 10 . This restriction is desirable, since we want to process a bill only of the products of this particular order. Here, w 7 is $-marked, and the result forest is defined by nodes r 6 , • • • r 10 . More formally, let query = Q ; P be a TPQ and let (f, t) be an injective matching between T and left. Moreover, let V l be the nodes of left and V Q those of Q. Let S 1 , . . . , S k be the trees composing the resulting forest query(T ), and let g 1 , . . . , g k be the respective associated matchings (that is, g i : V Q → V and S i is the instantiation of P by g i ). Then we define query f (T ) as the forest S i1 , . . . , S i l of those trees S j such that g j agrees with f over V l ∩ V Q . That is, query f (T ) is the subset of query(T ) that is consistent with the matching f . We now turn to the formal semantics of rules.

Definition 4 (Semantics of rules). Let T = (V, parent, λ, root) be a tree and R = (left, query = Q ; P, guard, right) be a rule, where left = (V l , parent l , ancestor l , λ l , root l ) and right = (V r , parent r , ancestor r , λ r , root r ).

We say that R is enabled if there exists an injective matching (f, t) from left into T , such that query f (T ) ∈ guard. The result of the application of R via (f, t) is the tree T = (V , parent , λ , root ) defined as follows:

-V = V 1 V 2 V 3 V 4 with 1. V 1 = f (V l ∩ V r ), % in the example on Fig. 5, V 1 = {v 1 , v 4 } 2. V 2 = node -1 (V 1 ),
% in the example on Fig. 5,

V 2 = {v i | i / ∈ {1, 4}} 3. V 3 = f (V r \ V l ),
% in the example on Fig. 5, V 3 = {w 6 , w 7 } 4. V 4 consists of distinct copies of the nodes of the forest query f (T ), one for each node marked by $ in right. % in the example on Fig. 5,

V 4 = {r i | i ∈ {6, . . . , 10}} -Setting f (u) = u for all u ∈ V 3 , we extend f : V r ∪ V l → V 1 V 3 . -root = f (root r ). -Let u ∈ V 1 and let ū = f -1 (u) be the associated node in V l ∩V r . If λ r (ū) / ∈ T var then λ (u) = λ r (ū), else λ (u) = t(λ r (ū)). For all u = root , if parent r (ū) is defined, then parent (u) = f (parent r (ū)) else parent (u) = parent(u). -For all u ∈ V 2 , parent (u) = parent(u) and λ (u) = λ(u). -For all u ∈ V 3 \ {root r }, parent (u) = f (parent r (u)) and λ (u) = λ r (u).
-To each node u ∈ V marked by $, we add a copy of the forest query f (T ) as children of u, and we unmark the node.

Note that if x ∈ V 2 , then its parent is in V 1 ∪ V 2 .
The same stands if ancestor r (x) is defined. Note also that we indeed obtain a tree: for instance, if u ∈ V 1 and parent r (ū) is not defined, then parent(u) is defined. This is because v = ancestor r (ū) is then defined, so by Def. 3, v = ancestor l (ū) in left, so that u = f (ū) cannot be the root of T .

We write T R → T if T can be obtained from T by applying the rule R. More generally, given a set of rules R we write T → T if there is some rule R ∈ R with T R → T , and T * → T for the reflexive-transitive closure of the previous relation. Notice that the tree T matches right, through the matching f :

V r → V defined by f (v) = f (v) if v ∈ V r ∩ V l , and f (v) = v if v ∈ V r \ V l .
Remark 1. Positive AXML systems [START_REF] Abiteboul | Positive Active XML[END_REF] are covered by our model except for one detail: in [START_REF] Abiteboul | Positive Active XML[END_REF], positive queries can address not only the document tree, but also specific subtrees, such as the subtree of a service call, or the subtree of its parent. However, such queries on subtrees can be expressed easily in our formalism. An AXML service call corresponds to a rule (left, query, guard, right) with left = right = r(-(v(w))), where w is labeled by a function tag. In addition, node v in right is marked by $ (since it collects the result of query as new subtrees). A positive AXML TP P that is matched against the subtree of w can be rewritten into a TP root(-P ), where P is obtained from P by renaming the root node into w.

Example (Play.com rules).

To show how easily rules can be defined, we describe now the other rules of the Play.com system. When the rule does not use a query or a guard, we only describe the left and right components.

-The rule New-Customer adds a new customer and its cart.

• left = w 1 [Play.com](w 2 [MailOrder]) • right =w 1 [Play.com](w 2 [MailOrder](w 3 [Customer](w 4 [Cart]))).
-The rule Delete-Product deletes a product from a cart.

• left = w 1 [Play.com](-w 7 [Cart](w 8 [X](w 9 [Y])) • right = w 1 [Play.com](-w 7 [Cart]
). -The rule Add-Product adds a new product to the cart of a customer.

• left = w 1 [Play.com](-w 2 [Product](w 3 [Name](w 4 [X]),w 5 (Price)(w 6 [Y])), -w 7 [Cart]) • right = w 1 [Play.com](-w 2 [Product](w 3 [Name](w 4 [X]),w 5 (Price)(w 6 [Y])), -w 7 [Cart](w 8 [X](w 9 [Y])).
-The rule Checkout can turn the cart into an order.

• left = w 1 [Play.com](-w 2 [Cart]) • right = w 1 [Play.com](-w 2 [Ordered]
) -As long as the bill is not processed, the customer can cancel her order with the rule Cancel.

• left = w 1 [Play.com](-w 2 [Ordered])
• right = w 1 [Play.com] -A processed order can be posted, and we count in unary the number of days since it was sent using day.

• left = w 1 [Play.com](-w 2 [Processed]) • right = w 1 [Play.com](-w 2 [Posted](w 3 [day])) -A posted parcel can be received. • left = w 1 [Play.com](-w 2 [Posted]) • right = w 1 [Play.com](-w 2 [Received]
) -Every new day, if a posted parcel has not yet been received yet, then the day counter is incremented.

• left = w 1 [Play.com](-w 2 [Posted]) • right = w 1 [Play.com](-w 2 [Posted](w 3 [day]
)) -If after 21 days a posted parcel is still not received, the customer can require a payback. We use the guard to ensure this time limit. Notice that the query is Q ; P , where Q uses the same w 2 as in left, that is the number of days will be counted only for this particular parcel.

• left = w 1 [Play.com](-w 2 [Posted]) • Q= w 1 [Play.com](-w 2 [Posted](w 3 [day]) • P = x 4 [day]
• guard: a forest containing at least 21 trees with root labeled day (and possibly more nodes).

• right = w 1 [Play.com]
Notice that we could model a stock by using tokens for each product in stock below its name in the catalog, decrementing the token when a product is added to cart and incrementing the token when it is deleted from cart. Also, a query could cancel a particular approvisioning from a manufacturer from some product when the stock is greater than some treshold.

Static Analysis of TPRS

We assume from now on that an active document is given by a tree pattern rewriting systems (TPRS) (T, R), consisting of a set R of TP rules and a Tlabeled tree T . That is, we assume that each service corresponds to a rule. Our results are easily seen to hold in the more general setting where services are regular expressions over R.

A tree T with node set V is subsumed by a tree T with node set V , noted T T , if there is an injective mapping from V to V that preserves the labeling, the root, and the parent relation. A forest F is subsumed by a forest F , written F F , if F is mapped injectively into F such that each tree in F is subsumed by its image in F . Similarly, a TP P with node set V is subsumed by a TP P with node set V , if there is an injective mapping from V to V that preserves the labeling, the root, the parent and the ancestor relations.

With a TPRS (T, R) we can associate the (infinite-state) transition system S(T, R), → with S(T, R) = {T | T * → T }. We are interested in checking the following properties:

-Termination: Are all derivation chains T → T 1 → T 2 → • • • of (T, R) finite? -Finite-state property: Is the set S(T, R) of reachable trees finite? -Reachability: Given (T, R) and a tree T , is T reachable in (T, R)? -Confluence (also called Joinability): For any pair of trees T 1 , T 2 ∈ S(T, R), does there exist some T such that T 1 * → T and T 2 * → T ? -Pattern reachability (coverability): Given (T, R) and a tree pattern P , does T * → T hold for some T matching P ? -Weak confluence: From any pair of trees T 1 , T 2 ∈ S(T, R), does there exist

T 1 T 2 such that T 1 * → T 1 and T 2 * → T 2 ?
For instance, pattern reachability is a key property when we want to talk about the reachability of some pattern. For example, we might ask whether an already cancelled order could be still delivered, which would mean a problem in the system. For this it suffices to tag cancelled orders with a special symbol #, and check for the pattern w 1 [Play.com](-w 2 [delivered](w 3 [#])). It is the same kind of properties which are checked in [START_REF] Abiteboul | Static Analysis of Active XML Services[END_REF]. As expected, any of the non-trivial questions above is undecidable in the general case, see Theorem 1 below.

We are thus looking for restrictions that lead to the decidability of at least some of these problems.

In the next section we consider a subclass of TPRS, which is a special instance of the so-called well-structured systems. We say that (T, R) is positive if all guards occurring in the rules from R, are upward-closed. This means for every guard G, and all forests F, F with F F , that F ∈ G implies F ∈ G, too. In particular, if a rule R in a positive system is enabled for a tree T , then R is enabled for any tree T that subsumes T . The reason is that for any TPQ query, we have that for every tree T 1 in query(T ) there is some tree T 1 in query(T ) such that T 1 is subsumed by T 1 . Notice that positive TPRS allow deletion of nodes, so they are more powerful than the positive AXML systems considered in [START_REF] Abiteboul | Positive Active XML[END_REF].

The theorem below shows that upward-closed guards alone do not suffice for obtaining decidability of termination: Theorem 1. Any two-counter machine M can be simulated by a positive TPRS (T, R) in such a way that M terminates iff (T, R) terminates.

Proof. Let M be a two-counter machine with control state set Q and counters c and d. In the sequel, a configuration of M , i.e. a tuple (q, x, y) ∈ Q×N×N where x and y respectively denote the value of counter c and d, will be represented by a tree whose root is labeled by q, which has two children, respectively labeled by c and d. The tree rooted at the node labeled c (respectively d) is formed of a single path containing x (respectively y) intermediate nodes labeled by i (as internal) and ending by a leaf labeled ⊥. We denote the previous tree by T (q,x,y) .

Without loss of generality we may assume that any transition of M requires the value of each counter to be either zero or non-zero (this can be enforced by inserting a zero test before each transition).

Each possible transition of M is modeled by a rewriting rule. For instance a transition enabled in state q with c being non-zero and d being zero that goes to state q , decrementing the counter c and incrementing the counter d, is simulated by the rule with left = root(u(w(t)), v(t )) and right = root (u(t), v(z(t ))), where root is labeled by q, root is labeled by q , u is labeled by c, v is labeled by d, w and z are labeled by i, t is labeled by * and t is labeled by ⊥. One defines similar rules for other possible transitions in M . Note here that our rules have no query/guard part, hence the system is positive.

It follows directly from the definition of the rules that a configuration (q , x , y ) is reachable in M from some configuration (q, x, y) iff T (q,x,y) * → T (q ,x ,y ) . 2

Remark 2. The TPRS defined in the previous proof uses rules that can erase nodes (and their subtrees). Technically we could avoid deletions by adding a special garbage node to which we attach all nodes of left that do not occur in right.

Theorem 1 shows that any non trivial property is undecidable for positive TPRS without further restrictions. However, notice that the above proof needs trees of unbounded depth. A realistic restriction in the XML setting is to consider only trees of bounded depth: XML documents are usually large, but shallow. A TPRS (T, R) is called depth-bounded, if there exists some fixed integer K such that every tree T with T * → T has depth at most K. Of course, Theorem 1 implies that it is undecidable to know whether a TPRS is depth-bounded. However, in many real-life examples this property is easily seen to hold (see e.g. the Play.com example, which has depth at most 8).

Decidability for positive and depth-bounded TPRS

For positive and depth-bounded TPRS we can apply well-known techniques from the verification of infinite-state systems that are well-structured. Well-structured transition systems were considered independently by [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF] and they cover many interesting models, such as Petri nets or lossy channel systems. We recall first some basics of well-structured systems. Definition 5. A well-quasi-order (wqo) on a set X is a preorder such that in every infinite sequence (x n ) n≥0 ⊆ X there exist some indices i < j with x i x j .

In general, the "subsumed" relation on the set X of T -labeled trees is not a wqo. 1 However, using Higman's lemma (see, e.g., [6, Chap. 12]), one can show that is a wqo on the set of trees of depth at most K (for any fixed K): Proposition 1. Fix K ∈ N, and let X K denote the set of unordered T -labeled trees of depth at most K. The "subsumed" relation ⊆ X K × X K is a wqo.

Proof. It is easy to see that the relation is a preorder. We show the second property by induction on K ≥ 0. Let K > 0 and consider an infinite sequence of trees T 1 , T 2 , . . . of depth at most K. We find a subsequence T i1 , T i2 , . . . of trees with the same root label a. Each such tree T ij consists of the root a, plus a multiset S ij of trees of depth at most K -1. By induction, (X K-1 , ) is a wqo. Higman's lemma states that whenever (X, ) is a wqo, we have that (X * , ) is a wqo, too. In particular, the set of multi-sets over X together with , is a wqo. Thus, we can find some j < k such that S ij S i k , thus T ij T i k .

2

By the previous lemma, a positive and depth-bounded TPRS (T, R) yields a well-structured transition system S(T, R), → as defined in [START_REF] Finkel | Well-structured transition systems everywhere![END_REF] (see also 2 [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF]). This follows from the transition relation → being upward compatible: whenever T R → T and T T 1 , there exists T 1 with T 1 R → T 1 and T T 1 . For the next theorem we need first some notation. Given a set X and a preorder , we denote by ↑X the upward closure {T | T T for some T ∈ X} of X. By min(X) we denote the set of minimal elements 3 of X. Finally, by Pred(X) we denote the set of predecessors of elements of X. Note that whenever the transition relation → is upward compatible and X upward-closed, the set Pred(X) is upward-closed, too.

Since the subsumed relation is a wqo, the relation on forests is a wqo as well. Thus, each guard G in a positive, depth-bounded TPRS (T, R) can be described by the (finite) set of forests min(G). The size |G| of G is the maximal size of a forest in min(G).

Theorem 2. Termination and pattern reachability are both decidable for positive and depth-bounded TPRS.

1 Indeed consider the sequence of trees (Tn) n≥0 where for each n ≥ 0, Tn is the tree formed by a single branch of length n + 1 whose internal nodes are labeled by a and the unique leaf is labeled by b. 2 As shown in the proof of Thm. 2, S(T, R), → is also well-structured as defined in [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF], which requires in addition that the set of predecessors of upward-closed sets is effectively computable. 3 For a wqo (X, ) and Y ⊆ X, the set min(Y )/∼ is finite, where ∼ = ∩ -1 . For the subsumed relation , note that ∼ is the identity.

Proof. First, termination is decidable for well-structured systems such that 1) is decidable, 2) → is computable and 3) upward compatible, see [START_REF] Finkel | Well-structured transition systems everywhere![END_REF]Thm. 4.6]. For pattern reachability, it is easy to see that the set of trees of depth bounded by some K which matches a TP P is upward-closed, and that the set of its minimal elements is effectively computable. We can thus use [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF], which shows decidability of the reachability of ↑T under the assumption that the set min(Pred(↑T )) is computable. This allows to use the obvious backward exploration algorithm. From now on we fix the tree T and the bound K of the system (T 0 , R). Let us also fix a rule R = (left, query, guard, right).

It suffices to consider the finite set S R (T ) of all trees T of size at most

|T | + |left| + K|query||guard| with T R -→ T .
Then, defining M as the set of minimal elements of R∈R S R (T ), we get by definition M ⊆ min(Pred(↑T )).

Let us now show that M = min(Pred(↑T )). Let T 1 ∈ min(Pred(↑T )). Thus, there exist some rule R and some injective matching (f, t) with T 1 R -→ T via (f, t). Let also F ∈ min(guard) be a forest with F F , where F is the result of query on T 1 (compatible with the matching f ).

The nodes of T 1 can be partitioned into 4 sets V 1 , V 2 , V 3 , V 2 (below V l are the nodes of left and V r those of right):

1. V 1 = f (V l ∩ V r ), 2. V 2 = node -1 (V 1 ), 3. V 3 = f (V l \ V r ), 4. V 2 = node -1 (V 3 ). Notice that V 1 and V 2 are common with T (see Def. 4), hence |T 1 | ≤ |T | + |V 3 | + |V 2 |. Now, |V 3 | ≤ |left|.
We now explain that V 2 has at most |query||guard| leaves, hence |V 2 | ≤ K|query||guard| which shows that T 1 ∈ S R (T ). Otherwise one can delete a leaf from V 2 and get a tree T 1 T 1 with T 1 R -→ T (via (f, t)), and still F F , where F denotes the result of query on T 1 . This contradicts the minimality of T 1 .

2 On the negative side, depth-bounded well-structured systems can simulate reset Petri nets (i.e., nets with an additional transition that empties a place), hence we can deduce the following from known results: Theorem 3. Exact reachability, confluence, weak confluence and the finite-state property are undecidable for positive and depth-bounded TPRS.

Proof. We encode a reset Petri net with n places (p i ) i≤n by a well-structured system with K = 2. Namely, we consider trees with root labeled r and with n children labeled p i . Each node p i has as many children as p i has tokens and the leaves are all labeled by t.

Each transition is modeled by a rule. For instance, a reset of place p i is modeled by the rule with left = root(v), right = root(w), where root is labeled r and both v and w labeled by p i (the rule has an empty query/guard part). Applying such a rule preserves the root, but the subtree whose root is labeled by p i is destroyed, and a new child of root is created with the label p i , and this node has no child. A rule which takes 2 tokens from place p i and one from place p j and creates a token in place p k is modeled as left = root(v(w, x), y(z), s), right = root(v, y, s(u)), with root, v, y, s labeled respectively by r, p i , p j , p k , and w, x, z, u are labeled by t.

It directly follows from the construction that the previous TPRS system is depth-bounded and positive. As both exact reachability and the finite-state property are undecidable for reset Petri nets [START_REF] Dufourd | Reset Nets between Decidability and Undecidability[END_REF], it follows that this holds for positive and depth-bounded TPRS as well.

We now show the undecidability of (weak) confluence for a reset Petri net, which hence implies the undecidability for positive and depth-bounded TPRS. For this, we reduce reachability to the confluence of a reset Petri net.

The question is whether a marking M f can be reached in a reset Petri net P from the initial marking. We create a new reset Petri net P with the same places as P , plus two new places q, r. The initial marking of P is the same as for P , and there is one token in place q and zero in place r.

For two markings M, M , we denote by (M, M ) the transition with M (a) tokens taken from place a, and M (a) tokens added to place a, for all a. For instance, the transition ({p, 2 • q}, {p, s, t}) checks that there are at least one token in place p and two in q, it deletes two tokens from place q, and adds one to both s and t.

For each transition (M, M ) of P , there is a transition (M + {q}, M + {q}) in P . We fix a place p of P . We add the three transitions (M f + {q}, {r}), ({q}, {r, p}) and ({r, 2 • p}, {r, p}), plus a transition ({r, l}, {r, p}) for all places l / ∈ {p, q, r}.

First, note that in each reachable marking of P , there is either a token in q or in r (but not both), and no marking with a token in q is reachable from a marking with a token in r. Second, every marking except {r} can reach {r, p}. Indeed, if the marking has a token in q, then it can first execute the transition ({q}, {r, p}). With a token in r, each place other than r, p can be emptied with ({r, l}, {r, p}) (and p is sure to be non-empty). Then all tokens in p but one can be deleted with ({r, 2 • p}, {r, p}). Also, notice that {r} is reachable in P iff M f is reachable in P . The reason is that from any marking M with M (r) = 1 and M = {r} we cannot reach {r}.

Therefore P is confluent iff {r} is not reachable in P iff M f is not reachable in P . As P is weakly confluent iff it is confluent, this concludes the proof. 2

On the positive side, we can show that the finite-state property is decidable for positive, depth-bounded TPRS, that are strict, i.e., for any rule (left, query, guard, right), we require V left ⊆ V right . One cannot encode reset Petri nets with such systems because deletion is no longer possible (actually one can only relabel an existing node and create new nodes). Strict systems enjoy the additional property that whenever T R → T and T ≺ T 1 , there exists T 1 with T 1 R → T 1 and T ≺ T 1 (notice that for non strict systems, we can only guarantee that T T 1 ). The results from [START_REF] Finkel | Well-structured transition systems everywhere![END_REF] yield the following theorem.

Theorem 4. The finite-state property and reachability are decidable for TPRS that are positive, depth-bounded, and strict.

Note that the finite-state property is not very interesting in itself, but if it holds, then the other problems become decidable as we are dealing with a finitestate system. In particular, in order to test for confluence, it suffices to test that (S(T, R), →) has a unique maximal strongly connected component.

Note that reachability is decidable for positive, depth-bounded and strict TPRS simply because T → T implies that |T | ≤ |T |, and then it suffices to look for reachability of a tree T 1 in the finite state system {T | |T | ≤ |T 1 |}.

The undecidability of confluence and weak confluence for positive, depthbounded and strict TPRS follows from Theorem 3 together with a simple technical modification: insted of deleting nodes (and their subtrees) we attach them to a special garbage node #. Additional rewriting rules ensure that at any moment, arbitrary descendants of the garbage node can be created. These rules ensure confluence, since for any subtrees T 1 , T 2 of # (of bounded depth) we can rewrite both T 1 , T 2 into some (larger) tree T 3 .

Below is a table that sums up the results we obtained so far. It presents (un)decidability results concerning the various classes of positive TPRS we considered (depth-bounded and strict). The negative results about strict TPRS come from Theorem 1 (see subsequent remark). Term., FS, Reach., P-reach, Confl. and W-confl. stand respectively for termination, finite state property, reachability, pattern reachability, confluence and weak confluence.

Model

Term. FS Reach. P-reach. Confl. W-confl.

Strict U U U U U U Depth-Bounded D U U D U U Depth-Bounded & Strict D D D D U U
Table 1. Decidability results for positive TPRS.

Lower bounds and extensions

Decidability results are obtained with non-constructive proofs coming from Higman's Lemma. This ensures termination of the algorithms, but without yielding complexity bounds. It is thus relevant to obtain lower bounds for these results.

Theorem 5. The following problems have at least non-elementary complexity:

-Input: A TP P , a TPRS system (S, R) and an integer k such that the depth of (S, R) is bounded by k. -Problem1: Is the pattern P reachable in (S, R)? -Problem2: Does (S, R) terminate, equiv., does it have an infinite path? Proof. Let tower(0, n) = n and tower(k + 1, n) = 2 tower(k,n) . Let M be an n → tower(k, n)-space bounded deterministic Turing machine and x be an input of M . Denote by log * n the smallest integer m such that n ≤ tower(m, 2) and let K = k + log * |x|, so that the computation of M on x uses at most tower(k, |x|) ≤ tower(K, 2) tape cells. We build a (K + 1)-depth bounded TPRS of size O(|M | + |x|) simulating M on x.

Informally, we encode each configuration of M by a tree. Each cell is encoded by a subtree of the root, labeled at its own root by the cell content, with the forest below it encoding the position of the cell. Since such a position is smaller than tower(K, 2), it can itself be encoded recursively by a forest of depth at most K (such a recursive encoding of large integers, by words, has already been used in [START_REF] Walukiewicz | Difficult Configurations-on the Complexity of LTrL[END_REF]). For instance, one can encode integers from 0 to 15 = tower(2, 2) -1 at depth 2. The forest of Fig. 6 encodes 13 (1101 in binary). To recover its position, each bit of the base 2 representation has under itself a forest of depth 1 encoding its position (recursively with the same encoding scheme). For instance, the leftmost 1 is at position 00, which is encoded by the forest

{[0]([0]), [0]([1])}. [1] [1] [0] [1] [0] [0] [0] [1] [1] [0] [1] [1] [0] [1] [0] [1] [0] [1] [0] [1]
Fig. 6. A level 2 counter encoding 13.

Formally, a level 0 counter consists of a single node labeled by 0 or 1. We define inductively a level counter as a forest of tower( -1, 2) trees, each of depth , to encode any integer between 0 and tower( , 2) -1. The level counter encoding i ≤ tower( , 2) -1 will be noted F i (for = 0: F 0 0 = {0}, F 0 1 = {1}). Assume inductively that F -1 i has been defined for 0 ≤ i ≤ tower( -1, 2) -1. For 0 ≤ j ≤ tower( , 2) -1, let a 0 • • • a p be the binary representation of j, with p = tower( -1, 2)-1. The level counter F j is the forest {

[a i ](F -1 i ) | 0 ≤ i ≤ p}.
Let N = tower(K, 2) -1. We encode the configuration C of M with tape content a 0 • • • a N , current state q and scanned position m, by the forest

F C = ā0 (F K 0 ) • • • āN (F K N ) of depth K + 1, with ām = [a m
, q] and āi = [a i ] for i = m. The head position is thus doubly tagged: by the letter, and by the state. Such a node with a double tag [α, β] is said marked by β, or a β-node.

In order to navigate through the cells, we use for each level ≤ K an additional placeholder node, child of the root, named c for holding a level counter below it. The idea is that the counter attached below c K will be able to count up to N , and hence can pinpoint a tape position. The other counters are needed in the inductive process. During the computation, additional markers will be used either as pebbles, or to guide the control. Figure 7 shows a typical tree reached during the computation. The rules of the TPRS are set up so that it performs successively the following actions: -increment( ) increments the level counter below c .

-compare( ) compares level counters below c and below the * -marked node.

-test-max( ) tests if the level counter below c has its maximal value.

-zero( ) generates under c the level counter F 0 .

Each task of level will be implemented using a sequence of tasks of level ( -1), plus some fresh tags to correctly organize the order of these level ( -1) tasks.

Let us explain how to handle the control. First, each function of level only performs local tasks, or calls to functions of level -1. Therefore, the underlying call stack size is K-bounded. The first tasks to be called are those of level K (recall that we aimed at checking that the head was correctly placed, thus having to handle level K counters). The call stack is simulated by markers put at the c i nodes. When the activated function is at level , nodes c 0 , . . . , c -1 are all marked ready,true or false, while nodes c , . . . , c K have other marks indicating an "active" state. For instance at the beginning of the simulation, c K is marked run while for < K, c is marked ready. This way, a left side of the form r[M ](u[c -1 , ready], v[c , x]) for some tag x = ready selects the counter where the current action is to be performed.

As an example, compare( ) works by running a level -1 counter from 0 to its maximal value, using zero( -1), increment( -1) and test-max( -1). For each value k of this counter, it compares the k-th bits of the level counters under comparison, by nondeterministically marking one bit of each counter, verifying with compare( -1) and compare ( -1) that they are at position k, and if so, comparing them. The call compare( ) is activated when c is tagged compare. We use as tags either names of functions to be called (compare, zero, etc.), "return values" (true, false, ready), or control states (cmp-guess-1st-bit,. . . ). Notice that we use another operator compare ( ) to compare bits marked * and the counter under c . Formally:

-Initialize level -1 counter to 0, by marking c -1 by zero, to "call" zero( -1):

•

left = r[M ](x[c -1 , ready], y[c , compare]) • right = r[M ](x[c -1 , zero], y[c , cmp-guess-1st-bit]).
-Guess and mark by * -1 a bit below * . Check the guess with compare( -1): The rules for other tasks follow the same ideas and are not described here. 2

• left = r[M ](x[c -1 ,
The bounded depth restriction needed for our decidability results can be relaxed if we forbid the use of the direct parent-child edges in tree patterns. This leads to the following preorder on unranked, unordered T -labeled trees, which is a well quasi-order by Kruskal's theorem (see [START_REF] Diestel | Graph theory[END_REF]Chap. 12]). For two trees T, T with sets of nodes V, V respectively, we write T T , if there is an injective mapping from V to V that preserves the labeling, the root, and the ancestor relation. So compared to the relation used previously, we do not require that the parent relation is preserved.

Clearly, we need to restrict the TPRS rules in order to obtain well-structured systems. Namely we require that all TP occurring in query and left use only ancestor edges (right can still use parent edges, but the parent relation cannot be tested for). We call such TPRS undirected. Using similar proofs as in Sect. 4, we get the same results as in Table 1. For the lower bound we obtain a stronger result, by encoding reachability for lossy channel systems (LCS). These are finite-state machines communicating over FIFO channels that can loose arbitrary many messages. Reachability for LCS has non primitive recursive complexity [START_REF] Ph | Verifying Lossy Channel Systems has Nonprimitive Recursive Complexity[END_REF], already for LCSs made up of two finite-state machines and two channels [START_REF] Chambart | The Ordinal Recursive Complexity of Lossy Channel Systems[END_REF]. Theorem 6. Termination and pattern reachability have at least non primitive recursive complexity for undirected TPRS.

Proof. We reduce the reachability of some global control state of an LCS to the pattern reachability of an undirected TPRS. Fix an LCS made up of two finite-state machines A 1 , A 2 communicating through two lossy FIFO channels (C 1 from A 1 to A 2 and C 2 in the opposite direction).

A configuration of the LCS is given by (q 1 , q 2 , w 1 , w 2 ), where q i is the current state of A i and w i ∈ Σ * is the content of channel C i . We encode this configuration by the following tree, where for instance w 1 = a • • • c. Channel tails, where writes occur, are marked by [end]. The rules associated with such a system are given below, assuming disjoint state sets for A 1 and A 2 , that do not contain symbols C1, C2. Notice that we do not use any query/guard part. One can assume that message losses happen just before read actions, ahead of the message actually read in that channel.

-A message loss possibly occurs at the head of channel C 1 , a message a is then read in C 1 by A 2 , which switches its state from q 2 to q 2 : • left = w 1 [LCS](-w 2 [q 2 ], -w 3 [C1](-w 4 [a])),

• right = w 1 [LCS](-w 2 [q 2 ], w 4 [C1]). -A 1 performs a transition from state q 1 to q 1 , sending message a into C 1 :

• left = w Dual rules are defined for A 2 . It should be clear that there is a bisimulation between the undirected TPRS system and the LCS, which yields the result. 2

Fig. 4 .

 4 Fig. 4. Tree patterns left and right of a rule.

1 .

 1 It creates the forest F C0 , and attaches it under the root, leaving c K labeled by [c K , run] and for < K, c labeled by [c , end].

  ready], y[c , cmp-guess-1st-bit], -t[T, * ](u[U ])), • right = r[M ](x[c -1 , compare], y[c , cmp-guess-2nd-bit], -t[T, * ](u[U, * -1 ])).

---

  Guess and mark by * -1 a bit below c . Check the guess with compare ( -1):• left = r[M ](x[c -1 , true], y[c , cmp-guess-2nd-bit](z[Z])), • right = r[M ](x[c -1 , compare ], y[c , cmp-compare-bits](z[Z, * -1 ])).-If the bits agree: clear the * and * marks and test if their position was maximal. Notice that bit equality is tested by using the same variable twice:• left = r[M ](x[c -1 , true], y[c , cmp-compare-bits](z[X, * -1 ]), -u[X, * -1 ]), • right = r[M ](x[c -1 , test-max], y[c , cmp-next-bits](z[X]), -u[X]). Return true if done:• left = r[M ](x[c -1 , true], y[c , cmp-next-bits]), • right = r[M ](x[c -1 ,ready], y[c , true]). Proceed to the loop if not, incrementing the value of the level -1 counter: • left = r[M ](x[c -1 , false], y[c , cmp-next-bits]), • right = r[M ](x[c -1 , increment], y[c , cmp-guess-1st-bit]).

Fig. 8 .

 8 Fig.8. The tree encoding the configuration (q 1 , q 2 , a• • • c, b • • • a) of an LCS.

1 [

 1 LCS](-w 2 [q 1 ], -w 3 [C1](-w 4 [end])), • right = w 1 [LCS](-w 2 [q 1 ], -w 3 [C1](-w 4 [a](w 5 [end])))).

2. It simulates repeatedly transitions of M , stopping if the final state is reached.

Fig. 7. The tree coding the tape b b q b a of the Turing machine M .

We only show how to encode transitions. The generation of the initial configuration, starting from the tree [M ]([c 0 , end], . . . ,

), is done using similar routines. We use a finite set of rules without query/guard part. Although the TPRS will be nondeterministic, appropriate tags shall ensure that rules applicable at some step have all the same left member. When the TPRS discovers that a nondeterministic guess was wrong, it blocks. Therefore, if M halts on x, then the TPRS always terminate. If M does not halt on x, then the corresponding run of the TPRS where all guesses are correct does not either. This ensures termination iff M halts on x.

To simulate a transition, the TPRS first performs the changes in the configuration, nondeterministically guessing the new head position. To check whether the head has been properly placed, it * -marks the original head position. The node c K marked by { run, check-suc1,check-suc2 . . . , check-pred1,check-pred2 . . . } (for instance, check-suc needs several steps) encodes the current stage of the simulation. For instance, to simulate a transition p a/b/→ ----→ q, we use the rule:

slightly abusing notation: we use a double tag involving a variable, to abbreviate a finite set of rules (with the obvious interpretation).

To complete the simulation of the transition, the TPRS checks whether the position written below the node pinpointed by q is a successor of that below the node pinpointed by * . If yes, it deletes the mark * , and labels c K back to [c K , run]. If not, the head position was incorrectly guessed and the system blocks.

The steps of check-suc, which checks that the nodes marked by * and q occur successively, are first a copy under c K of the level K counter located below the * -node, then an increment of that copy, and a comparison of the result to the counter below the q-node. We use auxiliary markers * , * for each level , attached to nodes below an counter: * in the part of the tree representing the configuration, and * under some c i , i > . We define inductively rules to achieve the following tasks for each level ≤ K:

-copy( ) copies below the * -marked node the level counters found below c .