Blaise Genest

Anca Muscholl

Zhilin Wu

Verifying Recursive Active Documents with Positive Data Tree Rewriting

Keywords: Active documents, Guarded Active XML, automated verification, data tree rewriting, tree decompositions

This paper proposes a data tree-rewriting framework for modeling evolving documents. The framework is close to Guarded Active XML, a platform used for handling XML repositories evolving through web services. We focus on automatic verification of properties of evolving documents that can contain data from an infinite domain. We establish the boundaries of decidability, and show that verification of a positive fragment that can handle recursive service calls is decidable. We also consider bounded model-checking in our data tree-rewriting framework and show that it is NexpTimecomplete.

INTRODUCTION

From static in house solutions, databases have become more and more open to the world, offering e.g. half-open access through web services. As usual for open systems, their design requires a careful static analysis process, helping to guarantee that no malicious client may take advantage of the system in a way for which the system was not designed. Static analysis of such systems very recently brought together two areas -databases, with emphasis on semi-structured XML data, and automated verification, with emphasis on model-checking infinite-state systems. Systems modeling dynamical evolution of data are pretty challenging for automated verification, as they involve feedback loops between semi-structured data, possibly with values from unbounded domains, and the workflow of services. If each of these topics has been studied extensively on its own, very few papers tackle decidability of algorithms when all aspects are present at the same time.

An interesting platform emerged recently for using XML repositories evolving through web services, namely Active XML (AXML) [START_REF] Abiteboul | The Active XML project: an overview[END_REF]. These are XML-based documents that evolve dynamically, containing implicit data in form of embedded service calls. Services may be recursive, so the evolution of such documents is both non-deterministic and unbounded in time. A first paper analyzing the evolution of AXML documents considered monotonous documents [START_REF] Abiteboul | Positive Active XML[END_REF]. With this restriction, as soon as a service is enabled in an AXML tree T , then from this point on the service cannot be disabled, and calling it can only extend T . In particular, information cannot be deleted and subsequent service calls return answers that extend previous answers. Recently, a workflow-oriented version of AXML was proposed in [START_REF] Abiteboul | Static analysis of active XML systems[END_REF]: the Guarded AXML model (GAXML for short) adds guards to service calls, thus controlling the possible evolution of active documents. Decidability in co-2NexpTime of static analysis for recursion-free GAXML w.r.t Tree-LTL properties was established in [START_REF] Abiteboul | Static analysis of active XML systems[END_REF]. The crucial restriction needed for decidability there is a uniform bound on the number of possible service calls. Compared to [START_REF] Abiteboul | Positive Active XML[END_REF], service invocation can terminate, and more importantly, negative guards can be used. Even more importantly, verification tasks are more complex and challenging because of the presence of unbounded data. However, the model relies on a rigid semantics of what a service call can do, and how (using a workspace etc). For instance, deletion of data is not possible.

In this work, our aim is twofold. First, we aim at extending the GAXML model in a uniform way, by expressing the effect of embedded service calls in form of tree rewriting rules. Our model DTPRS (data tree pattern rewriting systems) is based on the same basic ingredients as GAXML, which are tree patterns for guards and queries. However, our formalism allows a user to describe several possible effects of a service call: materialization of implicit data like in (G)AXML, but also deletion and modification of existing document parts. This model is a simplified version of the TPRS model proposed in [START_REF] Genest | Tree pattern rewriting systems[END_REF], but it can additionally handle data from infinite domains.

Our second, and main objective is to get decidability of static analysis of DTPRS without relying on a bound on the number of service calls. For doing that, we use a technique that emerged in the verification of particular infinite-state systems, such as Petri nets and lossy channel systems. The main concept is known in verification as well-structured transition systems (WSTS for short) [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF]. WSTS are one example of infinite-state systems where (potentially) infinite sets of states can be represented (and effectively manipulated) symbolically in a finite way. In contrast, [START_REF] Abiteboul | Static analysis of active XML systems[END_REF] uses a small model property which implies an enumeration of trees up to some bound.

Our basic objects are data trees, i.e., trees with labels from an infinite domain. We view data trees as graphs, and define in a natural way a well-quasi-order on such graphs. Then we show that a uniform bound on the length of simple paths in such graphs, together with positive guards, makes DTPRS 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]. As a technical tool we use here tree decompositions of graphs. In a nutshell we trade here recursion against positiveness, since considering both leads to undecidable static analysis. We show that for positive DTPRS, termination and tree pattern reachability are both decidable. Furthermore, we show that bounded modelchecking of (not necessarily positive) DTPRS is NexpTimecomplete. On the other hand, we show that the verification of simple but non positive temporal properties is undecidable even for positive DTPRS.

Related work: Verification of web services often ignores unbounded data (c.f. e.g. [START_REF] Hull | E-services: a look behind the curtain[END_REF][START_REF] Fu | Conversation protocols: a formalism for specification and verification of reactive electronic services[END_REF]). On the other hand, several data-driven workflow process models have been proposed. Document-driven workflow was proposed in [START_REF] Wang | A framework for document-driven workflow systems[END_REF]. Artifact-based workflow was outlined in [START_REF] Hull | Artifact-centric business process models: Brief survey of research results and challenges[END_REF], in which artifacts are used to represent key business entities, including both their data and life cycles. An early line of results involving data establishes decidability boundaries for the verification of temporal (first-order based) properties of a datadriven workflow processes, based on a relational data model [START_REF] Deutsch | Verification of communicating data-driven web services[END_REF][START_REF] Deutsch | Specification and verification of data-driven web applications[END_REF][START_REF] Deutsch | WAVE: Automatic verification of data-driven web services[END_REF]. This approach has been recently extended to the artifact-based model [START_REF] Deutsch | Automatic verification of data-centric business processes[END_REF].

On the verification side, there is a rich literature on the verification of well-structured infinite transition systems [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF], ranging from faulty communication systems [START_REF] Bouyer | On termination for faulty channel machines[END_REF] to programs manipulating dynamic data [START_REF] Abdulla | Monotonic abstraction for programs with dynamic memory heaps[END_REF] (citing only a few recent contributions). The latter work is one of the few examples where well-quasi-order on graphs are used.

Organization of the paper: In the next section, we fix some definitions and notations, define the DTPRS model, and illustrate how to reduce GAXML to our DTPRS model. Then in Section 3, we describe an example to illustrate the expressivity of DTPRS. In Section 4, we show that DTPRS with recursive DTD or negated tree patterns are undecidable. In Section 5 we define positive DTPRS and prove our decidability results. On the other hand, we show the undecidability of the verification of general, non-positive temporal properties in Section 6. Finally in Section 7, we consider bounded model-checking of (not necessarily positive) DT-PRS and show that the bounded model-checking problem is NexpTime-complete. Omitted proofs can be found in the appendix.

DEFINITIONS AND NOTATIONS

In this paper, documents correspond to labeled, unranked and unordered trees. Fix a finite alphabet Σ (with symbols a, b, c, . . ., called tags) and an infinite data domain D. A data tree is a (rooted) tree T with nodes labeled by Σ∪D. A data tree T can be represented as a tuple T = (V, E, root, ℓ), with labeling function ℓ : V → Σ ∪ D. Inner nodes are Σ-labeled, whereas leaves are (Σ ∪ D)-labeled. We fix a finite set of variables X (with symbols X, Y, Z, . . .) that will take values in D, and use * as special symbol standing for any tag. Let T denote Σ ∪ X ∪ { * }.

A data constraint is a Boolean combination of relations X = Y , with 1 X, Y ∈ X .

1 For simplicity we disallow here explicit data constants X = A data tree pattern (DTP) P = (V, E, root, ℓ, τ, cond ) is a (rooted) T -labeled tree, together with an edge-labeling function τ : E → {|, ||} and a data constraint cond . As usual, |-labeled edges denote child edges, and ||-labeled edges denote descendant edges. Internal nodes are labeled by Σ∪{ * }, and leaves by T . A matching of a DTP P into a data tree T is defined as a mapping preserving the root, the Σ-and D-labels (with * as wildcard), the child-and the descendant relations, satisfying cond and mapping X -labeled nodes to D-labeled ones. In particular, a relation X = Y (X, Y ∈ X ) means that the corresponding leaves are mapped to leaves of T carrying the same data value. If the mapping above is injective, then it is called an injective matching of P into T .

A relative DTP is a DTP with one designated node self . A relative DTP (P, self ) is matched to a pair (T, v), where T is a tree and v is a node of T .

We consider Boolean combinations of (relative) DTPs. The patterns therein are matched independently of each other (except that nodes designated by self must be matched to the same node of T ), and the Boolean operators are interpreted with the standard meaning.

A data tree pattern query (DTPQ) is of the form body head , with body a DTP and head a tree such that • the internal nodes of head are labeled by Σ and its leaves are labeled by (Σ ∪ D ∪ X ),

• every variable occurring in head also occurs in body ,

• there is at least one variable occurring in head , i.e., at least one leaf of head is labeled by X .

Let T be a data tree and Q = body head be a DTPQ. The evaluation result of Q over T is the forest Q(T ) of all instantiations of head by matchings µ from body to T . A relative DTPQ is like a DTPQ, except that its body is a relative pattern.

A locator is a relative DTP L with additional labels from the set {append , del} ∪ {rena | a ∈ Σ}. The labels append and rena are not exclusive and can be attached only to nodes of L that are labeled by a tag (that is by Σ ∪ { * } but not by D ∪ X ). Nodes not labeled by append , rena can be labeled by del (even data nodes), such that the descendants of a node labeled by del are labeled by del , too. The intuition behind this definition is to provide a context for data tree rewriting rules, together with some possible actions on this context: renaming, deletion, appending.

A data tree pattern rewriting rule (DTP rule) R is a tuple (L, G, Q, F, χ) with:

• L is a locator , • G is a Boolean combination of (relative) DTPs (the guard of R),
• Q is a finite set of relative DTPQs,

• F is a finite set of forests with internal nodes labeled by Σ and leaves labeled by Σ ∪ D ∪ X ∪ Q,

• χ is a mapping from the set of nodes of L labeled by append to F.

A DTP rewriting system (DTPRS) is a pair (R, ∆) consisting of a set R of DTP rules and a static invariant ∆, d (d ∈ D): they can be simulated by tags from Σ. consisting of a DTD and a data invariant, i.e. a Boolean combination of DTPs. We assume that the static invariant ∆ is preserved by the rewriting rules R. As usual for unordered trees, a DTD is defined as a tuple (Σr, P) such that Σr is the set of allowed root labels, and P is a finite set of rules a → ψ such that a ∈ Σ and ψ is a Boolean combination of inequalities of the form |b| ≥ k, where b ∈ Σ ∪ {dom} (dom is a symbol standing for any data value), and k is a non-negative integer. A positive DTD is one where the Boolean combinations above are positive.

We now define formally the semantics of a transition by DTP rules. So let T = (V, E, root, ℓ) be a data tree (with T |=∆) and let R = (L, G, Q, F, χ) be a DTP rule.

• Let µ be an injective matching from L to T . Let ν be the assignment of data values to variables in L such that ν(X) = ℓ(µ(v)) for every v labeled by X ∈ X in L.

• For each variable X ∈ X we denote its evaluation as X(T ), with X(T ) = ν(X) if defined, and X(T ) a fresh data value otherwise. Here a fresh data value is a data value which does not appear anywhere else in T . Furthermore, it is required that all the new variables of R, i.e. variables occurring in F, but not in L, should take mutually distinct fresh values. For each forest F ∈ F, we denote its evaluation by F (T ), by replacing labels Q ∈ Q by Q(T ) and labels X ∈ X by X(T ).

Recall that all queries Q ∈ Q are evaluated relatively to µ(self ).

• A data tree T ′ can be obtained from T by deleting subtrees rooted at nodes µ(v) whenever v is labeled by del in L, -changing the tag of a node µ(v) to a whenever v is labeled by rena in L, -appending F (T ) as a subforest of nodes µ(v) whenever v is labeled by append in L and χ(v) = F , -every other node of T keeps its tag or data.

• The rule R is enabled on data tree T if there exists an injective matching µ of L into T such that (1) G is true on (T, µ(v)) with v labeled by self in L, and (2) there is a data tree T ′ , obtained from T and µ by the operations specified above, satisfying T ′ |=∆.

Let T R -→ T ′ denote the transition from T to T ′ using DTP rule R ∈ R. Remark 1.
1. The injectivity of the matching µ ensures that the outcome T ′ is well-defined. In particular, no two nodes with label del and append (or rena), resp., can be mapped to the same node in the data tree. However, mappings used for guards or queries are -as usual -non injective.

For the new variables occurring in F, but not in L,

we choose mutually distinct fresh values. We could have chosen arbitrary values instead, and enforce the fact that they are fresh and mutually distinct a posteriori using the invariant ∆. In this case, the invariant needs negation. The invariant (or the locator) can be also used to enforce that the (arbitrarily) chosen values already occur in T . This kind of invariant would be positive.

3. In our definition of DTP rules, it might appear that guards are redundant wrt. the locator. But notice that this only concerns positive guards.

Given a DTPRS (R, ∆), let T -→ T ′ denote the union of T R -→ T ′ for R ∈ R, and T + -→ T ′ (or T * -→ T ′ ) denote the transitive (or reflexive and transitive) closure of T -→ T ′ . Moreover, let T * R (T ) denote the set of trees that can be reached from a data tree T by rewriting with DTP rules from R, i.e.

T * R (T ) = {T ′ | T * -→ T ′ }.
For a set of data trees I, let T * R (I) be the union of T * R (T ), for T ∈ I. We are interested in the following questions, given a DT-PRS (R, ∆):

• Pattern reachability: Given a DTP P and a set of initial trees2 Init, given as the conjunction of a DTD and a Boolean combination of DTPs, is there some T ∈ T * R (Init) such that P matches T ?

• Termination: Given an initial data tree T0, are all rewriting paths T0 → T1 → • • • starting from T0 finite?

The reason for the fact that termination of DTPRS is defined above w.r.t a single initial data tree is that termination from a set of initial trees is already undecidable without data (see Section 4).

Reduction from GAXML to DTPRS

DTPRS is a quite powerful model, which allows to model e.g. Guarded Active XML (GAXML) [START_REF] Abiteboul | Static analysis of active XML systems[END_REF]. We show this translation on two main GAXML steps: call and return of services. For completeness, we briefly recall the main features of GAXML here. AXML trees contain embedded function calls that are evaluated (via tree pattern queries) in a workspace. GAXML adds call and return guards, that control the function call and the return of the result (as sibling of the call node). Functions can be internal or external. The external ones return some arbitrary forest that is consistent with the static invariant ∆.

We describe here how to model an (internal) function call in GAXML with DTPRS. Let f ∈ Σ be a function associated with the argument query Q and the call guard G. The associated DTP rule has the same guard G, the set of queries Q = {Q}, and F = {T f , TX } is the set defined below:

• T f is a tree with three nodes, the root being labeled by f , and the two leaves labeled by the query Q and by the variable X, respectively.

• TX is a tree with a unique node labeled by the variable X,

The locator L is given in Figure 1. Finally, χ maps the !f -node to TX and the WS-node to T f . Applying the DTP rule amounts in evaluating Q to get the arguments of the call, writing them into the workspace WS, and creating a fresh identifier X that it copied both below WS and below the node with the function call (aka return address for f , see below).

We describe now how to model the return of an (internal continuous) function f ∈ Σ associated with the return query Q and the return guard G. The associated DTP rule has the same guard G, the set of queries

Q = {Q}, F = {TQ} has root !f WS self ren?f ,append (TX) append (Tf )
Figure 1: The locator for service invocation.

a unique tree with a unique node labeled by the query Q, and the locator is given in Figure 2 with the data constraint Finally, χ maps the node labeled append with TQ. This DTP rule locate where the call was computed in the workspace WS using X, evaluates Q to get the return of the call, puts the result of the return query as a sibling of ?f , and deletes the associated data in the workspace, as well as the identifier X.

X = Y : root * ?f WS f Y X self append (TQ) ren!f del del del

MAILORDER EXAMPLE

The following is a DTPRS description of the basic functionalities of a MailOrder system for Play.com. For simplicity, we represent only what happens on the Play.com peer, although we could also model client peers, bank peers etc. The Play.com example can be compared with the MailOrder example in [START_REF] Abiteboul | Static analysis of active XML systems[END_REF]. Syntactically, GAXML uses guards and queries. Most of the time, guards and queries are very simple and can be encoded in the locator of DTP rules. In this case, we omit the self label in our rules. Unlike MailOrder we can express deletion with DTPRS, and thus model the selection of the products in the cart (adding and deleting products), and also handle an inventory (how many items of a product remain -each time an item is added to a cart, it is also deleted from the inventory). More importantly, compared with the recursion-free decidable restriction of GAXML, we are able to represent the process of many customers ordering many different products in our decidable fragment.

On the Play.com peer, there are a product catalog, a customer catalog, a set of carts and a set of orders. The inventory is encoded in the product catalog: if there are three items of a product in the inventory, then there are three tokens as children of the product. Each cart is associated with a customer (at first anonymous, and he can later login in as a registered member). The cart is first in the select mode, which allows the associated customer to add/delete products. Then the customer can check out, the cart gathers the different prices for the products into a bill, and goes into payment mode. When the customer pays, a corresponding order is created with a receipt, the customer is disconnected and the cart is deleted.

A simple example of a configuration of Play.com is illus-trated in Figure 3. We represented a data value only when it is used by at least two different nodes. Some key rewriting rules are described in the following. We only describe nontrivial components in these rules. Tree patterns are represented below in term form, with descendant edges preceded by asymbol.

• An anonymous customer can connect to Play.com with the rule create-cart.

-

L := [Play.com append(F ) ] -F := [Cart]([nolog]([CId](X)), [products], [select]).
Notice that here X is a fresh data value.

• An anonymous customer can login as a registered member with the rule login. As the customer peer is not modeled, we do not handle the check of a password, although it would not be a problem to do so in our framework.

-

L := [Play.com](-[Customer]([CId](X)), [Cart append(F ) ]([nolog del ])) -F := [log]([CId](X)).
Here, X is the same PId for the cart and for the customer.

• The rule Add-Product adds a new product into the cart (and deletes a token from the inventory).

-

L := [Play.com]([Cart]([products append(F ) ]), -[Product]([PId](X), [tokendel ])) -F := [PId](X).
• The rule Delete-Product deletes a product from the cart (and puts the token back).

-

L := [Play.com]([Cart]([select], -[PIddel ](X)), -[Product append(F ) ]([PId](X))) -F := [token].
• The rule Check-out checks whether the cart is nonempty and retrieves the prices of products in the cart into a bill through a query. It changes the mode of the cart from select to payment.

-

L := [Play.com]([Cart self ,append(F ) ](-[PId], [selectren payment ])) -F := [Bill](Q), and Q := body Y is the query with body = [Play.com]([Cartself ](-[PId](X)), -[Product]([PId](X), [Price](Y ))).
• The customer can pay with the rule Pay, and a corresponding order is created. For simplicity, it disconnects the customer, and transforms the cart into an order. The order contains the customer ID, an order ID (a fresh unique identifier), and the total price (sum of the prices of each items). As we model prices by data values and we do not use any arithmetics, the total price is a fresh data value. The only important thing is that this data value Total is the same as the one registered in the bank account, which we could check for equality (although we do not explicitly model the bank here). The order does not recall the individual PID of products since there will be no more products to put back in the inventory (and anyway the product can be later removed from the catalog).

-

L := [Play.com]([Cartappend F ,ren Order ]([Billdel ], [products del ], [payment ren paid ], [log rencust ])) -F := [Receipt]([OId](X), [Total](Y ))
• The rule Add-member allows a customer to register as a member.

-

L := [Play.com]([CCatalog append(F ) ]) -F := [Customer]([CId](X), [Name](Y ), [Email](Z))
We do not specify the following rules here, which are easy to come up with: shipped, delivered, add product to catalog etc.

Notice that this example is intentionally not correct. Indeed, as there is no check of the state in which the cart is at rule Add-Product, it is possible that a bill is produced after a check out, and the customer can still add products with the aforementioned rule which will never be accounted for in the bill. We will show later that we can decide whether such a problem occurs or not. To fix this problem, it suffices to check in the locator L of Add-Product rule that the cart is in the select mode.

UNDECIDABILITY

As one might expect, analysis of DTPRS is quickly undecidable -and sometimes already without using any unbounded data. The proof of the proposition below is obtained by straightforward simulations of 2-counter machines.

Proposition 2. Both termination and pattern reachability for DTPRS (R, ∆) are undecidable whenever one of the following holds:

1. the DTD in ∆ is recursive, 2. either guards in R or the invariant ∆ contain negated DTPs.
The above result holds even without data.

The next result shows that with data, we can relax both conditions above and still get undecidability of DTPRS. The main idea is to use data for creating long horizontal paths (although trees are supposed to be unordered). Such horizontal paths can be obtained e.g. with a tree of depth 2, having subtrees of height one with 2 leaves each, say labeled by data values di, di+1. Assuming all di are distinct (and distinguishing d1) we get a linear order on these subtrees. Theorem 3. Both termination and pattern reachability are undecidable for DTPRS (R, ∆) such that [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF] the DTD in ∆ is non-recursive and [START_REF] Abdulla | Monotonic abstraction for programs with dynamic memory heaps[END_REF] all DTPs in guards from R and the invariant ∆ are positive.

Proof. We reduce Post correspondence problem (PCP) first to pattern reachability. We may assume that our PCP instance (ui, vi) 1≤i≤n is such that the following holds for every non-empty sequence i1, . . . , i k of indices:

• Either U = ui 1 • • • ui k , V = vi 1 • • • vi k are incompara-
ble, or V is a prefix of U . In the latter case we call (U, V ) a partial solution.

• If (U, V ) and (U ui, V vi) are partial solutions and U = V , then either U ui = V vi or V vi is a prefix of U .

• Every solution starts with with the pair (u1, v1) and ends with (un, vn).

It is not hard to verify that the usual Turing machine reduction to PCP satisfies the restrictions above.

A partial solution (U, V ) with U = a1 • • • an, V = a1 • • • am-1 will be represented by the data tree below. In this data tree the leaves are labeled by data di, with di = dj for all i = j. Moreover, notice that the last position has the special marker $, and the first position in U without V has the special marker #. root With each PCP pair (ui, vi), i < n, we associate DTPRS rules Ri = (L, G, Q, F, χ). For simplicity we describe below the locator L and the forest F for (ui, vi) = (aba, bb) (the guard G and the query set Q are both empty):

root append (F (aba)) b, # ren b X1 X2 b X2 X3 c ren c,# X3 X4 d, $ ren d X5 X6
We need a rule Ri for each pair of tags c, d ∈ Σ (these are the tags at positions n and m + 2 in the example with |vi| = 2). The forest F (aba) which will be added under the root node will contain 3 trees T1, T2, T3, with roots labeled a, b and a, $, respectively. Tree T1 has two leaves, labeled X6 and X7. Tree T2 (T3, resp.) has two leaves, labeled X7 and X8 (X8 and X9, resp.). Notice that variable X6 occurs in both L and F (aba), whereas X7, X8, X9 will take fresh (and mutually distinct) values.

The pair (un, vn) has similar rules, except that we will not append any forest to the root, but rename the root with a special marker √ . The initial tree T0 is defined as expected, from (u1, v1). The PCP instance has a solution iff we can reach a data tree with root label √ . Notice that all guards and the invariant are empty.

For termination we can modify the above proof in order to ensure that executions that do not correspond to partial solutions, are infinite. More precisely, if U, V as above is a partial solution, but U ui, V vi is not, then we use a DTP rule associated with (ui, vi) that forces an infinite execution. In this way, termination will hold iff the PCP instance has a solution.

We end this section with a remark on the decidability of termination from an initial set of trees. First we notice that -already without data -DTPRS can simulate so-called reset Petri nets [START_REF] Genest | Tree pattern rewriting systems[END_REF]. These are Petri nets (or equivalently, multi-counter automata without zero test) with additional transitions that can reset places (equivalently, counters) to zero. They can be represented by trees of depth 2, where nodes at depth one represent places, and their respective number of children (leaves) is the number of tokens on that place. A DTPRS (without data) can easily simulate increments, decrements and resets (using deletion in DTPRS). It is known that so-called structural termination for reset Petri nets is undecidable [START_REF] Mayr | Undecidable problems in unreliable computations[END_REF], i.e., the question whether there are infinite computations from any initial configuration, is undecidable. This implies: Proposition 4. The following question is undecidable: Given a DTPRS (R, ∆), is there some tree T0 satisfying ∆ and an infinite computation

T0 -→ T1 -→ • • • in (R, ∆)?
This holds already for non-recursive DTD in ∆ and without data constraints in DTPs.

POSITIVE DTPRS

In this section we consider positive DTPRS, a fragment of DTPRS for which we show that termination and pattern reachability are decidable.

From Proposition 2, we know that in order to get decidability, the DTD in the static invariant ∆ must be nonrecursive. For a non-recursive DTD, there is some B such that every tree satisfying the DTD has depth bounded by B.

In the following, we assume the existence of such a bound B. Also from Proposition 2, we know that for decidability we need to consider only positive guards and positive data invariants.

However, from Theorem 3, we know that these restrictions alone do not suffice to achieve decidability. We need to disallow long linear orders created with the help of data. For this, we introduce a last restriction, called simple-path bounded, which is defined in the following.

Let T = (V, E, root, ℓ) be a data tree. The graph G(T ) associated with T is the undirected graph obtained by adding to V the set of data values occurring in T , and adding to E the links between a leaf labeled by a data value and the node representing that value (see also Figure 3). Formally,

G(T ) = (V ′ , E ′ ), where V ′ = V ∪ {ℓ(v) | ℓ(v) ∈ D} and E ′ = E ∪ {{v, d} | ℓ(v) = d ∈ D}.
A simple path of T is a simple path in G(T ), i.e. a sequence of vertices v1, . . . , vn in G(T ) such that for all i = j, {vi, vi+1} ∈ E ′ and vi = vj . The length of a path v1, . . . , vn is n -1.

Formally, a DTPRS (R, ∆) is a positive DTPRS with set of initial trees Init, if:

• non-recursive-DTD: the DTD in the static invariant ∆ is non-recursive. In particular, trees satisfying the DTD have depth bounded by some B > 0.

• positive: all guards in R and the data invariant in ∆ are positive Boolean combinations of DTPs. The DTD in ∆ is positive as well.

• simple-path bounded: there exists K > 0 such that the length of any simple path in any T ∈ T * R (T0) for any T0 ∈ Init, is bounded by K.

Notice that the third condition above implies that all data trees have depth bounded by K. So we always assume that B ≤ K. Notice also that in positive DTPRS, the data value inequality is allowed in DTPs, that is, we can state that two data values are different. The Play.com example in Section 3 satisfies the first 2 conditions above. However, in general, the third condition is not satisfied. PIds can create create a long path: a cart can be linked to a product, linked to another cart linked to another products etc. So the number of carts or the number of products needs to be bounded (unless a cart can contain at most one product). On the other hand, Name and Total are fresh data values, they cannot be used as links. At last, CId can be used in different carts and orders, but as a cart or order is associated to a unique customer, it cannot create long links. More formally, if the system can handle only C active carts at a time (but the number of orders is unlimited), then the system has simple paths bounded by 12C + 7. If there are at most D different products in the catalog, then the system has simple paths bounded by 12D + 7. Finally, if each customer can have only one active cart at a time (but she can have many orders), and each cart has at most one product, then the system has simple paths bounded by 14. Any of these restrictions can be described using only positive rules. The rest of the section is devoted to the proof of the following result: Theorem 5. Given a positive DTPRS (R, ∆), the pattern reachability and the termination problem are decidable.

We prove Theorem 5 by using the framework of wellstructured transition systems (WSTS) [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF], which has been applied to DTPRS without data in [START_REF] Genest | Tree pattern rewriting systems[END_REF]. We recall briefly some definitions. A WSTS is a triple (S, -→, ) such that S is an (infinite) state space, is a well-quasi-ordering 3(wqo for short) on S, and -→ is the transition relation on S. It is required that -→ is compatible w.r.t. : for any s, t, s ′ ∈ S with s -→ t and s s ′ , there exists t ′ ∈ S such that s ′ -→ t ′ and t t ′ .

Let TB,K denote the set of data trees whose depths are bounded by B and lengths of simple paths are bounded by K. From the definition of positive DTPRS, we know that T * R (Init) ⊆ TB,K . In the following, we show Theorem 5 by showing that (TB,K , -→, ) is a WSTS.

We define the binary relation on TB,K . Let T1 = (V1, E1, root1, ℓ1), T2 = (V2, E2, root2, ℓ2) ∈ TB,K , then T1 T2 if there is an injective mapping φ from V1 to V2 such that

• root preservation: φ(root1) = root2, • parent-child relation preservation: (v1, v2) ∈ E1 iff (φ(v1), φ(v2)) ∈ E2, • tag preservation: If ℓ1(v) ∈ Σ, then ℓ1(v) = ℓ2(φ(v)),
• data value (in)equality preservation: If v1, v2 ∈ V1 and ℓ1(v1), ℓ1(v2) ∈ D, then ℓ2(φ(v1)), ℓ2(φ(v2)) ∈ D, and ℓ1(v1) = ℓ1(v2) iff ℓ2(φ(v1)) = ℓ2(φ(v2)).

It is easy to see that is reflexive and transitive, so it is a quasi-order. In the following, we first assume that is a wqo on TB,K and show that -→ is compatible with , in order to prove Theorem 5. We show in Section 5.3 that is indeed a wqo: for any infinite sequence of data trees T0, T1, . . . ∈ TB,K , there are i < j such that Ti Tj.

Well-structure of positive DTPRS

Let (R, ∆) be a positive DTPRS. andT1 T ′ 1 . Then there exists

Proposition 6. Let T1, T ′ 1 , T2 ∈ TB,K , T1 R -→ T2 for some R ∈ R,
T ′ 2 ∈ TB,K such that T ′ 1 R -→ T ′ 2 and T2 T ′ 2 . Proof. Let R = (L, G, Q, F, χ).
Taking an injective mapping φ : T1 → T ′ 1 preserving the root, parent-child relation, tag, and data (in)equality relation, and an injective matching ψ : L → T1 satisfying the data constraint cond of L, we have an injective matching φ • ψ : L → T ′ 1 which respects the parent-child, tags and data (in)equality relation. Hence cond is satisfied by φ

• ψ too. As G is positive, if G is true at T1 wrt. φ, then it is true at T ′ 1 wrt. φ • ψ as well. Applying the rule R to T ′ 1 wrt. φ • ψ, we get a tree T ′ 2 such that T2 T ′ 2 .
As both the DTD and the data invariant in ∆ are positive and T2 fulfills ∆, so does

T ′ 2 . Thus T ′ 1 R -→ T ′ 2 .
Consequently, we have shown that -→ is compatible wrt. in TB,K , thus (TB,K , -→, ) is a WSTS.

In the following, we prove that (TB,K , -→, ) satisfies some additional computability conditions, needed to show the decidability of pattern reachability and termination.

First consider pattern reachability. To get the decidability of this problem, from Theorem 3.6 in [START_REF] Finkel | Well-structured transition systems everywhere![END_REF], we need to show that (TB,K , -→, ) has effective pred-basis. A WSTS (S, -→, ) has effective pred-basis if there exists an algorithm that computes for any state s ∈ S the finite basis pb(s) of the upward closed set ↑ Pred (↑ s). A solution for reachability of a given DTP P from an initial set of data trees Init is obtained by backward exploration: we start with I 0 as the set of data trees matching P and satisfying ∆. Then compute iteratively the upward closed sets I n+1 = I n ∪ (Pred (I n ) ∩ ∆) by representing each set through its finite basis. Since the sequence I n is increasing by construction, and since is a wqo, the sequence must be finite and termination can be effectively tested. If I n = I n+1 then it suffices to check whether I n ∩ Init = ∅. Notice that we did not impose any restriction on the set Init of the initial trees. We need to test the existence of a data tree from TB,K satisfying an (arbitrary) Boolean combination on DTPs and an (arbitrary) DTD. This problem is in general undecidable [START_REF] David | Complexity of data tree patterns over XML documents[END_REF], but becomes decidable in the special case where trees are of bounded depth [START_REF] David | Complexity of data tree patterns over XML documents[END_REF]. Here we need to talk in addition about trees from TB,K , but we can apply the same proof ideas as in [START_REF] David | Complexity of data tree patterns over XML documents[END_REF] in order to infer decidability. Now consider the termination problem. From Theorem 4.6 in [START_REF] Finkel | Well-structured transition systems everywhere![END_REF], to show the decidability of termination problem from a single initial tree T0, it is sufficient to show that (T * R (T0), R -→, ) has effective Succ, i.e. for each T ∈ T * R (T0), the set Succ(T ) := {T ′ | T -→ T ′ } is computable. Then we can compute the finite reachability tree starting with T0: we compute trees T s.t. T0 * -→ T and we stop whenever we find T T ′ along some branch. It is not hard to see that Succ(T ) contains only a finite number of equivalence classes induced by the quasi-order . Since the DTPRS (R, ∆) is not able to distinguish between two distinct data trees belonging to the same equivalence class, by selecting one data tree from each equivalence class, we can get a finite representation of Succ(T ), therefore, (T * R (T0), -→, ) has effective Succ.

Tree Decompositions

In order to prove that is a wqo over TB,K , we first represent a data tree T as a (labeled) undirected graph G ℓ (T ), then we encode G ℓ (T ) into a tree (without data) of bounded depth using the concept of tree decompositions. Define a binary relation ≤ on (labeled) trees of bounded depth as follows: T1 ≤ T2 if there is an injective mapping from T1 to T2 preserving the root, the tags, and the parent-child relation. It is known that ≤ is a wqo on labeled trees of bounded depth without data [START_REF] Genest | Tree pattern rewriting systems[END_REF].

Let GK be the set of labeled graphs with the lengths of all simple paths bounded by K. We show that on TB,K corresponds to the induced subgraph relation (formally defined later) on GK, and the fact that ≤ is a wqo for labeled trees of bounded depth implies that the induced subgraph relation is a wqo on GK.

Given a data tree T = (V, E, root, ℓ) ∈ TB,K , the labeled undirected graph representation G ℓ (T ) of T is obtained from G(T ), the graph associated to T , by adding labels encoding information of data tree nodes (tag, depth . . .). Formally,

G ℓ (T ), is a ((Σ ∪ {#}) × [B + 1]) ∪ {$}-labeled (where [B + 1] = {0, 1, • • • , B}) undirected graph (V ′ , E ′ , ℓ ′ ) defined as follows, • V ′ = V ∪ {ℓ(v) | v ∈ V, ℓ(v) ∈ D}, • E ′ = E ∪ {{v, d} | v ∈ V, ℓ(v) = d ∈ D}, • If ℓ(v) ∈ Σ, then ℓ ′ (v) = (ℓ(v), i), otherwise, ℓ ′ (v) = (#, i), where i is the depth of v in T . In addition, ℓ ′ (d) = $ for each d ∈ V ′ ∩ D. Let ΣG denote ((Σ ∪ {#}) × [B + 1]) ∪ {$}.
For ΣG-labeled graphs, we define the induced subgraph relation as follows. Let G1 = (V1, E1, ℓ1), G2 = (V2, E2, ℓ2) be two ΣG-labeled graphs, then G1 is an induced subgraph of G2 (denoted G1 ⊑ G2) iff there is an injective mapping φ from V1 to V2 such that

• label preservation: ℓ1(v1) = ℓ2(φ(v1)) for any v1 ∈ V1, • edge preservation: let v1, v ′ 1 ∈ V1, then {v1, v ′ 1 } ∈ E1 iff {φ(v1), φ(v ′ 1 )} ∈ E2.
From the definition of the labeled graph representation of data trees, it is not hard to show that the induced subgraph relation ⊑ corresponds to the relation on data trees.

Proposition 8. Let T1, T2 ∈ TB,K , then T1 T2 iff G ℓ (T1) ⊑ G ℓ (T2).
Now we show how to encode any ΣG-labeled graph belonging to GK into a labeled tree of bounded depth by using tree decompositions.

Let G = (V, E, ℓ) be a connected ΣG-labeled graph, then a tree decomposition of G is a quadruple T = (U, F, r, θ) such that:

• (U, F, r) is a tree with the tree domain U , the parentchild relation F , and the root r ∈ U ,

• θ : U → 2 V is a labeling function attaching each node u ∈ U a set of vertices of G,

• For each edge {v, w} ∈ E, there is a node u ∈ U such that {v, w} ⊆ θ(u),

• For each vertex v ∈ V , the set of nodes u ∈ U such that v ∈ θ(u) constitutes a connected subgraph of T .

The sets θ(v) are called the bags of the tree decomposition.

The depth of a tree decomposition T = (U, F, r, θ) is the depth of the tree (U, F, r) and the width of T is defined as max{|θ(u)| -1 | u ∈ U }. The tree-width of a graph G = (V, E) is the minimum width of tree decompositions of G. For a tree decomposition of width K of a graph G, without loss of generality, we assume that each bag is given by a sequence of vertices of length K + 1, v0 . . . vK , with possible repetitions, i.e. possibly vi = vj for some i, j : i = j (tree decompositions in this form are sometimes called ordered tree decompositions).

Theorem 9 ( [START_REF] Nesetȓil | Tree-depth, subgraph coloring and homomorphism bounds[END_REF][START_REF] Blumensath | On the monadic second-order transduction hierarchy[END_REF]). If G ∈ GK , then G has a tree decomposition with both depth and width bounded by K.

Proof. Let G = (V, E, ℓ) ∈ GK and T = (V, ET , r) be a depth-first-search tree of G with r ∈ V as the root. Then T is of depth at most K. For each v ∈ V , let θ(v) be the union of {v} and the set of all ancestors of v in T , then (V, ET , r, θ) is a tree decomposition of G of depth at most K and width at most K.

As a matter of fact, the converse of Theorem 9 holds as well.

Proposition 10. If G has a tree decomposition of width ≤ A and depth ≤ B, then the length of any simple path of G is bounded by (A + 2) B + 1≤i≤B (A + 2) i . So generally speaking, for a class of graphs, all simple paths are length-bounded for each graph in the class iff there is a tree decomposition of bounded depth and width for each graph in the class. Now we describe how to encode labeled graphs by labeled trees using tree decompositions.

Let G = (V, E, ℓ) ∈ GK be a ΣG-labeled graph, and T = (U, F, r, θ) be a tree decomposition of G with width K and depth at most K. Remember that each θ(u) is represented as a sequence of exactly K + 1 vertices, and

[K + 1] = {0, . . . , K}. Define ΣG,K := (ΣG) K+1 × 2 [K+1] 2 × 2 [K+1] 2 × 2 [K+1] 2 .
We transform T = (U, F, r, θ) into a ΣG,K -labeled tree T ′ = (U, F, r, η), which encodes in a uniform way the information about G (including edge relations and vertex labels). η : U → ΣG,K is defined as follows. Let θ(u) = v0 . . . vK , then η(u) = (ℓ(v0) . . . ℓ(vK ), λ), where λ = (λ1, λ2, λ3),

• λ1 = {(i, j) | 0 ≤ i, j ≤ K, vi = vj }, • λ2 = {(i, j) | 0 ≤ i, j ≤ K, {vi, vj} ∈ E}, • If u = r, then λ3 = ∅, otherwise let u ′ be the parent of u in T and θ(u ′ ) = v ′ 0 • • • v ′ K , then λ3 = {(i, j) | 0 ≤ i, j ≤ K, v ′ i = vj}.

Well-quasi-ordering for data trees

The encoding of labeled graphs into labeled trees establishes a connection between the wqo ≤ of labeled trees and the induced subgraph relation (⊑) of labeled graphs.

Proposition 11. Let G1, G2 be two ΣG-labeled graphs with tree-width bounded by K, and T1, T2 be two tree decompositions of width K of resp. G1, G2, then the two ΣG,Klabeled trees T ′ 1 , T ′ 2 obtained from T1, T2 satisfy that:

If T ′ 1 ≤ T ′ 2 , then G1 ⊑ G2.
Proof. Let Gi = (Vi, Ei, ℓi), Ti = (Ui, Fi, ri, θi) and

T ′ i = (Ui, Fi, ri, ηi)(i = 1, 2). Suppose that T ′ 1 ≤ T ′ 2 .
Then there is an injective mapping φ from U1 to U2 preserving the root, the parent-child relation and the node-labels.

Define an injective mapping π : V1 → V2 as follows:

For v ∈ V1, select some u ∈ U1 such that θ1(u) = v0 . . . vK and v = vi for some i.

Writing θ2(φ(u)) = v ′ 0 . . . v ′ K , we let π(v) = v ′ i .
First we show that π does not depend upon the choice of i such that v = vi, neither on the choice of u ∈ U1 such that v ∈ θ1(u). The former holds because η1(u) = η2(φ(u)) (and in particular the component λ1 is preserved), hence if vi = vj , then we also have v ′ i = v ′ j . For the latter, notice that the λ3 component of η1(u) = η2(φ(u)) is preserved, hence the choice of u or of its father is irrelevant. Now, the set {u ∈ U1 | v ∈ θ1(u)} is a connected subgraph of T1 by definition of tree decomposition, hence π does not depend upon the choice of u ∈ U1. Now we show that π is injective. Let v2 be a vertex of G2. Because of the preservation of λ1, no two different vertices v, v ′ of G1 with v, v ′ ∈ θ(u) can satisfy π(v) = π(v ′ ) = v2. Because of the preservation of λ3, no two different vertices v, v ′ with v ∈ θ(u) and v ′ ∈ θ(u ′ ) with u father of u ′ can satisfy π(v) = π(v ′ ) = v2. Again, as the set {u ∈ U1 | v2 ∈ θ(u)} is a connected subgraph of T2, it means that π is injective.

We finish the proof by showing that π preserves the nodelabels and edge relations.

Node-label preservation: Suppose π(v) = v ′ . Then there exists some u ∈ U1 such that θ1(u

) = v0 • • • v k , v = vi for some i, θ2(φ(u)) = v ′ 0 • • • v ′ k , and v ′ = v ′ i . Since η1(u) = η2(φ(u)), ℓ1(v0) . . . ℓ1(v k ) = ℓ2(v ′ 0 ) . . . ℓ2(v ′ k ), it follows that ℓ1(v) = ℓ1(vi) = ℓ2(v ′ i ) = ℓ2(v ′ ). Edge relation preservation: We show that {v, w} ∈ E1 iff {π(v), π(w)} ∈ E2 for any v, w ∈ V1. If {v, w} ∈ E1, there exists u ∈ U1 such that θ1(u) = v0 • • • v k , v = vi and w = vj for some i, j. So (i, j) ∈ λ2(u) in T ′ 1 . Then (i, j) ∈ λ2(φ(u)). Let θ2(φ(u)) = v ′ 0 • • • v ′ k , then {v ′ i , v ′ j } ∈ E2. Consequently {π(v), π(w)} = {v ′ i , v ′ j } ∈ E2. If {π(v), π(w)} ∈ E2,
then there exists u ′ ∈ U2 such that π(v), π(w) ∈ θ2(u ′ ). Without loss of generality, we can choose u ′ at minimal depth such that π(v), π(w) ∈ θ2(u ′ ). It means that for instance, the father

u ′′ of u ′ satisfies π(v) / ∈ θ2(u ′′ ). Since U ′ 2 = {u ′′′ ∈ U2 | π(v) ∈ θ2(u ′′′ )} is connected,
it means that U ′ 2 is entirely contained in the subtree rooted at u ′ . By contradiction, if there does not exist u ∈ U1 such that φ(u) = u ′ , then φ(U1) ∩ U ′ 2 = ∅. On the other hand, according to the definition of π, there is u ∈ U1 such that v ∈ θ1(u) and π(v) ∈ θ2(φ(u)). So φ(u) ∈ φ(U1) ∩ U ′ 2 , a contradiction. Thus there is u ∈ U1 such that u ′ = φ(u). Let θ1(u) = v0 . . . v k and θ2(u ′ ) = v ′ 0 . . . v ′ k , by injectivity of π, we have π(v) = v ′ i , π(w) = v ′ j , v = vi, w = wj for some i, j. Then (i, j) ∈ λ2(u ′ ) = λ2(u), which proves that {v, w} is an edge of G1. Now we are ready to show that is a wqo for TB,K . Let T0, T1, . . . be an infinite sequence of data trees from TB,K . Consider the infinite sequence of ΣG,K -labeled trees T ′ 0 , T ′ 1 , . . . obtained from the tree decompositions (with width K and depth at most K) of graphs G ℓ (T0), G ℓ (T1), . . . . Then there are i, j : i < j such that T ′ i ≤ T ′ j , because ≤ is a wqo for labeled trees of depth at most K. So G(Ti) ⊑ G(Tj) from Proposition 11, and Ti Tj from Proposition 8. We thus prove following theorem.

Theorem 12.
is a well-quasi-ordering over TB,K .

VERIFICATION OF TEMPORAL PROP-ERTIES

Until now we considered only two properties for static analysis: termination and pattern reachability. (Non-)reachability of a DTP can be expressed easily in Tree-LTL [START_REF] Abiteboul | Static analysis of active XML systems[END_REF], which corresponds roughly to linear time temporal logics where atomic propositions are DTPs 4 . We show in this section that allowing for runs of unbounded length makes the validation of (even simple) Tree-LTL properties undecidable, even without data: Proposition 13. It is undecidable whether a TPRS with initial (data-free) tree T0 satisfies a given Tree-LTL formula.

The fact that Tree-LTL is undecidable does not disallow us to verify quite complicated properties. We show on the Play.com example how to proceed: it suffices to encode in the system the property we want to check with additional tags and check for pattern reachability. For example, suppose that we want to verify whether a customer can add some product after the bill was processed. For that, we add new tags #, 1, 2, 3 to the alphabet, and we add one child to Play.com labeled by 1 in the initial tree. We add one rule which checks that the additional tag is 1 and selects one cart in the payment mode. The outcome of the rule is to change the tag from 1 to 2, and to append # as child of the selected cart. We add another rule which checks that the tag is 2. The outcome of the rule is to change the tag from 2 to 3, and to append a new product with one item in the inventory below PCatalog with a special marker # as brother of PId. Now one can reach in the new system a tree with a cart marked # and with a product with PId X such that there exist a Product with PId X in the PCatalog which is marked by # iff a customer can add some product after the bill was generated in the original system. The former property is a pattern reachability problem, which we proved to be decidable. 4 Such formulas use actually free variables in patterns, which are then quantified universally. This is consistent with the approach of testing whether a model satisfies the negation of a formula.

BOUNDED MODEL-CHECKING DTPRS AND RECURSION-FREE GAXML

Recall that [START_REF] Abiteboul | Static analysis of active XML systems[END_REF] shows that the largest decidable fragment of GAXML that can be model-checked w.r.t. Tree-LTL properties is the recursion-free one. Absence of recursion in GAXML roughly means (1) disallowing recursive DTDs (as we do here) and (2) imposing that no function is called more than once, on any execution path. On the other hand, one can use negated DTPs in this fragment.

In this section we consider bounded model checking for DTPRS: Given a DTPRS (R, ∆), a set of initial trees Init, a DTP P and a bound N (encoded in unary) we ask whether there is some T0 satisfying Init and some T s.t. P matches T and T0 ≤N -→ T . We show the following result:

Theorem 14. Bounded model-checking for DTPRS is NexpTime-complete.

Theorem 14 can be actually extended to bounded modelchecking Tree-LTL properties. Bounded model-checking of a Tree-LTL formula ϕ with a bound N is the problem checking whether a counter-example for ϕ holds in ≤ N -steps. For instance, bounded model-checking for G¬P with a bound N is to check whether the DTP P can be reached in ≤ N steps.

For the upper bound we show how to encode a DTPRS (R, ∆) with the given bound N into a recursion-free GAXML system, and use the upper bound provided by [START_REF] Abiteboul | Static analysis of active XML systems[END_REF]. We recall that [START_REF] Abiteboul | Static analysis of active XML systems[END_REF] provides a simply exponential bound in the number of transition steps of the recursion-free GAXML system. Also notice that the DTPRS in Theorem 14 are not supposed to be positive -the lower bound relies on negations of DTPs.

The basic idea of the reduction from bounded modelchecking DTPRS to recursion-free GAXML is the following: we "guess" on-the fly the rules R1, R2, . . . , RM , M ≤ N , that are applied on a successful path of the DTPRS, and use function labels for pinpointing the nodes used by the matching of the corresponding locators. Suppose that nodes of locators have identifiers. A node having a child (leaf) labeled by the function call !(i, Ri, w) with i ≤ M , Ri ∈ R and w an identifier within the locator Li of rule Ri, is "guessed" to correspond to node w in the matching of the locator Li when applying rule Ri. Notice that node can have several function calls (i, Ri, v), (j, Rj , w) attached to it (but then, i = j, since the matching of Li should be injective).

We use the DTD in the invariant ∆ in order to ensure that (1) each of the (polynomially many) function labels !(i, Ri, w) occurs at most once at any time point, and (2) we use GAXML call/return guards for ensuring that calls related to rule Ri are only performed after all function calls (j, Rj, v) with j < i, have been completed, for each i. Checking (2) is done by forbidding the presence of function calls !(j, Rj, v) and ?(j, Rj, v) with j < i, whenever (i, Ri, w) is called. Similarly, when the result of a call ?(i, Ri, w) is returned, we forbid that it contains some label !(j, Rj, v) or ?(j, Rj, v) with j < i.

Applying rule Ri means calling all functions !(i, Ri, w) one-by-one (say in DFS order) and performing the associated actions. When we call the first function with index i, its guard also checks that the locator Li was properly guessed. A rename action must be simulated, since GAXML has no renaming facility: a call !(i, Ri, w) with w labeled by ren b in Li has as effect to attach label bi as a child (leaf) of node w. Checking which is the current label of a node is done by using negative guards: we look for a child bi that has no sibling c k with k > i. A delete action must be simulated, too, since GAXML has no deletion. A call !(i, Ri, w) with w labeled by del in Li has as effect to return a node with tag del. This might be syntactically inconsistent if the current node is a data node. However, standard encoding tricks can remedy this problem. For simplicity, let us assume that the tag del is always appended as a sibling of the node that is supposed to be deleted in DTPRS.

Finally, the append action is done as in GAXML, by performing the query and attaching the result. Here, we need to take care about the nodes that added via a forest F ∈ F, resp. a query. For such nodes, we must "guess" some attached function calls. In both cases we use external GAXML functions: for example, we can simulate the addition of an annotated copy of F via an external call, and use ∆ for checking that the right F was added. For query answers we may split a query Q in polynomially many copies, where for some of the copies, the head has attached external function calls. Their role is to generate (sets) of functions of type !(i, R, v) attached to nodes in head .

The last point is that we need to adapt the GAXML upper bound in order to take care of nodes marked by del : this can be done e.g. by extending the notion of matching tree patterns in such a way that none of the nodes to which tree patterns are matched, nor their ancestors, are allowed to have a child labeled by the tag del. It can be easily checked that the complexity checking a Tree-LTL formula for recursion-free GAXML still holds with this extended notion of matching. The reason is that the proof is based on small models obtained by taking tree prefixes of the bigger model. Obviously, the absence of children with tag del is preserved by taking tree prefixes.

The lower bound is adapted from the 2-NexpTime lower bound proof for recursion-free GAXML. We only recall the rough idea here.

The main ingredient of the proof is to create/check lists of length 2 n . This is done using data values, similarly as in the proof of Theorem 3. A "list" of length k corresponds to a tree of depth 2, where each node at depth one has 2 children, with distinct data values di, di+1. If each data value di occurs twice (except for d1 and d k+1 , which occur only once) we get a linear order, i.e. a list. Using n queries we can compute n steps of transitive closure and thus verify that k = 2 n . Obviously, this suffices for encoding a (2 n ×2 n ) tableau representing a computation of a 2 n -time bounded TM. Details are fairly easy to complete.

CONCLUSION

In this paper, we defined a rich class of systems describing active documents, possibly with recursive calls. We show that this class of systems is easy to use and powerful, demonstrating it on the MailOrder example. We studied the boundary of decidability for different properties and restrictions of the active documents. Namely, we show that termination from one document and pattern reachability from a set of documents are both decidable for positive DTPRSs, which are DTPRSs where the DTD is non-recursive, there is no negative guard or data invariants, and simple paths are bounded. We showed that without these restrictions, the problem is undecidable. We also show that the problem is undecidable for more complex properties (Tree LTL or termination from a set of active documents). Nevertheless, we also demonstrate on the MailOrder example that one can find bugs with our method.

Compared with GAXML [START_REF] Abiteboul | Static analysis of active XML systems[END_REF], the respective restrictions used to get decidability (positiveness and non-recursion) are incomparable. We showed however a reduction from (not necessarily positive) rewriting-length bounded DTPRS to recursion-free GAXML.

Considering further work it seems possible to get decidability results for another (incomparable) class of systems, namely DTPRSs whose new data variables do not get mutually distinct fresh values, but possibly arbitrary data values.

Figure 2 :

 2 Figure 2: The locator for service return.

  Here, ↑ I = {s ′ ∈ S | ∃s ∈ I s.t. s s ′ } denotes the upward closure of I wrt. , and Pred (I) = {s ∈ S | ∃t ∈ I, s -→ t} the set of immediate predecessors of states in I. A basis of an upwardclosed set I is a minimal set I b such that I = x∈I b ↑ x. Recall that whenever is a wqo, the basis I b of an upward closed set I is finite. Proposition 7. (TB,K , -→, ) has effective pred-basis.

We require that every tree in Init satisfies ∆.

A wqo is a reflexive, transitive and well-founded relation with no infinite antichain.

Although the TPRS model used in[START_REF] Genest | Tree pattern rewriting systems[END_REF] is slightly more general than the present model, it is easily seen that in the reduction in[START_REF] Genest | Tree pattern rewriting systems[END_REF] we use the TPRS model presented here.

APPENDIX

Proof of Proposition 2:

In both cases we encode a 2-counter machine with counters a, b. In the first one, a configuration (q, na, n b ) ∈ Q × N × N is encoded by a tree with root labeled q and two subtrees, one of the form a na a $ , and the other of the form b n b b $ . E.g. a zero test on the first counter corresponds to checking that the root has a child labeled a $ . Decrementing the first counter in state q (and going to state q ′ ) is done using the locator [q](-[a]([a $ ])), where the additional labels are: ren q ′ for the root, rena $ for the a-node and del for the a $ -node.

With non-recursive DTDs we can encode a configuration (q, na, n b ) by a tree of depth one, with root labeled by q, and na (n b , resp.) leaves labeled by a (b, resp.). The zero test is now done using a negative guard (e.g. "no a-leaf") or a negative invariant. In the latter case we split a transition in 2 steps: first we relabel the root by a transition from that state; second, we perform the corresponding rewriting as be-

The invariant states that whenever the root is labeled by a transition corresponding to a zero test of counter c, the tree has no c-leaf (c ∈ {a, b}).

Proof of Proposition 7:

It is sufficient to consider min(Pred (↑ T )), the set of minimal elements wrt.

in Pred (↑ T ), for each tree T ∈ TB,K . Fix a rule R = (L, G, Q, F, χ) with L = (VL, EL, rootL, ℓL, τL, condL, ℓ ′ L ) such that ℓ ′ L attaches additional labels {append , rena, del}, Q = {Q1, . . . , Qm} (Qi = body i head i), and F = {F1, . . . , Fn}. Let T1 = (V1, E1, root1, ℓ1) ∈ min(Pred (↑ T )), then

In the following, we show that the size of T1 (number of nodes) is bounded by the following constant (we actually show even more, by exhibiting T1 satisfying ∆):

Thus a finite basis, which is a finite subset of min(Pred (↑ T )), is computable.

Let

3 contains distinct copies of Fj, excluding the leaves labeled by those Qi,

4 contains distinct copies of the nodes of the forest Qi(T1), one for each node labeled by Qi in each copy of Fj .

The node set of T1 consists of

Now we consider an upper bound on the size of T1 that are sufficient to allow T1 satisfying ( * ),

• To guarantee the matching φ from L to T1:

The nodes in V ′ 1 ∪ V3 = φ(VL) and all their ancestors in T1 are sufficient. Note that in L, ancestor relations || may occur, so the inclusion of the ancestors of nodes in

• To witness that G is satisfied over T1 wrt. φ:

G is a positive Boolean combination of DTPs. To witness the satisfaction of each DTP Pi in G, we need keep a matching φi from Pi to T1 and all the ancestors of nodes of φi(Pi) in T1. Size: B|G|;

• To guarantee that T T ′ :

-

∩ ψ(VT ) and all their ancestors in T1, -At most |T | instantiations of head i on T1 by matchings from body i to T1 wrt. φ are sufficient. The ancestors of all the nodes of T1 in these instantiations should be preserved as well.

Size:

• Finally, to satisfy the DTD in ∆, T1 should be completed into a data tree of size at most (c.f. [START_REF] Abiteboul | Static analysis of active XML systems[END_REF])

where max(∆) is the maximum integer used in the definition of DTD in ∆.

Thus a sufficient upper bound for the size of T1 is

Proof of Proposition 10.

Let G = (V, E) and T = (W, F, r, θ) be a tree decomposition of G of width at most A and depth at most B.

Let P = v1 • • • vn be a path in G, and w1 • • • wn be a trace of P in T such that vi ∈ θ(wi), wi = wi+1 or there is a path in T from wi to wi+1 such that for each w = wi+1 on the path, vi ∈ θ(w).

Because all bags are of size at most A + 1, each bag can only occur at most A + 1 times on the sequence w1 • • • wn.

Let B0 be the minimal depth of wi's. Then there is only one bag at depth B0, say w, occurring on the sequence

) be all the occurrences of w on the sequence w1 • • • wn. Then all the bags on each sub sequence wi j +1wi j +2 • • • wi j+1 -1 is at depth no less than B0 +1. By induction hypothesis, each subsequence

Proof of Proposition 13:

We give a reduction from the exact reachability problem, i.e. checking whether a tree T2 can be reached exactly from a tree T1 via a TPRS R. This problem was shown to be undecidable in [START_REF] Genest | Tree pattern rewriting systems[END_REF] by a reduction from the reachability problem on reset Petri nets 5 .

We reduce the exact reachability problem for R to checking the Tree-LTL formula ϕ = G(P1 → F P2) (P1 and P2 are DTPs) for a TPRS R ′ and initial tree T0.

Let Σ be the set of tags of R, and let Σm be a disjoint copy of Σ. We will use five new tags root, α, β, γ, δ / ∈ T , thus T ′ = T ∪ Σm ∪ {root, α, β, γ, δ}.

The starting tree T0 consists of a root with one child labeled α, and one other child tree that equals T1.

The TPRS R ′ consists of R (adapted in order to take the additional root into account), plus two kinds of new rules (with empty guards):

In the rule above, T m 2 means that we use the tag copy Σm for T2. Technically, the rule renames α by β, renames each tag a ∈ Σ in T2 by am ∈ Σm, and appends a new node with tag γ.

The second type of additional rules is the following (here, a ∈ Σ parametrizes the rule): root α a γ -→ root δ Technically, the rule above deletes node α and the subtree rooted at a, and rename γ by δ.

Finally, the Tree-LTL property to be checked on (R ′ , ∆ ′ ) and initial tree T0 is ϕ = G(P1 → F P2), where P1 = [root]([γ]) and P2 = [root]([δ]). It is easy to see that T1 * -→ T2 via R iff R ′ does not satisfy ϕ from the initial tree T0: TP P1 can be generated only if from T1 we can reach a tree via R, that contains T2 as prefix. But then, TP P2 cannot be generated only if from T1 we reach exactly T2 (cf. second rule).


Etienne Côme
email: come@inrets.fr

Zohra Cherfi
email: cherfi@inrets.fr

Latifa Oukhellou
email: oukhellou@inrets.fr

Patrice Aknin
email: aknin@inrets.fr

Semi-supervised IFA with prior knowledge on the mixing process An application to a railway device diagnosis

Independent Factor Analysis (IFA) is a well known method used to recover independent components from their linear observed mixtures without any knowledge on the mixing process. Such recovery is possible thanks to the hypothesis that the components are mutually independent and non-Gaussians. The IFA model assumes furthermore that each component is distributed according to a mixture of Gaussians. This article investigates the possibility of incorporating prior knowledge on the mixing process and partial knowledge on the cluster belonging of some samples to estimate the IFA model. In this way, other learning contexts can be handled such as semi-supervised or partially supervised learning. Such information is valuable to enhance estimation accuracy and remove indeterminacy commonly encountered in unsupervised IFA such as the permutation of the sources. The proposed method is illustrated by a railway device diagnosis application and results are provided to show its effectiveness for this type of problem.

Introduction

A considerable amount of research has been devoted to solving diagnosis problems that aim to assign any measurement signal represented by a feature vector to one of labeled classes. Research in this area has employed either discriminative methods which directly focus on learning class boundaries, or generative approaches that aim to model the underlying distributions of the classes. The choice between these two approaches is closely linked to the classification problem. The generative technique seems to be interesting when a prior knowledge about the measurement process or about the data could be incorporated.

Traditionally, two learning paradigms are possible: supervised learning and unsupervised learning. In the recent years, other paradigms have emerged to mix them as semi-supervised [START_REF]Semi-Supervised Learning[END_REF] or partially supervised learning [START_REF] Ambroise | EM algorithm for partially known labels[END_REF]. In the former approach, one uses a mix of unlabeled and labeled examples, whereas in the latter, one can define constraints on the possible classes of the examples. A more general framework involving partially or imprecisely labeled samples can also be considered to handle situations where only imperfect knowledge on class labels is available. In this case, possibilist or belief function based labels can be used [START_REF] Denoeux | Handling possibilistic labels in pattern classification using evidential reasoning[END_REF]. The importance for such problems comes from the fact that labeled data are often difficult to obtain, while unlabeled or partially labeled data are easily available.

In this article, we present a generative diagnosis approach which allows to taking advantage from prior knowledge on the dependencies between the latent variables (linked to the system defects) and the observed variables (features extracted from the measurement signal). The generative model involved here assumes that observed variables are generated by a linear mixture of independent and non Gaussians latent variables (sources). Furthermore, each latent variable is assumed to be non Gaussian but generated according to a mixture of Gaussians. In this context, the well known method so called Independent Factor Analysis which is traditionally used in signal processing can be applied to recover the independent components from observed variables [7] [8].

This generative model is often considered within unsupervised learning framework. Both the mixing process and the source densities are only learned from the observed data. The paper investigates the possibility of incorporating partial knowledge on the latent variables to estimate such model. In the general case, this partial information will be encoded by a Dempster-Shafer mass function over the set of clusters describing each source but it can also be adapted to handle more specific learning problems such as the semi-supervised and the partially supervised cases. In this way, the mixture model of each source density will be supplied by the component origins of a subset of training samples. Such information is valuable to enhance estimation accuracy and remove indeterminacy commonly encountered in unsupervised independent factor analysis such as the permutation of the sources.

The approach will be illustrated applying it to a railway device diagnosis. This component can be considered as a complex system made up of a series of spatially related subsystems: the presence of a defect in one subsystem modifies not only its own signature but also those of subsystems located upstream. The aim of the diagnosis system is to identify the working state of the global component and localize the defective subsystem. This kind of system is present in many other applications such as electrical power distribution systems, gas or water distribution networks, telephone networks, road traffic,… The structure of the problem supplies therefore prior knowledge on the mixing process. As there is no influence between a subsystem S i state and signatures of subsystems located upstream, some elements of the mixing matrix are null. This information will be introduced in the model estimation.

I 3 I N I 1 I 2 S 1 S 3 S N S 2

Subsystems

Signatures

This article is organized as follows. We will first present Independent Component Analysis (ICA) and Independent Factor Analysis (IFA) as maximum likelihood estimation problems. The problem of learning the IFA model with prior knowledge on labels will then be addressed in Section 3. In Section 4, the method is applied to the diagnosis of a railway track circuit. The impact of using constraints on the mixing matrix and of semi-supervised learning will then be evaluated. The paper ends with a conclusion.

Independent Factor Analysis

Background on ICA

Independent Component analysis aims at recovering independent latent components {z 1 ,…,z S } from their observed linear mixtures [START_REF] Hyvarinen | Independent Component Analysis[END_REF] [START_REF] Bell | An information-maximization approach to blind separation and blind deconvolution[END_REF]. In its general formulation the relationship between latent and observed variables takes the following form:

A. = + ε x z (1)
where ε is a Gaussian noise independent from z and A a mixing matrix of size (D × S). The independence assumption is translated to a factorization of the joint distribution:

( ) ( )

1 S s s s p p z = = ∏ z (2)
The problem concerns the estimation of both the mixing matrix A and the realizations of the latent variables z. This general problem is handled differently depending on the number of the observed and latent variables D and S. If D > S the system is over-determined and a pre-processing is classically performed (by a Principal Component Analysis (PCA) to transform the observed variables x to S new variables, which also leads to remove the noise. After this pre-processing the noiseless ICA model is assumed to be:

A. = x z (3)
with A a square matrix. The distribution of the observed variables is given by: (

= S t s s s p p A. det A - = ∏ x x ) ( ) ( ) ( ) 1 1
Considering a set of N samples, the relation (3) can be written in matrix form as:

1 .A - = Z X ( 5
)
where X is the data matrix of size (N × S) and Z is the source matrix of size (N × S). The log likelihood for the N observations has the form

{ } ( ) ( ) ( ) ( ) ( ) ( ) 1 1 1 = N N S t s i s i s L A; N log det A log p A . - = = - + ∑∑ x x (6)
Once particular source density models have been chosen, the estimation of the mixing matrix A can be performed by differentiating the log likelihood with respect to either A or the un-mixing matrix W=A -1 its inverse:

t t A N . A . - Δ = -Φ Z ( 7
)
where Φ is the score function of each sample

( ) ( ) ( ) ( ) 1 1 1 S S t S log p z log p z A , , , z z - ⎛ ⎞ δ δ Φ = φ φ = - - ⎜ ⎟ ⎜ ⎟ δ δ ⎝ ⎠ z X
, and Z the matrix of estimated latent variables. In order to take account of known constraints on the mixing process, the log likelihood will be differentiated with respect to A rather than to W.

The maximum likelihood mixing matrix could be found with an ascended gradient procedure. A better optimization strategy is obtained by using the natural gradient [START_REF] Amari | A new learning algorithm for blind signal separation[END_REF] in which the climbing direction is found by multiplying the gradient by a first order Hessian approximation. The updating of the matrix A is achieved by the following learning rule

( ) ( ) ( ) ( ) 1 q q q t A A A . N + = + τ Φ - Z I ( 8
)
where τ is the learning rate that must be tuned, I the identity matrix of size (S x S).

Independent Factor Analysis Principle

The ICA model requires the choice of the probability density functions of the sources. They can be fixed by using prior knowledge, or according to some indicator which allows switching between sub and super Gaussian densities [START_REF] Hyvarinen | Independent Component Analysis[END_REF]. An alternative solution investigated by several authors [START_REF] Attias | Independent factor analysis[END_REF] [8], so called Independent Factor Analysis (IFA), consists to model each source density as a mixture of Gaussians so that a wide class of densities can be approximated.

In IFA model, each latent variable is assumed to be distributed according to a mixture model given by: ( ) ( )

1 = s K s s S s s k s k k k p z N z ; , = π μ σ ∑ (9)
where N refers to the unidimensional Gaussian distribution. The model parameters are the mixing matrix A and the parameters of latent variable distributions. The set of all model parameters is denoted θ = (A, π 1 ,…., π S , θ 1 ,…, θ S , μ 1 ,…., μ S , σ 1 ,…., σ S ). π S is the vector of clusters proportions of source s which sum to one, μ S and σ S are the vectors of size K s containing the means and the variances of each cluster.

Traditional methods for learning these parameters from an independently and identically distributed learning set use the likelihood function which can be obtained by substituting the density function p s in (6) by its definition given in (9):

{ } ( ) ( ) ( ) ( ) 1 1 1 1 = s N K N S s t s s s i k k k i s k L A; N log det A log N A .x , , - = = = - ⎛ ⎞ + π μ σ ⎜ ⎟ ⎜ ⎟ ⎝ ⎠ ∑∑ ∑ x (10)
As outlined previously a gradient climbing algorithm can be set up to optimize such function with respect to A if the source densities are frozen. Similarly, with A kept fixed this likelihood function can be optimized with respect to the parameters of each source model by means of an Expectation Maximization (EM) algorithm. These remarks lead to the definition of an alternating optimization algorithm which takes the form a Generalized Expectation Maximization algorithm (GEM) since the objective function is only increased during the maximization step [START_REF] Dempster | Maximum likelihood from incomplete data via the EM algorithm[END_REF]. It should be noted that two indeterminacies affect the ICA model: the scaling and the permutation of sources.

Partially-supervised learning in IFA

The IFA model is often used in unsupervised learning context. The idea that we investigate in this paper is to incorporate partial knowledge on the cluster belonging of some samples in the learning process. In this way, other learning contexts can be handled such as semi-supervised or partially supervised learning. For that purpose, an objective function generalizing the likelihood function needs to be defined and an EM algorithm dedicated to its optimization has to be set up.

Derivation of a Generalized likelihood criterion

We shall assume a learning set of the form X iu = {(x 1 ,m 1 ), . . . , (x N ,m N )}, where

1 2 S i i i i m m ,m , ,m ⎡ ⎤ = ⎣
⎦ is a set of basic belief assignments or Dempster-Shafer mass functions [START_REF] Dempster | Upper and lower probabilities induced by a multivalued mapping[END_REF] encoding our knowledge on the cluster belonging of sample i for source s. The set of all possible cluster for source s will be denoted Y s ={c 1 ,…,c Ks }. The observed data x i will be assumed to be generated according to the IFA model defined in Section 2.

Depending on the choice of the mass functions, this formulation can therefore be seen as addressing a more general issue which encompasses unsupervised, supervised and semi-supervised learning paradigms as mentioned in Table 1.

The concept of likelihood function has strong relations with that of possibility, and more generally plausibility as already noted by several authors. Furthermore, selecting the simple hypothesis with highest plausibility given the observations is a natural decision strategy in the belief functions framework.

The proposed estimation principle to search the value of θ is based on the maximization of the conditional plausibility given the data [START_REF] Côme | learning from partially supervised data using mixture models and belief functions, Pattern recognition[END_REF]:

( ) iu ˆarg max pl Θ Θ θ = θ X (11)
s 1 s i m = Y 1 s ik pl , k = ∀ Supervised ( ) 1 s i k m c = 1 0 s s ik ik ' pl ,pl k' k = = ∀ ≠ Partially supervised ( ) 1 s i m C = 1 0 s ik k s ik k pl i f c C pl i f c C = ∈ = ∉ "soft" supervised s i m ? [ ] 0 1 s ik pl , ∈
Previous work on mixture model estimation with belief function based labels [START_REF] Côme | learning from partially supervised data using mixture models and belief functions, Pattern recognition[END_REF] using such principle can easily be extended to the IFA model. It can be shown that the logarithm of the conditional plausibility of the IFA parameters given the dataset can be expressed as:

{ } ( ) ( ) ( ) ( ) 1 1 1 1 = s N K N S s s t s s ik s i k k k i s k L A; N log det A log pl N A .x , , - = = = - ⎛ ⎞ + π μσ ⎜ ⎟ ⎜ ⎟ ⎝ ⎠ ∑∑ ∑ x (12)
where s ik pl are the plausibilities of each cluster k of source s for each sample i. Once the criterion is defined, the remaining work concerns its optimization. The next section details this approach in the particular context of semi-supervised context.

Semi-supervised learning in IFA model

In semi-supervised learning approach, the IFA model is built from a combination of M labeled and N-M unlabeled samples. Consequently the log-likelihood can be decomposed in two parts corresponding, respectively, to the supervised and unsupervised learning examples. Criterion (12) can then be rewritten as:

{ } ( ) ( ) ( ) ( ) ( )
( )

1 1 1 1 1 1 1 = s s N K M S s s t s s ik s i k k k i s k K N S s t s s s i k k k i M s k L A; N log det A l log N A .x , , log N A .x , , - = = = - = + = = - + π μ σ ⎛ ⎞ + π μ σ ⎜ ⎟ ⎜ ⎟ ⎝ ⎠ ∑∑∑ ∑ ∑ ∑ x (13) with { } 0 1 S K s ik l , ∈
are binary variables encoding the class of sample i,

1 s ik l = if sample i comes from cluster k c , and 0
s ik l = otherwise.
The GEM algorithm can easily be adapted to optimize this function. The modification affects only the E step, where the posterior probabilities s ik t are only computed for unlabeled observations. During the M step, the known labels are used instead of the s ik t , for the labelled data.

Algorithm GEM, pseudo-code for semi-supervised IFA

Inputs: centered data matrix { } 1 = i N i
x and labels { } Initialize parameters vector ( )

0 0 1 0 0 1 0 0 1 0 0 ( ) ( ) ( ) S( ) ( ) S( ) ( ) S( ) A , , , , , , , , , θ π π μ μ σ σ = … … … 0 q ← While increment in log likelihood > precision threshold do 1 A - = Z X // Source Update For all sources { } 1 s , ,S ∈ … For all clusters { } 1 s k , ,K ∈ … do // E step 1 s( q ) s ik ik t l , i M = = 1 1 s s( q ) s( q ) s( q ) s( q ) k i s k k ik K s( q ) s( q ) s( q ) k k i s k ' k ' N( ; , ) t , i M N N( ; , ) π μ σ π μ σ ′ ′ = = =+ ∑ Z Z End for End for For all sources { } 1 s , ,S ∈ … For all clusters { } 1 s k , ,K ∈ … do // M step 1 1 1 N s( q ) s( q ) k i k i t N π + = = ∑ 1 1 1 1 N s( q ) s( q ) k i k i s s( q ) N i i ik t t + = = = ∑ ∑ μ Z 1 1 2 1 1 1 N s( q ) s( q ) s( q ) k i k i s k s( q ) N i i ik t ( ) t σ + + = = = - ∑ ∑ Z μ End for ( ) ( ) 1 φ + Φ = q .S
. S Z // Score function update End for ( ) ( ) ( ) ( )

1 q q q t A A A . NI + = + τ Φ - Z // Mixing matrix update 1 q q ← +

End while

Outputs : estimated model parameters ( )

1 1 1 ML S S S
A, , , , , , , , ,

θ π π μ μ σ σ = … … …

Railway application 4.1. Track circuit principle

The application considered in this paper concerns the automatic diagnosis of a railway track/vehicle transmission system. On high speed lines, signalling information is transmitted to the train driver using modulated currents that are injected into the rail and picked up by antennas mounted under the train. This system, called a track circuit, provides a great deal of information that is useful for train movement, such as the speed limit on a given track section.

So, the railway track is divided into different sections, each section is equipped by a track circuit consisting of (see Figure 2): 1) a transmitter connected to one of the two section ends that delivers a frequency modulated alternating current 2) the two rails that can be considered as a transmission line 3) at the other end of the track section, a receiver that detects the presence or the absence of train on the section 4) trimming capacitors connected between the two rails at constant spacing to compensate for the inductive behaviour of the track. Electrical tuning is then performed to limit the attenuation of the transmitted current and improve the transmission level. The number of compensation points depends on the carrier frequency and the length of the track section.

Diagnosis purpose and methodology

The different parts of the system are subject to malfunctions (due to aging, or track maintenance operations) that must be detected as soon as possible in order to maintain the system at the required safety and availability levels. In the extreme case, this causes an unfortunate attenuation of the transmitted signal that leads to the stop of the train. The purpose of diagnosis is to inform maintainers about track circuit failures on the basis of the analysis of a specific current, recorded by an inspection vehicle. This paper will focus on trimming capacitor defects that affect capacitor internal capacitance. Figure 2 shows examples of signals simulated along a 1500m track circuit: one of them corresponds to an absence of defect, while the others correspond to a defective 9 th capacitor. The idea is to consider the track circuit as a global system S, and each trimming capacitor as a subsystem S i . A defect on one subsystem is represented by a continue value of the capacitance parameter. The proposed diagnosis method must take account of a variable number of subsystems depending on the track circuit length and a spatial relationship between subsystems.

A generative model can be build where the observed variables are the coefficients of the local polynomial approximating the measuring signal located between two subsystems, and the latent variables are the capacitances of each trimming capacitor. In this way, the diagnosis of a shorter system (N'<N) simply uses a sub-model extracted from the global one and the model structure can also take advantages from prior knowledge (downstream-upstream dependencies) as shown in Figure 1 which leads to a block lower triangular mixing matrix.

Results and discussion

To access the performances of the method, we considered a track circuit of S = 18 subsystems (capacitors) and built a database containing noised signals obtained for different values of the capacitance of each capacitor. 2500 signals are thus obtained of each capacitor where 1000 are used in the training phase while the 1500 others are employed for the test phase to estimate the performances. A piecewise approach is then adopted for the signal representation: each arch was approximated by a second degree polynomial of which two coefficients are used as observed variables for each node in the generative model.

Given an observation matrix, the aim is to recover S latent variables from 2*S observed ones with the hope that they will be strongly correlated with the variables of interest that are the capacitor capacitances. As prior information on the mixing matrix is available, PCA cannot be used as a preprocessing because the mixing structure will be lost. 2*S latent variables are therefore extracted, the S most correlated with the capacitances being kept and the others being considered as noise. We have investigated the influence on the method results of using different amount of labeled samples and imposing constraints on the mixing matrix.

The comparison between the different settings will be quantified by the correlation between the true capacitances and their estimates calculated on the test set. The results presented in Figure 3 show that the source permutation is avoided when the components origins of a sufficient amount of training samples is provided. The non detection rate is also decreased in this case since no capacitor is weakly correlated with its estimate.

Figure 4 shows the mean correlation between estimated latent variables and capacitor capacitances function of the number of labeled samples when the mixing matrix is constrained or not. Fifty random starting points were used for the GEM algorithm and only the best solution according to the likelihood was kept. To avoid the source permutations which occur when not enough labeled samples are supplied, the mean correlation was computed according to the best permutation of the sources. As expected, when the number of labeled data increases, the mean correlation also increases. Furthermore, when prior information on the mixing matrix is provided, the sources are well estimated. The use of labeled data seems less influent when prior information such as constraints on the mixing matrix are available.

Conclusion

Here we presented a diagnosis method based on independent factor analysis which aims to recover the latent variables linked to the defects from their linear observed mixtures. In this paper, we investigate the possibility of incorporating knowledge on the cluster belonging of some samples and also on the structure of the mixing matrix to estimate the IFA model. A generalized maximum likelihood criterion was defined and a GEM algorithm dedicated to its optimization was given. The proposed approach was illustrated on a railway device diagnosis application. The results show that our solution is able to take advantage of information on class labels and on the mixing form. The benefits are in terms of source estimation accuracy and no permutation of sources. Further studies will be carried out to apply the approach on real signals in order to take account of imprecise and uncertain labels (label noise).

Figure 1 .

 1 Figure 1. Diagnosis of a complex system made up of a series of spatially related subsystems S 1 , S 2 ,….,S N

Figure 2 .

 2 Figure 2. Track circuit representation and inspection signal without defect and with a defective 9 th capacitor

Figure 3 .

 3 Figure 3. Correlation between estimated latent variables and true capacitor capacitances, computed on a test set for unsupervised IFA (a) and semi-supervised IFA with constraints on the mixing matrix and 40% of labeled samples among 1000 training samples (b).

Figure 4 .

 4 Figure 4. Mean correlation between estimated latent variables and true capacitor capacitances evaluated on a test set, function of the percentage of laleled samples among the 1000 training samples, for IFA with and without constraints on the mixing matrix.

Table 1 .

 1 Different learning paradigms and soft labels

		Mass function	plausibility
	Unsupervised	( )