Lucie Campagnolo
email: lucie.campagnolo@alumni.enseeiht.fr

Milan Nikolic

Julien Perchoux

Yah Leng Lim

Karl Bertling

Karine Loubiere

Laurent Prat

Aleksandar D Rakic

Thierry Bosch

Milan Nikolić

Karine Loubière

Aleksandar D Rakić

Flow profile measurement in microchannel using the optical feedback interferometry sensing technique

Keywords: pdfcreator=HAL,pdfproducer=PDFLaTeX,pdfsubject=Physics [physics]/Physics [physics]/Optics [physics.optics], Physics [physics]/Physics [physics]/Instrumentation and Detectors [physics.ins-det], Physics [physics]/Physics [physics] Photonic device, Laser sensor, Optical feedback interferometry, Flow profile measurement PACS PACS code1, PACS code2, more

,

Introduction

There has been a growing interest to develop microscale devices that can manipulate and transport small amounts of fluid, such as microreactors, micromixers, and lab-onchip devices. Miniaturization and integration of chemical operations have many specific advantages such as increased speed, efficiency, portability and reduction of reagent consumption [START_REF] Anxionnaz | Heat exchanger/reactors (hex reactors): Concepts, technologies: State-of-the-art[END_REF]. Indeed, decreasing device size allows a reduction of technology constraints to the benefit of chemistry [START_REF] De Mello | But what is it good for? applications of microreactor technology for the fine chemical industry[END_REF][START_REF] Ahmed | Enhancement of reaction rates by segmented fluid flow in capillary scale reactors[END_REF]. This has created a need for new diagnostic tools with spatial resolution in the order of several micrometers. Accurate measurement of velocity distribution in miniature channels is of great interest to provide better understanding of fluidic transport, mixing and fluid properties. Currently, particle imaging velocimetry (PIV) is the most advanced technique for obtaining accurate measurement of velocity distribution in sub-millimeter channels [START_REF] Meinhart | Piv measurements of a microchannel flow[END_REF][START_REF] Santiago | A particle image velocimetry system for microfluidics[END_REF][START_REF] Sarrazin | Experimental and numerical study of droplets hydrodynamics in microchannels[END_REF]. However, this kind of sensing technology is extremely complex, expensive and bulky.

Optical Feedback Interferometry (OFI) [START_REF] Bosch | Optical feedback interferometry[END_REF]) offers a rapid, direct, non-invasive and high-resolution alternative for determining flow rate within flow-channels [START_REF] De Mul | Self-mixing laserdoppler velocimetry of liquid flow and of blood perfusion in tissue[END_REF]. This technique allows the laser itself to function as both the light source and the detector, making possible low-cost and compact sensors. A number of preliminary applications to flow rate measurement have been previously reported [START_REF] Zakian | Particle sizing and flow measurement using self-mixing interferometry with a laser diode[END_REF][START_REF] Norgia | Low-cost optical flowmeter with analog front-end electronics for blood extracorporeal circulators[END_REF] and recently measurement of flow in microchannels has been demonstrated [START_REF] Kliese | Rapid scanning flow sensor based on the self-mixing effect in a vcsel[END_REF].

In this study a flow sensor based on OFI is presented that accurately measures the fluid flow profile in sub-millimeter channels. It employs a low-cost Vertical-Cavity Surface-Emitting Laser (VCSEL), a simple 2-lens optical setup and senses fluid flow rate by monitoring the change in the laser's terminal voltage [START_REF] Lim | Self-mixing imaging sensor using a monolithic vcsel array with parallel readout[END_REF]. This sensor has been designed to operate in the single scattering regime, that is of interest for a number of chemical and biomedical applications [START_REF] Norgia | Selfmixing laser doppler spectra of extracorporeal blood flow: A theoretical and experimental study[END_REF]. The aims of this paper are: (i) to present the theory of OFI for fluid flow-rate measurement, (ii) to demonstrate the performance of an OFI flow sensor that measures local velocity in fluids with spatial resolution in the micrometer range and enables reconstruction of a velocity profile inside a microchannel, (iii) to validate the performance of the sensor with deterministic flows that can be easily described with classical analytical solutions.

In Sec. 2., OFI theory applied to fluid flow rate measurement for the single scattering regime is briefly discussed. A detailed description of the experimental set-up is given in Sec. 3. Section 4 presents the experimental results, highlighting the accuracy and the repeatability of the sensor for velocity profile measurement for both Newtonian and non-Newtonian fluids in a circular microchannel. Finally, conclusions are drawn in Sec. 5.

OFI applied to fluid flow rate measurement

The optical feedback effect occurs when a portion of the light emitted from a laser is reflected from an external target and re-enters the laser cavity [START_REF] Kane | Unlocking Dynamical Diversity: Optical Feedback Effects on Semiconductor Lasers[END_REF]. This optical feedback causes measurable changes in the laser frequency and emitted power [START_REF] Giuliani | Laser diode self-mixing technique for sensing applications[END_REF]. The effect can also be observed by monitoring the change in the laser terminal voltage, allowing velocity, distance or displacement measurement [START_REF] Lim | Self-mixing imaging sensor using a monolithic vcsel array with parallel readout[END_REF][START_REF] Lim | Self-mixing flow sensor using a monolithic vcsel array with parallelreadout[END_REF].

When a laser illuminates an object moving with a velocity V target , the reflected optical wave experiences a Doppler shift in frequency. The difference frequency, f Doppler is usually referred to as the Doppler frequency [START_REF] Albrecht | Laser Doppler and Phase Doppler Measurement Techniques[END_REF][START_REF] De Groot | Backscattermodulation velocimetry with an external-cavity laser diode[END_REF]:

f Doppler = 2nV target cos(θ ) λ ( 1
)
where θ is the angle the target velocity vector makes with respect to the propagation axis of the laser beam, λ is the laser wavelength in free-space and n the refractive index of the surrounding medium. The Doppler signal is acquired through variations in laser terminal voltage and will be referred to as the OFI signal.

Measuring the flow rate of a moving fluid is similar to measuring the velocity of a solid object. Light emitted from the laser is focused into the fluid by an optical system therefore defining the sensing volume from where the signal is being obtained. Light scattered from a single moving particle that is suspended in the fluid, is shifted in frequency by the Doppler effect, Eq. (1). The optical system collects light back-scattered from a number of different particles with different velocities, leading to a distribution of Doppler frequencies in the OFI signal spectrum instead of a single beat frequency peak. For a liquid where the particle concentration is low enough that multiple scattering can be ignored, a peak appears in the frequency spectrum corresponding to the mean Doppler frequency of the moving particles within the sensing volume.

In OFI systems the illumination and collection beams spatially overlap. Assuming the laser operates in the fundamental Gaussian mode, the measurement volume centred around the beam focus, is defined as the volume within which the optical intensity has a magnitude higher than 1/e 2 of the intensity peak value [START_REF] Albrecht | Laser Doppler and Phase Doppler Measurement Techniques[END_REF]. Nevertheless, a very small particle in the measuring volume may not reflect sufficient light to be detected; therefore the detection volume in this case is smaller than the measurement volume. On the contrary, a large number of highly reflective particles may be detected, even if they are slightly outside the measurement volume as defined above. Under these conditions, the detection volume is clearly larger than the measurement volume. Throughout the article it is understood that the calculated measurement volume is only an estimate of the effective detection volume.

Experimental set-up

The laser used was a commercial VCSEL (Firecomms, model RVM665T) lasing at 667 nm with a threshold current, I th , of 0.8 mA. In all experiments the VCSEL was operated at a constant current of 2.25I th , where it was found to exhibit good optical feedback sensitivity and stability, as well as single mode behaviour. A dual-lens system was used (Fig. 1) with collimating (lens 1) and focusing (lens 2) lenses of respective focal lengths 15.29 and 8 mm. The laser beam axis was angled at 80 • relative to the flow direction. The two lenses were chosen so as to minimize the spot size, and hence improve the spatial resolution of the measurement system. The assembled optical head was characterized with a beam profiler, and the spot diameter in focus was measured to be 32.26 µm. This results in a sensing volume of 7.16x10 5 µm 3 , providing for a sufficient spatial resolution to scan the channel, which has a 320 µm internal diameter. The optical head was mounted on a computer controlled 3-axis motorized translation stage. The focus point was stepped through the channel by the translation stage to obtain the measurement points needed to reconstruct the flow profile.

The voltage across the VCSEL terminals was AC-coupled to a low-noise voltage amplifier and then fed into an analogto-digital converter for digital signal processing on computer. A Fast Fourier Transform (FFT) was performed in software to obtain the signal frequency spectrum. All the reported Doppler spectra have been obtained as the mean of 64 successively acquired spectra. The acquisition time was lower than 10 ms. Therefore, the sensor response time can be considered as being close to real-time.

A microfluidic channel with circular cross-section of inner diameter 320 µm was fabricated using Polydimethylsiloxane (PDMS) with the refractive index of 1.4 [START_REF] Mark | Polymer Data Handbook[END_REF]. The liquid under test was composed of 98 % water and 2 % milk by mass.

For a laminar flow, the velocity profile in a circular channel is parabolic, with the velocity increasing from zero at the wall (no slip boundary condition) to a maximum value at the centre. The Reynolds number, which indicates laminar regime is defined by:

R e = QD H νA ( 2
)
Where Q is the volumetric flow rate (m 3 /s), D H is the hydraulic diameter (m), A is the pipe cross-sectional area (m 2 ) and ν is the kinematic velocity (m 2 /s), that can be expressed by:

ν = µ ρ ( 3
)
Where µ is the dynamic viscosity of the fluid (Pa.s) and ρ is the density of the fluid (kg/m 3 ). By assuming that the particle concentration in our solution is low enough that the parameters of the fluid can be approximated to those for water (µ = 0.001 Pa.s, ρ = 997 kg/ m 3 at 20 • C) and with respect to the flow rates imposed (from 5 to 50 µL/min), the Reynolds number varies from 0.33 to 33 (laminar regime).

The velocity profile in a circular cross-section channel for Newtonian fluid in the laminar regime is given by Poiseuille's law. In order to investigate non-Newtonian flow profiles, xanthan gum powder was added in various concentrations to

µ = K • γm (4)
where K is the consistency index and m the flow index. They are determined from experimental rheograms. The analytical solutions for the velocity profile when a purely shearthinning fluid flows inside a circular channel is given by:

V (z) = 2Q S 3m m + 1 1 + z R m+1 m (5)
where Q is the pumping flow rate, S the area of the crosssection of the channel, z the distance from the center, and R the radius of the channel.

Experimental Results

Sensor calibration

The sensor was calibrated using a solution of 98 % distilled water and 2 % milk. First, the laser beam focus was moved to the middle of the channel (position B in Fig. 2) and the position was then further adjusted to where the OFI signal exhibited the highest frequency (Fig. 3). Then, the average Doppler frequency within the sensing volume was extracted from the OFI signal spectrum using the following fitting function:

a f -b + c + d exp -f -f peak 2 h (6)
where a, b and c are the fitting parameters depending only on the experimental set-up. Thus, a and b in the first term are the parameters used for fitting the 1/f noise, and parameter c in the second term is used for fitting the broadband noise in the spectrum. In the last term of the fitting function, d corresponds to the strength of the Doppler peak, the half-width The final step of the calibration procedure consists in calculating the incident angle θ from the slope of the fitting in Fig. 4(b). It was calculated to be 80.25 • , close to the value given by the goniometer stage.

Laminar flow profile : Newtonian fluid

To measure the velocity profile, the laser focus was first moved back to position A in Fig. 2, and the laser scanned across the flow channel (z direction in Fig. 2) in 10 µm steps toward position C.

The first liquid under test was milk diluted in distilled water (1:50), pumped at 20 µL.min -1 , which corresponds to an average velocity of 4.15 mm.s -1 . The experimentally reconstructed flow profile is plotted in Fig. 5. The solid curve represents the theoretical parabolic velocity profile described by Poiseuille's law, whereas the blue curve represents the measured velocity at each radial location. The experiment agrees well with theory in the mid to high flow rate range.

The difference between the experimental and the theoretical velocities is plotted in Fig. 6. Notwithstanding the first point (with a discrepancy of 3 %), this measurement indicates good agreement with theory. Over the usable range, the relative error for each measurement point was less than 1.8 %. The error near the channel's walls can be attributed to the difficulty in fitting the Gaussian peak close to the low frequency noise induced by the system.

To estimate the repeatability of the measurement, the standard deviation for 8 consecutive scans was calculated for each measurement point (Fig. 5). In addition to the increase of the error observed in the previous paragraph, the sensor shows also a compromised repeatability near the channel's wall. The discrepancy observed at low particle velocities can be also explained by difficulties in extracting the Gaussian peak from low frequency noise. Nevertheless, overall this measurement indicates good repeatability. The minimum spatial resolution of the system depends on the fluid composition and velocity, and could not be accurately measured. The laser spot size has been estimated at 32 µm, but Fig. 5 and Fig. 8 show that the effective spatial resolution of the sensor is better than 10 µm. These preliminary results demonstrate the feasibility of OFI measurement in microchannels of size well below 320 µm. Future work shall consist in characterizing accurately the OFI spatial resolution as a function of the fluid parameters and the optical system.

Laminar flow profile : Shear thinning fluid

Adding a shear thinning fluid to the initial milk-water mix leads to a different velocity distribution in microchannels. Within the laminar range, the velocity profile is expected to become flatter in the center as the solution becomes shearthinning. Four solutions at different xanthan gum concentrations (0, 0.25, 1, and 3 g/L) were pushed through the flow channel at a pumping rate of 30 µL.min -1 . We measured the relationship between the shear rate and the viscosity for each solution, using a rheometer (TA instruments AR 2000) in a small-angle cone and plate configuration (Fig. 7). The temperature was controlled at 25 • C. The power law exponent m was then extracted from these experimental rheograms using Eq. ( 4), and found to be 1, 0.73, 0,56, and 0.37 respectively. The theoretical velocity profiles are obtained using Eq. ( 5) and the calculated values of m, and are compared to the measurement results in Fig. 8. The experimental profile for non-Newtonian fluid in the laminar range shows also good agreement with theory (Eq. 5). Thus the discrimination of different velocity profiles by OFI is demonstrated, and the technology's application to the measurement of complex flow behaviour is verified.

Conclusion

An OFI microfluidic flow sensor capable of accurately measuring flow rates and profiles in micrometer-scale channels was presented. Flow profile reconstruction of laminar flow in a channel with an internal diameter of 320 µm was demonstrated. OFI differs from the well established technique of µ-PIV by the simplicity of implementation and the low cost of its technology. The OFI sensors can be fully automated, offering opportunity of on-site implementation with unskilled operators. OFI possible applications include following the establishment of flow steady-state regime, detecting the deviations from normal behaviour, and performing rapid one dimensional flow scans. However, µ-PIV remains so far the most powerful tool to accurately measure fluid flow distribution in complex systems (multiphase flows, complex rheology..), and to provide velocity distribution in large two-dimensional areas. Future extensions of this work include operation in the multiple scattering regime and characterization of non-laminar flows. Considering it is a single point raster-scanning technique (in its current implementation), OFI has limited applicability for mapping large flow-channels. Its demonstrated acquisition time is around 10 ms per single point measurement which effectively limits the image resolution achievable. Nevertheless, the use of a VCSEL array [START_REF] Lim | Self-mixing imaging sensor using a monolithic vcsel array with parallel readout[END_REF][START_REF] Lim | Self-mixing flow sensor using a monolithic vcsel array with parallelreadout[END_REF] can remove the need for mechanical scanning completely, thus improving acquisition time, spatial resolution and reducing mechanical complexity of the system. This should lead to the acquisition of a complete map of the velocity distribution in a channel in about 10 ms. Using OFI to characterize liquids through measurement of their flow profiles could lead to innovative, new, low-cost sensors, and brings about new possibilities for the design of enhanced Bio-system-on-a-Chip.

Fig. 1

 1 Fig. 1 Experimental setup

Fig. 2

 2 Fig. 2 Diagram showing the scan configuration with respect to the zaxis of the flow channel. The angle calibration is calculated at position B, and the velocity profile is measured from A to C. The flow channel has a 160 µm internal radius R

Fig. 3

 3 Fig.3OFI signal in frequency domain measured at the middle of the channel and the corresponding fitting curve (Eq. (6)). The mean frequency in the sensing volume is calculated by extracting the Doppler frequency of the signal

Fig. 4

 4 Fig.4(a) OFI signal in the frequency domain for several flow rates (0, 10, 20, 30, 40 and 50 µL.min -1 ) (b) Plot of the Doppler frequency as a function of the flow rate. The peak frequency shows a linear relationship with velocity. The angle between the flow direction and the optical beam can be estimated from the slope of this relationship, and has been calculated to be 80.25 •

Fig. 5 AFig. 6

 56 Fig. 5 A comparison between theoretical profile (solid red curve) and 8 consecutive measured profiles (blue errorbars) along the centre-line of the flow channel with a flow speed of 20 µL/min -1 . The liquid is milk (2 %) diluted in water

Fig. 7

 7 Fig. 7 Experimental rheograms for various concentrations of xanthan gum (0.25 (cross) 1 (circle) and 3 g/L (square)). The viscosity of each solution as a function of the shear rate applied are plotted in logarithm

Fig. 8

 8 Fig. 8 Measured (markers) and theoretical (solid line) velocity profile in a 320 µm channel for various solutions of xanthan gum (0 (plus), 0.25 (cross), 1 (circle), and 3 g/L (square))

Acknowledgements This work was performed in part at the Queensland node of the Australian National Fabrication Facility, a company established under the National Collaborative Research Infrastructure Strategy to provide nano and microfabrication facilities for Australia's researchers. This research was supported under Australian Research Council's Discovery Projects funding scheme (DP0988072), and The Commonwealth of Australia International Science Linkages programme (FR090026)


Nicole Bidoit
email: bidoit@lri.fr

Dario Colazzo
email: colazzo@lri.fr

Federico Ulliana
email: fulliana@lri.fr

Type-Based Detection of XML Query-Update Independence

This paper presents a novel static analysis technique to detect XML query-update independence, in the presence of a schema. Rather than types, our system infers chains of types. Each chain represents a path that can be traversed on a valid document during query/update evaluation. The resulting independence analysis is precise, although it raises a challenging issue: recursive schemas may lead to infer infinitely many chains.

A sound and complete approximation technique ensuring a finite analysis in any case is presented, together with an efficient implementation performing the chain-based analysis in polynomial space and time.

INTRODUCTION

A query and an update are independent when the query result is not affected by update execution, on any possible input database. Detecting query-update independence is of crucial importance in many contexts: i) to minimize view re-materialization; ii) to ensure isolation, when queries and updates are executed concurrently; iii) as outlined in [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF], to enforce access control policies, when the query is used to define the part of the database that must not be changed by a user update.

In all these contexts, benefits are amplified when query-update independence can be checked statically. In order to be useful, every static analysis technique must be sound: if query-update independence is statically detected, then independence does hold. The inverse implication (completeness) cannot be ensured in the general case, since static independence detection is undecidable (see [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF]). This means that if a static analyzer is used, for instance, in a view maintenance system, sometimes views are re-materialized after updates even if not needed, because the analysis has not been smart enough to statically detect a view-update independence. Useless view re-materialization frequently occurs if a static analyzer with low precision is adopted. This can lead to great waste of time, since view materialization cost can be proportional to the database size.

High precision of static independence analysis can be ensured by taking into account schema information. In many contexts, schemas are defined by users, mainly by means of the DTD or XML Schema languages, while in other contexts quite precise schemas, in the form of a DTD, can be automatically inferred, by using accurate and efficient existing techniques like the one proposed by Bex et al. in [START_REF] Bex | Inference of concise regular expressions and DTDs[END_REF].

State of the Art

Schema-based detection of XML query-update independence has been recently investigated. The state of the art technique has been presented by Benedikt and Cheney in [6]. This technique infers from the schema the set of node types traversed by the query, and the set of node types impacted by the update. The query and the update are then deemed as independent if the two sets do not overlap. This technique is effective since the static analysis i) is able to manage a wide class of XQuery queries and updates, ii) can be performed in a negligible time, and iii) as a consequence, even on small documents, can avoid expensive query re-computation when independence wrt an update is detected. However, the technique has some weaknesses. As illustrated in [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF], in some cases, independence is not detected, due to some over-approximation made by the type inference rules.

For example, this technique cannot detect independence between the query q1=//a//c and the update u1=delete //b//c, when the schema enforces that c descendants of b nodes are never descendants of a nodes. This is because the type inference technique of [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF] infers the type c both for the query path and the update path, without considering contextual information about the inferred types. Since the query and update types overlap, independence is wrongly excluded. Indeed, the technique is not precise enough when ancestor or descendant axes are used in queries and updates.

The way XPath axes are typed is not the only source of low precision of this technique. Consider documents typed by the well known bibliographic DTD used in [START_REF]XML Query Use Cases[END_REF], the query q2=//title and the update u2=for x in //book return insert <author/> into x. The technique of [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF] infers bib, book and title as types traced by q2, and book as type impacted by u2. According to this technique, the two expressions share the type book, hence independence is not detected, while it holds.

In none of the above examples, independence can be detected by techniques ignoring schema information like the path-based approach proposed by Ghelli et al. 1 [START_REF] Ghelli | Commutativity analysis for XML updates[END_REF] and the recent destabilizersbased approach proposed by Benedikt and Cheney [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF]. Following these approaches, for the example q1-u1, the paths //a//c and //b//c are deemed as overlapping since, for instance, documents matching the path /a/b/c match both paths and similarly, for example q2-u2 and the paths //title and //book.

Contributions

This paper proposes a novel schema-based approach for detecting XML query-update independence. Differently from [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF][START_REF] Cheney | FLUX:FunctionaL Updates for XML[END_REF][START_REF] Colazzo | Static analysis for path correctness of XML queries[END_REF], our system infers sequences of labels (hereafter called chains). Intuitively, for each node that can be selected by a query/update path in a schema instance, the system infers a chain recording i) all labels that are encountered from the root to the node, ii) in the order of traversal. This information is at the basis of a precise static independence analysis. For instance, for q1=//a//c and u1=//b//c over the schema { doc←(a|b) * , a←c, b←c }, the chains doc.a.c and doc.b.c are inferred for the query and the update, respectively. Disjointness of these two chains allows us to statically derive the independence for q1-u1. For the DTD of the XQuery Use Cases [START_REF]XML Query Use Cases[END_REF] before discussed, the chains bib.book.title and bib.book.author, respectively inferred for q2 and u2, diverge after the book symbol; this allows us to conclude independence for q2-u2. These two examples highlight that chain inference provides a more precise independence analysis than that of [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF][START_REF] Ghelli | Commutativity analysis for XML updates[END_REF][START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF].

The main contribution of this work is a precise algorithm to detect independence for a query-update pair q-u knowing that documents are valid wrt a DTD d. It strongly relies on the following developments.

• Chain-based independence for q-u, a static notion, is the foundation of our algorithm: starting from the set C d of all possible chains associated with the DTD d, our inference system extracts subsets of chains Cq and Cu which soundly approximate the navigation through valid documents made by the evaluation of the query q and the update u, respectively. Note that our inference system (Section 3) is cautiously specified for dealing with all XPath axes. Chain-based independence is the result of the absence of overlapping pair of chains in Cq and Cu. Chain-based independence is proved to be sound wrt the semantics notion of query-update independence (Section 4).

• A major step of our work concerns recursive schemas, for which chain-based independence analysis may cripplingly involve to deal with an infinite number of chains. Our technique enabling the restriction of the analysis to finite subsets of Cq and Cu is a key contribution, and the core of our algorithm is the resulting finite analysis (Section 5). It is proved to be equivalent to the infinite analysis2 .

• The algorithm has been carefully implemented, and extensive tests have been performed to validate our claim of precision and efficiency (Section 6). Indeed, using a DAG-based representation of inferred chains allows the finite analysis to run in polynomial space and time. Concerning precision, our results show that our technique outperforms [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF] to a large extent. Test results also show that high savings of time can be ensured by avoiding re-evaluation of queries deemed as independent of an update, even on relatively small documents.

A nice property of our technique (Section 7) is that it can be easily extended in order to cope with Extended DTDs [START_REF] Gelade | Optimizing schema languages for XML: Numerical constraints and interleaving[END_REF], and thus XML Schema. Discussions about related and future work are provided in Sections 8 and 9.

<doc> <c/> <c/> <c/> <c/> </doc>

a document t valid wrt d sd=doc d(doc)=(a | b) * d(a)=c d(b)=c a DTD d σ =        lt ← doc[l1, l2, l3, l4] l1 ← a[l 1 ] l2 ← a[l 2 ] l3 ← b[l 3 ] l4 ← a[l 4 ] l i ← c[], i = 1..4
the store (σ, lt)

PRELIMINARIES

Data model. We represent an instance of the XML data model as a store σ, which is an environment associating each node location (or identifier) l with either an element node a[L] or a text node s.

In a[L], a is the element tag, while L=(l1, . . . , ln) is the ordered list of children locations in σ. A tree is a pair t=(σ, lt), where lt is its root location. dom(σ) denotes the set of locations of σ, while σ@l denotes the subtree of σ rooted at l whose domain is limited to locations connected to l. See Figure 1 for a small document together with its store.

DTDs.

A DTD is a 3-tuple (Σ, s d , d) where: Σ is a finite alphabet for element tags, denoted by a, b, c; s d ∈Σ is the start symbol; d is a function from Σ to regular expressions over Σ∪{S}, where S denotes the string type. For simplicity, next we often use only the d component to specify a DTD.

A tree t=(σ, lt) is valid wrt d, denoted t∈d, iff there exists a mapping ν : dom(t) → Σ∪{S} such that: ν(lt)=s d ; ν(l)=S implies that σ(l) is a text node; ν(l)=a implies that σ(l)=a[L] and the word ν(L) is generated by the regular expression d(a). Given two chains c1 and c2, the concatenation of c1 and c2 is denoted c1.c2; we write c1 c2 to indicate that c1 is a prefix of c2, that is c2=c1.c for some chain c .

Observe that chains in C d are of finite length and may start with any DTD symbol. The set C d is infinite only if d is a verticalrecursive schema. DEFINITION 2.2 (NODE TYPE AND CHAIN). Given σ and l∈dom(σ), we define typ(l)=a if σ(l)=a[L], otherwise typ(l)=S. The chain associated to the node l is defined by c σ l =typ(l) if l has no parent, otherwise c σ l =c σ parent(l) .typ(l).

Consider the DTD and store of Figure 1 Queries, Updates and Independence.

We assume that the reader is familiar with the XQuery and XQuery Update Facility languages. In this paper we consider the two large fragments considered in related approaches [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF][START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF], respectively defined by the following grammars.

q :: = () | q,q | q | s | x/step | for x in q return q | let x := q return q | if q then q else q step :: = axis :: φ φ :: =a | text() | node()

axis :: = self | child | descendant | descendant-or-self | parent | ancestor | ancestor-or-self | preceding-sibling | following-sibling
The empty-sequence and sequence queries are denoted by () and q, q respectively. The query s denotes a constant string value. The symbol φ is used for XPath node tests; a stands for a tag symbol. XPath expressions x/step 1 / . . . /step n , although used in examples, are not directly supported by the grammar; they can be encoded in the standard way, by means of iteration and the allowed single step expression; axes that are not included can be easily encoded too. 3 The rest of the grammar is self explicative.

In examples, /φ and //φ are respectively used as shortcuts for /child::φ and /descendant-or-self::node()/child::φ.

Also, to simplify the formal treatment, we assume that element construction q is not used in the left-hand side expression of a for/let-expression. This restriction is met by a very large class of queries used in practice, while queries like let x := q  return x can be rewritten by simple variable substitution.

The subset of XQuery Update Facility we consider is defined as follows. All update operations (namely: insert, delete, rename and replace) are included.

u

:: = () | u,u | for x in q return u | let x := q return u | if q then u1 else u2 | delete q0 | rename q0 as a | insert q pos q0 | replace q0 with q pos :: = before | after | into (as first | as last)?

Like for queries, updates can be composed sequentially or by means of let/for statements, where only the return part can contain update operations. In other update expressions, q0 is the target expression producing the (target) node in the input document, that is where the update has to be done. In insert and replace updates, q is the source expression producing elements for the insertion or replacement. Deletion delete q0 and renaming rename q0 as a are self-explicative. According to the W3C semantics [START_REF] Robie | XQuery update facility 1.0[END_REF] the target expression q0 is required to output a single node otherwise a run time error occurs.

Query and update semantics are specified in [START_REF] Draper | XQuery 1.0 and XPath 2.0 Formal Semantics[END_REF][START_REF] Robie | XQuery update facility 1.0[END_REF], while a succinct and elegant formalization can be found [START_REF] Benedikt | Semantics, types and effects for XML updates[END_REF], from which we borrow some notions that are needed for our own presentation. Query semantics is denoted by σ, γ |= q ⇒ σq, Lq meaning that the execution of the query q over σ outputs a sequence of locations Lq, roots of the answer trees for q, and a new store σq, 3 e.g., /following::a becomes /ancestor-or-self::node()/ following-sibling::node()/descendant-or-self::a. including σ plus new elements built by q; the environment γ binds each free variable of q to a sequence of locations in σ.

According to the W3C specification, update evaluation is split into three phases: i) creation of an update pending list (UPL) of simple update commands, ii) execution of sanity check on this list, and iii) application of the UPL on the input store so as to obtain the updated data. Update commands ι in a UPL w are of the form:

ι :: = ins(L, pos, l) | del(l) | repl(l, L) | ren(l, a)
where l is the target location and L the sequence of roots of source elements to be inserted. The creation of the UPL (phase i) is denoted by:

σ, γ |= u ⇒ σw, w
As usual, γ binds u free variables to locations in σ and the store σw contains newly created locations potentially used in the UPL w. Applying the UPL w to the input store σ (phase iii) produces the updated store. This is denoted by: σw w ; σu The composition of phases i) and iii) is denoted by: σ, γ |= u : σu Above, dom(σ)⊆dom(σw)⊆dom(σu) holds. For a tree t=(σ, lt), u(t) denotes the tree (σu@lt, lt) and dom(σ) ⊆dom(σu@lt) may not hold anymore 4 . Given two stores σ and σ , two locations l∈σ and l ∈σ are said to be value equivalent, written (σ, l) ∼ =(σ , l ), iff the two trees σ@l and σ @l are isomorphic (they possibly differ only in terms of locations). We write (σ, L) ∼ = (σ , L ) to indicate value equivalence on location sequences L=(l1, . . . , ln) and L =(l 1 , . . . , l n ), with li∈σ and l i ∈σ , and holding iff (σ, li) ∼ = (σ , l i ) for i=1..n.

DEFINITION 2.4 (INDEPENDENCE).

Let σ be a store and γ a variable environment. A query q and an update u are said to be independent wrt (σ, γ) if σ, γ |= q ⇒ σq, Lq σ, γ |= u : σu σu, γ |= q ⇒ σ q , L q implies (σq, Lq) ∼ = (σ q , L q ). Also, q and u are independent, written q |= u, iff they are independent for any pair (σ, γ). Finally, q and u are independent wrt the DTD d, written q |= d u, iff for every tree t=(σ, lt)∈d and γ, they are independent for (σ, γ).

As a natural consequence of the fact that XML data are typed by a schema, we assume that our independence analysis is run in a context where all data remain consistent wrt the schema after each update. In case an update entails schema evolution, then a larger task of schema maintenance has to be carried on. This task may imply existing views (queries) to be reformulated in order to be correct wrt the new schema, and thus it is likely to exclude any other kind of schema-based analysis until its completion.

CHAIN INFERENCE

In this section, we define deduction rules to statically infer chains for query and update expressions. Our system produces chains of different kinds. The classification resembles that of Marian and Simeon in [START_REF] Marian | Projecting XML documents[END_REF] for query path extraction, and is needed due to the fact that different kinds of chains play different roles in the independence analysis.

A query chain belongs to one of the following three disjoint classes:

• Return chains type input document nodes (return nodes) that are roots of elements returned by the query. All descendants of a return node are in the query result, thus a return chain c implicitly embodies these descendants. Now, if a change of an update u targets a return node or some of its ancestors or descendants, query-update independence is not guaranteed.

• Used chains type nodes (used nodes) belonging to the input document and participating to the query evaluation, without necessarily being part of the result itself. Clearly, if a change of an update u targets a used node or some of its ancestors, then query-update independence is not guaranteed.

• Element chains type newly constructed elements; an element chain is of the form a.c , where a is the tag of the constructed a element. Extracting these chains is important for the precision of the independence analysis (see example below).

For updates, we have one class of chains:

• The purpose of an Update chain, denoted by c:c , is twofold: c types nodes l whose content may be changed by the update and c types descendants of l (either introduced or removed by the update) involved in the changes. For example, given c:c , independence is not guaranteed if a query returns an element whose root is typed by c.c , with c a prefix of c .

Let us now illustrate why element chains are necessary for a precise independence analysis. Consider the following update over the well-known XQuery Use Cases DTD [START_REF]XML Query Use Cases[END_REF]:

for x in //book return insert <author>q </author> into x
Here the source expression is an element query, for which we infer element chains of the form author.c , with c a chain inferred for q . The update chain bib.book:author.c is obtained by concatenation of the chain bib.book associated with the target expression x, and the chain author.c . This allows one to conclude independence wrt the query //title, whose unique return chain is bib.book.title (forasmuch as title element is never a descendant of an author element): the update chain is not a prefix of the query chain and vice-versa. Now, let us do the analysis without considering element chains: for the source expression <author>q </author>, the best that can be done is to infer the chain bib.book:, telling that something happens beneath book elements. As a consequence, we would not deduce the independence.

In the presence of nested element construction, the same remark holds. In the previous example, if q is <f irst>U mberto</f irst>, <second>Eco</second> then by composing element chains during the inference, we end up with the following two update chains bib.book:author.f irst.S and bib.book:author.second.S. Indeed, this is necessary to exclude independence wrt the query //author/email (assuming the DTD allows for email elements into author elements).

Chain Inference for XPath Steps

The definition of our chain inference system makes the assumption that the inference is made starting from an input set of chains C. This set can be either C d (infinite analysis) or a finite subset of C d (finite analysis). We would like to stress that assuming a precomputed chain set is only made to ease the formal presentation. Any reasonable implementation can avoid this, by inferring chains on the fly (see Section 6).

The first ingredient for query/update chain inference is chain inference for a single XPath step. We first define chain inference for axes, and then for node tests.

Axis chain inference aims at inferring all chains that can be generated by axis navigation, in a d instance, starting from a node typed by a chain c∈C. Chain inference rules strictly mimic XPath semantics of axes, and are defined below (notice that c can be empty):

A C (c, self) def = { c } A C (c, child) def = { c.α | c.α ∈ C } A C (c, descendant) def = { c.c | c.c ∈ C, c = } A C (c, descendant-or-self) def = { c.c | c.c ∈ C} A C (c, parent) def = { c | c = c .α } A C (c, ancestor) def = { c | c = c .c , c = } A C (c, ancestor-or-self) def = { c | c = c .c }
In the following rules, with a little abuse of notation, given a chain c on d, we use d(c) to indicate either the regular expression d(a), if c = c .a, or the empty regular expression , if c = c .S. Chain inference for preceding/following-sibling axes is defined as follows.

A C (c, following-sibling) def = {c1.β∈C | c=c1.α, α< d(c 1 ) β} A C (c, preceding-sibling) def = {c1.α∈C | c=c1.β, α< d(c 1 ) β}
The relation <r is such that for all α, β∈Σ ∪ {S}, α <r β holds if there exists a word u belonging to the language generated by r in which an α occurs before a β. This relation can be easily defined by structural induction on r (see [START_REF] Bidoit | Detecting XML Query-Update Independence[END_REF]). For instance, we have Rules for node-test chain inference are straightforward:

T C ( c, node() ) def = { c } T C ( c.α, a ) def = { c.α | α = a } T C ( c.α, text() ) def = { c.α | α = S } LEMMA 3.

(SOUNDNESS OF STEP CHAINS).

Let t∈d be a tree and lx∈dom(t). If σ, (x := lx) |= x/axis::φ ⇒ σ, L then 5 for each l ∈ L we have:

c σ l ∈ T C ( A C (c σ lx , axis), φ ).
The proof of soundness is reported in [START_REF] Bidoit | Detecting XML Query-Update Independence[END_REF].

Step chain inference is also minimal for any d, see [START_REF] Bidoit | Detecting XML Query-Update Independence[END_REF] for further details.

Γ C qi : (ri; vi; ei) i=0..2 Γ C if q0 then q1 else q2 : (r1 ∪ r2; i=0..2 vi ∪ r0; e1 ∪ e2) (IF) Γ C () : (∅; ∅; ∅) (EMPTY) Γ C q1 : (r1; v1; e1) Γ[x → c] C q2 : (rc; vc; ec) for any c∈r1 Γ C for x in q1 return q2 : ( c∈r 1 rc; v1 ∪ c∈r 1 rc∪ec = ∅ (vc ∪{c}); c∈r 1 ec) (FOR) Γ C s : (∅; ∅; {S}) (TEXT) Γ C q1 : (r1; v1; e1) Γ[x → r1] C q2 : (r2; v2; e2) Γ C let x := q1 return q2 : (r2; r1 ∪ v1 ∪ v2; e2) (LET) Γ C qi : (ri; vi; ei) i=1..2 Γ C q1, q2 : (r1 ∪ r2; v1 ∪ v2; e1 ∪ e2) (CONC) axis ∈ {self, child, descendant-or-self} rc = TC( AC(c, axis), φ ) for any c∈Γ(x) Γ C x/axis :: φ : ( c∈Γ(x) rc ; c∈Γ(x) rc = ∅ {c}; ∅) (STEPUH) axis ∈ {self, child, descendant-or-self} rc = TC( AC(c, axis), φ ) for any c∈Γ(x) Γ C x/axis::φ : ( c∈Γ(x) rc ; ∅; ∅) (STEPF) Γ C q : (r; v; e) e0 = { a.α.c | c.α∈r, c.α.c ∈r } ∪ { a.c | c∈e } ∪ { a | r ∪ e=∅ } Γ C q : (∅; r ∪ v; e0) (ELT)
Table 1: Chain Inference Rules for Queries

In the rules, τ denotes all descendant chains of chains in the set τ wrt C:

τ def = { c.c | c∈τ , c.c ∈C }
All the rules mimic query semantics [START_REF] Draper | XQuery 1.0 and XPath 2.0 Formal Semantics[END_REF][START_REF] Benedikt | Semantics, types and effects for XML updates[END_REF]. We only comment on the main ones. Rules (FOR) and (LET) are very similar, thus we only comment on the (FOR) rule. It performs an iteration on the set of return chains inferred for q1. Return chains for q1 are then converted into used chains. This is needed because chain inference is a bottom-up process: inside q1 a path expression is seen as a query producing a result (and as such it locally produces return chains), while it only selects nodes to be used in the outer iteration for x in q1 return q2.

In the (FOR) rule, irrelevant chains are filtered out. To illustrate, consider the query for x in //node() return if x/b then x/a

The chain inference, thanks to chain filtering, only produces used chains that lead to either an a or a b node. Otherwise, the set of all possible chains generated by the subquery //node() would be inferred as used chains, for the whole query; as a dramatic consequence, the query would be considered as dependent wrt almost every update.

The rule (STEPF) produces return chains, those pointing to nodes returned by the forward XPath step. The rule (STEPUH) is similar, and deals with upward and horizontal axes. It also produces used chains, by filtering only those bound to the step variable and leading to new result chains according to the step navigation. This is needed since return chains produced by an horizontal/upward step may not contain as a prefix the used chain in Γ(x) from which they have been generated. E.g., for the DTD d = {a ← (b+, c * )}, and the query /a/b/following-sibling::c, we infer a.b as a used chain, and a.c as a return chain.

Element queries q are dealt with by rule (ELT). This rule infers element chains of the form a.c, where c is obtained from either an element or return chain of q. The rule also infers used chains by collecting: i) used chains of q, and ii) used chains obtained from return chains of q. To this end r is used to extend returned chains of the inner query. This return-to-used chain conversion is needed to correctly handle nested element construction. For instance, consider the following query q = <r1>q </r1>, where q = ( x/a , <r2>x/b</r2> ) Element chains for q are inferred in terms of chains for q . So, element chains for q are r1.a and r1.r2.b, assuming that for q the return chains are c.a (for x/a) and r2.b (for <r2>x/b</r2>). In order to avoid ending up with a wrong element chain a.b for q, the return chain c.b for x/b does not have to be considered as a return chain for q as well. This is handled by the return-toused conversion of the return chain c.b when inferring chains for <r2>x/b</r2> (and hence for q ). It is worth stressing that if we just convert return chains to used ones without the extension r, then we lose their semantic property of representing entire subtrees of data. Notice that this extension is needed for the purpose of the formal presentation although any efficient implementation can avoid performing these extensions by using intensional representations.

The rule (TEXT) deals with expressions building new text nodes. The rule infers S as an element chain 6 .

Chain Inference for Updates

Γ C q : (r; v; e) Γ C q0 : (r0; v0; e0) pos∈{into, first, last}

U = { c:c | c∈r0, c ∈e } ∪ { c:α.c | c∈r0, c .α∈r, c .α.c ∈C } Γ C insert q pos q0 : U (INSERT-1)
Γ C q : (r; v; e) Γ C q0 : (r0; v0; e0) pos∈{after, before}

U = { c:c | c.α∈r0, c ∈e } ∪ { c:β.c | c.α∈r0, c .β∈r, c. β.c ∈C } Γ C insert q pos q0 : U (INSERT-2) Γ C q0 : (r0; v0; e0) U = { c:α | c.α∈r0 } Γ C delete q0 : U (DELETE) Γ C q0 : (r0; v0; e0) U = { c:α | c.α∈r0 } ∪ { c:b | c.α∈r0 } Γ C rename q0 as b : U (RENAME) Γ C q : (r; v; e) Γ C q0 : (r0; v0; e0) U = { c:α | c.α∈r0 } ∪ { c:β.c | c.α∈r0, c .β∈r, c .β.c ∈C } ∪ { c:c | c∈r0, c ∈e } Γ C replace q0 with q : U (REPLACE)

Soundness of Chain Inference

From now on, we consider given a DTD d, and some valid document t=(σ, lt)∈d. For a query q, we assume: σ, γ |= q ⇒ σq, Lq and Γ C d q : (r; v; e)

For an update u, we assume: σ, γ |= u ⇒ σw, w σw w ; σu and Γ C d u : U.

Recall that u(t) denotes the tree (σu@lt, lt). Also, for the sake of simplicity, queries and updates are assumed to be quasi-closed: they contain only one free variable x initially bound to the root of the input XML tree (see [START_REF] Bidoit | Detecting XML Query-Update Independence[END_REF] for the general case). It means that γ={x → lt} for query and update evaluation, and Γ={x → ds } for static chain inference.

Soundness of query chain inference. Proving soundness of query chain rules consists of proving that, for any schema instance, any node used or built by the query q is captured (typed) by the chains inferred for q. The proof relies on the notion of XML projection [START_REF] Marian | Projecting XML documents[END_REF][START_REF] Benzaken | Type-based XML projection[END_REF]. A tree t is a projection of t, denoted t t, if t is obtained from t by discarding some subtrees. A projection of a tree t can be obtained from a set L⊆dom(σ), where L is non-empty and upward closed with respect to the σ parent-child relationship 7 . For a sequence of locations L, we define L |L as the subsequence of L containing only L identifiers, and preserving L ordering. Then a projection of t wrt a set L is defined as t |L =(σ |L , lt) where

σ |L def = { l ← a[L |L ] | l∈L, (l ← a[L])∈σ } ∪ { l ← s | l∈L, (l←s)∈σ }
We say that t |L is a q-projection of t if, assuming that σ |L , γ |= q ⇒ σ , L we can conclude (σq, Lq) ∼ = (σ , L ). Given a set of

7 ∀l (l∈L ∧ (l ←a[L])∈σ ∧ l∈L) ⇒ l ∈L.
chains τ , the set L t τ of locations in t=(σ, lt) typed by chains in τ is defined as:

L t τ def = { l | l∈dom(σ), c σ l .c ∈ τ } Finally, t |L is a minimal q-projection
of t if none of the strict projections of t |L is a q-projection. Note that, t is a q-projection of t provided that t |L t , for t |L a minimal q-projection. A minimal projection is not unique, due to the query language considered.

The following theorem formally states that chains inferred for a query q cover the structure of data relevant for the query, and newly constructed elements. THEOREM 3.2. (SOUNDNESS OF QUERY CHAINS) The first item of Theorem 3.2 states that chain inference is sound for used and return chains: a projection of any valid input tree made in terms of used and return chains includes every minimal q-projection, hence preserves query semantics (the projection contains all the query needs for its evaluation). The second item is dedicated to element chain inference which is one of the key feature of our query-update analysis as already illustrated. Intuitively, this statement says that if element chains are used to project newly constructed elements (notice that l ∈Lq\dom(σ)) no node is pruned out, so element chains cover all possible chains in new elements of the query result.

1. If t is a minimal q-projection of t,

Soundness of update chain inference. Proving update chain

soundness consists in establishing a link between i) nodes in the stores t and u(t) that are involved in the changes (deletion, insertion, renaming and replacements) made by u and ii) nodes in these trees which are captured (typed) by the chains statically inferred for u.

DEFINITION 3.3 (INVOLVED LOCATION).

We say that the update u involves the location l∈dom(σw) if l is either the target location of an elementary delete, rename or replace command in w, or a critical location or a descendant of a critical location, where a critical location is a location in the source list L of a command ins(L, , ) or repl( , L) in w.

Note that an involved location may belong to the initial tree t but not to the updated tree u(t) and conversely. It may also, of course, belong to both trees. The theorem below states that all locations involved by the update u are typed by chains inferred from u. THEOREM 3.4 (SOUNDNESS OF UPDATE CHAINS). If l is a location in t, i.e. l∈dom(σ) (respectively a location in u(t), i.e. l∈dom(σu@lt)) and the update u involves l then there exists c:c ∈U such that c σ l =c:c (respectively c σu l =c:c ) where c = . In the above statement, in case a location l belongs both to t and u(t), it may be that the chain typing l in t is different from the chain typing l in u(t) (e.g., due to renaming).

Although we made the assumption that the update expression is preserving the schema, it is worth noticing that Theorem 3.4 holds also for updates violating schema constraints (u(t) / ∈d), since chains corresponding to deleted or inserted nodes are always traced by the system regardless of correctness wrt the schema.

INFINITE ANALYSIS

The notion of query-update independence q |= d u (Definition 2.4) is based on the semantics of q and u, and involves all possible d instances. The static counterpart of this notion is now proposed and is of course based on query and update chain inference. As chain inference depends on a set C of chains, we first introduce a general static notion of C-independence.

Given two sets of chains τ1 and τ2, the set of conflicting pairs of chains for τ1 and τ2 is defined by:

confl(τ1, τ2) def = { (c1, c2) | c1∈τ1, c2∈τ2, c1 c2 } DEFINITION 4.1 (C-INDEPENDENCE).
A query q and an update u are C-independent, denoted by q ⊥ C u, if provided that Γ C q : (r; v; e) and Γ C u : U, we have:

confl(r, U) = confl(U, r) = confl(U, v) = ∅.
The main result of this section states that, when C is taken as the set C d of chains generated for the DTD d, C-independence implies q |= d u independence. q ⊥ C d u implies q |= d u

In order to prove Theorem 4.2, the following property is used; it is a consequence of soundness of chain inference (Theorems 3.2 and 3.4). Next, I t U denotes the set of nodes in a tree t typed by update chains in U:

I t U def = { l∈dom(t) | c σ l = c:c ∈U , c = } PROPOSITION 4.3. If q ⊥ C d u,
then we have:

I t U ∩ L t r∪v = I u(t) U ∩ L u(t) r∪v = ∅
This proposition states that C d -independence implies that nodes typed by query chains are disjoint from nodes typed by update chains. The proof is reported in [START_REF] Bidoit | Detecting XML Query-Update Independence[END_REF]. As already stated, updates are assumed to preserve the schema. The above theorem needs this assumption in order to correctly use query chains in the independence analysis. Actually, if deletions violate the schema (a mandatory node is deleted), the ⊥ C d is still sound. The problem comes from insertions creating new chains (not belonging to C d ) because they are not considered during chain inference for queries. As a consequence, the analysis made to check ⊥ C d could miss conflicting chains. Extending our technique so as to capture schema evolution is left as future work.

FINITE ANALYSIS

The notion of C d -independence (Definition 4.1) cannot be directly used to define a terminating decision algorithm, because for DTDs with vertical recursion the sets of inferred chains can be infinite. In this section we show how to finitely approximate sets of inferred chains so that C d -independence can be detected in finite time.

One feature of chains generated by a recursive DTD d is that some of them contain multiple occurrences of (recursively defined) tags. So one way to characterize a finite set of d-chains is to restrict to chains having at most k occurrences of each tag. Hereafter, these chains are called k-chains, and for any set of chains τ , its subset of k-chains is denoted by τ k . Thus, C k d denotes the set of k-chains generated by d.

As illustrated next, a multiplicity value k can be inferred from the query q and update u, so that independence according to inferred chains in C d is equivalent to independence according to inferred chains in C k d . The value k is derived by a two-steps static analysis. Given an expression exp, being either a query q or an update u, the first step associates a value kexp to exp such that the set of kexp-chains inferred for exp is representative of all possible inferred chains for exp. Intuitively, the representative set of inferred chains for an expression synthesizes all possible inferred chains: any possible inferred chain can be mapped to a chain in the representative set by some folding transformations, according to recursive definitions in the DTD. The second step infers a value k from the values kq and ku, such that the search of conflicting chains decisive for statically detecting q-u independence can be safely done in the finite set of inferred k-chains.

Inferring the values kq and ku mainly depends on navigational properties of the XPath expressions occurring in the query and update. Thus, we start the discussion by focusing on XPath expressions, and then consider FLWR expressions.

Dealing with child, self and parent. In this case, a good choice for kp is the maximal tag frequency in the path p. Consider the following recursive DTD d1:

r ← a b, c, e ← f a ← (b, c, e) * f ← a, g
For the path p=/r/a/b/f /a the maximal tag frequency is 2, and indeed 2-chains include the representative chain r.a.b.f.a (the only chain inferred for this path); the same holds for the navigational path /r/a/b/f /a/parent::f (note here that the 2-chain r.a.b.f.a is a used chain). Similarly, for the path /r/a/b/f / * we choose kp=2, since the wildcard * stands for any label.

Dealing with descendant and ancestor. When a path p makes use of the descendant axis, the length of inferred chains are totally unrelated to the length of p (e.g., consider /descendant::b over d1). This is what led us to reason in terms of tag frequency rather than path length. Furthermore, such a path can lead us to infer an infinite number of chains over a recursive DTD. To generate a finite set of representative chains, the value kp is determined by taking into account the number of descendant axes occurrences in p.

To illustrate, we still consider the schema d1, and observe that the type a is defined in terms of b, c and e, and vice versa. In a valid document instance, a b node can be a descendant of a c node, and vice versa, along the same chain of the tree. In addition, a chain connecting b and c nodes always contains an intermediate a label, which also occurs before the first occurrence of a b, c or e label. As a consequence, for the following path p /descendant::b/descendant::c/descendant::e over the DTD d1, the shortest chain that is inferred for the path p is r.a.b.f.a.c.f.a.e, a 3-chain. Simple tag frequency, like for the previous cases, would lead to kp=1. This is not satisfactory because no chain is inferred for p starting from 1-chains. To reflect the fact that each recursive axis may permit any tag to repeat once in inferred chains, the correct maximal tag frequency we have to consider for the path p is 3; in fact, 3-chains do allow to infer a non-empty set of representative chains. Of course, an XPath expression may combine both recursive and non-recursive axis. In this case, for a path p we obtain kp as the sum of two components computed independently: the maximal tag frequency for non-recursive steps, and the number of recursive steps in p. As an example, for p=/descendant::b/a/b, we have kp=2 since the maximal tag frequency for the descendant-free part /a/b is 1, and there is 1 descendant step /descendant::b.

Recursive backward axes are handled similarly. Here we have to pay attention to the fact that chains navigated by an ancestor step are prefixes of some chains generated by previous steps. Consider p=/descendant::b/ancestor::c. Here kp has to be such that the used chain r.a.c.f.a.b can be generated. Thus, we enforce ancestor steps to increment the tag frequency by 1. This is reminiscent of what we have seen before in the case of descendant; the way p is processed can be compared to the way the navigational path /descendant::c/descendant::b would be processed, as chains containing c ancestors of b need to be generated for p.

Concerning paths p employing either descendant-or-self or ancestor-or-self, kp is computed as for the self-less axes.

Dealing with sibling axes. Dealing with FLWR expressions. Based on concepts previously illustrated, we provide now formal definitions to deal with the general case of FLWR expressions.

As seen before, the computation of kexp is decomposed into two tasks. The first one determines via the function F(a, exp) the frequency of each tag a∈Σ on the whole expression, in order to derive the maximal frequency. The second task computes via the function R(exp) the maximal number of consecutive recursive steps in the whole expression. The value kexp is the sum of these two values. Formally:

kexp def = max{ F (a, exp) | a∈Σ } + R(exp)
The functions F(a, exp) and R(exp) are defined by structural induction in Table 3. When exp is a for/let expression, the value kexp is specified by summing the sub-expression values. This is motivated by the fact that, for instance, for-expressions are usually used to encode nested iterations performed by XPath paths, like in the query for x in /a for y in x/b return y. This leads in some cases to an overestimation of the value kexp that would be actually sufficient for a finite analysis. For instance, for the query q for x in /a/a return for y in /a/b return x,y we have F(a, q )=3, while the value 2 would be sufficient. More precision can be obtained by tracing variable bindings in the definition of F(, ). The same argument holds for R(). However, this would make the formalization cumbersome without being a decisive factor for the analysis. Thus, our choice has been guided by simplicity and conciseness of F(, ) and R() definitions. The rule for element construction deserves some comment. Note that tags of constructed elements are taken into account. Indeed, these elements can be inserted by an update as children of existing elements, thus generating new chains that can be used by a query. Consider the recursive schema {a ←b, b ←b?, c?} and the following update u: for x in /a/b return insert <c/> into x

As already outlined, precision of the independence analysis relies (among other things) on the chains generated for element construction. The rules in Table 3 lead to ku=3, and thus the chain a.b:b.b.c is inferred for the finite analysis. Note that tag frequency for rename expression is determined in a similar way: after renaming, the tag frequency may increase, and chains, for the finite analysis, have to capture this change. Other rules are self-explicative.

Finite independence analysis.

We see now how to use the values kq and ku in order to determine a k value such that C dindependence can be detected by restricting to k-chains.

Consider q=/descendant::b and u=delete /descendant::c over the previous DTD d1. They are dependent and kq=1, ku=1. We could argue that a sound choice is k=max(kq, ku), which allows the finite analysis to infer the query chain r.a.b and the update chain r.a:c. Unfortunately, these chains do not conflict, and rule out dependence. The problem here comes from the fact that the update may change a descendant of a query returned node, and that k=max(kq, ku) does not permit to capture this in the finite analysis. To avoid this problem, it is necessary that representative chains that are inferred for the update cover query returned nodes. To this end, while inferring chains for the update u, structural properties of the query q have also to be taken into account. This is obtained by setting k to kq + ku.

In the remaining part of this section we focus on one of our main results, soundness of the finite analysis. Let d be a DTD, q a query and u an update. Let k=kq + ku as defined above. Then:

q ⊥ C k d u implies q |= d u
We focus on soundness because completeness (q

⊥ C d u implies q ⊥ C k d u) is straightforward, as C k d ⊆C d .
We next develop the main steps of the proof of Theorem 5.1. We reason in terms of dependence, rather than independence. We prove that C d -dependence implies C k d -dependence (these notions The proof is composed of three steps. First, we show that there exists a folding from query chains to k-query-chains, for any query q (Lemma 5.2). Then, we show that there exists a folding from query chains to k-query-chains also preserving the prefix relation , for any pair of queries (q, q ) (Lemma 5.3). Finally, we show that such a folding exists for chains inferred for any query-update pair (q, u) (Theorem 5.1). Proofs are reported in [START_REF] Bidoit | Detecting XML Query-Update Independence[END_REF]. Given a DTD d, we define a folding relation

→ d ⊆ C d ×C d as → d def = { (c1, c2) | c1=c.a.c .a.c ∧ c2=c.a.c }
Notice that, above, the symbol a is a recursive type of the schema. We dub → * d the reflexive and transitive closure of → d .

LEMMA 5.2 (FOLDING). For each chain c inferred from a query q there exists a chain c inferred for q such that c → * d c and c is a kq-chain.

When q and u are C d -dependent, at least one of confl(U, v), confl(r, U), confl(U, r) is nonempty (see Definition 4.1). This implies that there exists a conflicting pair of inferred chains, witness of the C d -dependence of q and u. As updates are defined in terms of queries, the next lemma which focusses on "conflicting" query chains is needed to conclude the proof of Theorem 5.1.

LEMMA 5.3 (FOLDING AND CONFLICT PRESERVATION).

For each pair of chains (c1, c2) inferred for queries q1, q2, and such that c1 c2, there exists (c 1 , c 2 ) inferred for q1, q2, such that c 1 c 2 and ci → * d c i with c i a (kq 1 +kq 2 )-chain (i=1, 2).

IMPLEMENTATION AND EXPERIMENTS

Complexity and Implementation

We implemented in Java our technique for independence analysis. The crucial aspect of the implementation concerns the choice of the data structure for representing inferred chains for the query and the update: the overall performance of the analysis depends on this. This is because the number of distinct chains inferred for a single expression can grow exponentially with the size of the expression to analyze 8 .

In order to avoid this blow-up we represent a set of inferred chains for the query (or update) as a chain-DAG (CDAG) where common prefixes and suffixes shared by different chains are merged according to the following principle. A CDAG is rooted at the schema root type, contains no self-loops and meets the following property: for all type α defined in d, there is at most one CDAGnode of type α at a distance h from the root. In other words, if two chains happen to have the same type-name in position h, they will share a common node in the CDAG at depth h. This implies that during chain inference the width of the CDAG is upper-bounded by the schema size.

The CDAG representation requires a small overhead in order to distinguish two chains inferred for distinct sub-expressions, in the case that these chains share some nodes of the graph. To this end, any edge connecting two CDAG-nodes is labeled with a code identifying the query/update expressions that created it during chain inference. These identifiers are necessary to correctly perform chain inference for backward axes, and independence checking as well. For instance, consider the query q1, q2 = //c/e, /a/d/c/f . Assume q1 and q2 produce {a.b.c.e, a.d.c.e} and {a.d.c.f }. The CDAG representation of these chains is illustrated in Figure 2. First, we clearly see that the merge does not produce non-existing chains as artifacts: by following query codes there is no way to trace a chain a.b.c.f . Second, we can observe that if in q1, q2 we had q2 = /a/d/c/f /ancestor:: * , when inferring chains for the last step of q2, thanks to edge-labeling we avoid to navigate upward parts of the CDAG that have not been generated by q2 (i.e., a b node). Notice that backtracking on unvisited nodes would not affect the correctness of the analysis, but would compromise precision of the independence analysis.

An auxiliary index associates each expression with nodes representing ending points of inferred used and return chains (e and f nodes in Figure 2). Concerning element chains, these are kept in a specific/separate component of the CDAG, in order to distinguish among chains those typing input and those typing constructed data.

The following theorem proves that the chain inference needed for checking C k d -independence has polynomial complexity. THEOREM 6.1. By using CDAGs, finite chain inference for a DTD d, a value k, and an expression exp, can be done in O(k 2 × |d| 4 ) space and O(|exp| × k 2 × |d| 5 ) time.

For space reason, the proof is reported in the full version [START_REF] Bidoit | Detecting XML Query-Update Independence[END_REF]. Here we discuss some cases of practical relevance for which complexity is better than that stated in Theorem 6.1.

When the test condition node() is not used in XPath steps, then time complexity is O(|exp|×k 2 ×|d| 4 ). This is because each inference step would produce O(k × |d|) nodes in the CDAG (i.e., at most one for each CDAG level), while with node() it produces O(k ×|d| 2 ). Furthermore, if we assume that during chain inference each XPath step can have at most m CDAG nodes as input, time complexity goes down to O(m × |exp| × k × |d| 3 ). The value m is likely to be close to 1 for most XPath steps used in practice. This holds in particular for XMark and XPathMark expressions. Another fact observable from such expressions is that they employ a small number of recursive navigations, thus making chain inference doable in O(|d| 3 ) time.

When d is not recursive, the k value stops being determinant for the analysis since no label repeats twice in any d chain. In this case the number of edges of the CDAG is bound by the size of the parent-child relation induced by the schema. Therefore the spatial complexity goes down to O(|d| 4 ), while time complexity is O(|exp|×|d| 2 ). If we also assume the absence of the test filtering node(), time complexity is O(|exp|×|d|). These restrictions are often met in practice, and in particular by expressions used in our testbed (when the recursive component of the XMark schema is not visited at all by the expression).

Once chain inference is done for a query q and an update u, independence (Definition 4.1) is checked over the two inferred CDAGs. This check can be done in O(c × |q| × |u|) time, where c is the size of the smallest CDAG.

Experiments

We performed extensive experiments by using our Java implementation, in order to measure i) efficiency, ii) precision and iii) scalability of our static analysis. We used two different benchmarks: a first one based on XMark /XPathMark, and a second one, dubbed R-benchmark, we specifically designed to measure iii). Concerning the first one, we used a superset of the view maintenance benchmark adopted by Benedikt and Cheney in [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF]. Our benchmark is composed of a set of 36 views vi and a set of 31 updates ui. A view is a query belonging to either the XMark query set q1-q20 [START_REF] Schmidt | XMark: A benchmark for XML data management[END_REF], or to the XPathMark query set A1-A8/B1-B8 [START_REF] Franceschet | XPathMark -An XPath benchmark for XMark generated data[END_REF]; Ai queries only use downward axes, whereas Bi queries use upward and horizontal axes as well. Concerning updates, a first set corresponds to those used in [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF]; these are derived from the XPath-Mark query set A1-A8/B1-B8 and are of the form UAi=delete Ai or UBi=delete Bi. We added a set of 15 updates formed by insert expressions U I1-U I5, rename expressions U N 1-U N 5, and replace expressions U P 1-U P 5. These updates have been defined so as to cover all different types of nodes in XMark documents, and in particular those parts defined by mutually recursive types. It is worth remarking that, even if not all of the delete-updates of the testbed preserve the schema (see UA4, UA5, UA6, UA7, UA8, UB1, UB5, UB6, UB7, UB8 ), the correctness of our technique is still ensured, since no new chain is created by these expressions. As outlined before, our technique is just unaware of new chains built by breaking schema constraints. In light of this, insert, rename and replace update expressions have been chosen in order to preserve document validity. Before performing the tests, XMark and XPath-Mark expressions have been opportunely rewritten into expressions belonging to the XQuery fragment we consider (Section 3), as done in [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF]. The rewriting essentially consists of: putting predicate conditions in disjunctive form, removing attribute use, and extracting paths from functions calls and arithmetic expressions. Clearly, the rewriting is such that a query and an update are independent if the rewritten query and update are. Due to lack of space, queries and updates are reported in the full version [START_REF] Bidoit | Detecting XML Query-Update Independence[END_REF]. We used the above described benchmark to measure precision and efficiency of our technique. Concerning the R-benchmark, it is designed for understanding the impact of recursion in the performances of our analysis. It is formed by schemas and expressions with a massive use of recursion; it is described later on.

We ran all tests on a desktop 4-core Intel Xeon 2.13 GHz machine with 8 GB RAM (the JVM was given 2 GB) running Linux. To avoid perturbations coming from system activity, we ran each experiment ten times, discarded the best and the worst performance, and computed the average of the remaining times.

Runtime on XMark. We measured the time needed by the static analysis to detect independence of each update wrt the whole set of XMark views. The XMark schema is particularly suitable for testing the performances of our technique since the type dependency graph of this schema contains 5 mutually recursive types that form two cliques of size 2 and 3 respectively. We recall that the execution cost depends on the three parameters |d|, |exp| and k. In this testbed we have |d| = 76, and |exp| ≤ 20, while multiplicity values k range from 2 to 6. As observed in Section 6.1, in many cases chain inference is made in O(|exp|×|d|) time.

Time values include the time for CDAGs inference and comparison, for each pair of expressions. Results are collected in Figure 3.a. It shows that the analysis is quite fast: in the worst case the analysis is performed in less than 40 ms for the whole set of views, while the average cost is around 15 ms. According to complexity results of Section 6.1, inference time is influenced by i) the k values needed by a query-update pair and ii) the number of recursive types of the schema effectively unfolded. We see small changes in inference time values according to the k value (e.g., the pair UB1-UB2). Yet, two expressions having the same k value may have different time costs for chain inference, depending on the effective number of recursive types unfolded by the analysis (e.g., the pair UI3-UP3).

Running times obtained from the available OCaml implementation 9 of the analysis presented in [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF] are rather close to ours: the average time for analyzing an update vs all of the views is around 10 ms. It is worth observing, that inference time for [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF] has no sensible oscillations, while in our case inference time depends on k, hence on the query and update expressions. The analysis presented in [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF] has time complexity O((|d| 2 +|q|) 2 +|u|), and thus is expected to be faster than our analysis in the presence of recursive schemas. Nevertheless, as shown shortly, our running times remain low enough to ensure high time savings in views maintenance, even when views are defined on relatively small documents.

Precision on XMark. Independence (Definition 2.4) is undecidable in general [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF], so for the purpose of measuring precision, for each update ui we manually determined independent pairs (ui, vj), details are reported in the full version [START_REF] Bidoit | Detecting XML Query-Update Independence[END_REF] (note that for most pairs in the considered testbed independence is evident, so this process is much less time consuming than one may guess). We then express precision as the percentage of independent pairs that are deemed independent by our static analysis too. To estimate improvements wrt the alternative schema-based technique [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF] we computed the same percentages for that technique by using the public tool 9 .

Results are reported in Figure 3.b. Our chain-based analysis turned out to be precise. Percentages goes from 72% to 100%, while the average precision is 96%. Also, Figure 3.b shows that the analysis proposed in [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF] (that has an average detection of 49%) is always outperformed in terms of precision by our static analysis, and in some cases improvements are huge. This happens in particular for updates UB1, UB5, UB6, UB8 (employing backward and horizontal axes).

For these updates, the over-approximation made by type rules in [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF] entails a high number of false negatives. Our chain based inference instead is so precise to avoid most of these false-negatives. In general, improvements in terms of precision go from 8% (UN4) to 96% (UP1), and the average gain is 46%. In particular, precision of our analysis remains high in the presence of views using upward and horizontal axes (XPathMark queries in the group B). These queries are likely to be among the most expensive ones to re-evaluate after document updating.

Maintenance time on XMark. We measured time savings obtained by avoiding the re-materialization of views which our analysis deem as independent of an update. We used three XQuery engines: Saxon 9.2EE, BaseX 7.0.1 and QizX 4.4. We considered a 1MB XMark document and we scaled to 10MB and 100MB, in order to measure time savings in real scenarios.

Our test results only take into account query answering time. Full details about engine configurations can be found in [START_REF] Bidoit | Detecting XML Query-Update Independence[END_REF]. For As in [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF], for each update ui we measured the time ri needed for refreshing all the 36 views after the update, and the time r type i and r chain i needed to refresh only views that are not deemed as independent by the static analysis of [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF] and by ours, respectively. In Figure 3.c, for each of the three used engines we report the averages of all refreshing times ri, r type i r chain i . As a consequence of time efficiency and precision of our static analysis, even for a relatively small document of 1MB, our independence analysis ensures high time savings for all engines: 82% for Saxon, 75% for BaseX and 85% for QizX. While type based analysis [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF] ensures much lower time savings: 36% for Saxon, 31% for BaseX and 37% for QizX.

These percentages are essentially the same as those obtained for 10MB and 100MB documents, both for our technique and for that of [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF]. This is because in the considered benchmark, queries that are not statically deemed as independent of an update, and hence refreshed, are the most expensive ones to refresh.

Scalability on R-benchmark. The benchmark is composed of a parametric schema dn including n fully-mutually recursive types (each of the n types is defined in terms of all the n types), and a set of XPath expressions em, each one consisting of m consecutive descendant::node() steps. Parameters n and m allow us to range over several configurations and trace the perimeter of applicability of our technique. We considered four schemas dn with n ranging over {1, 3, 5, 10, 20}, and, for each schema, three expressions em with m ranging over {1, 5, 10}. Also, for each expression em we considered k ranging over { |em|, |em|+5, |em|+10 }. Observe that |dn|=n and |em|=m.

The schema d5 is quite complex, it contains 5 mutually recursive types. We can see from Figure 3.d that even with such complex form of recursion, for e5, and for each k ∈ {5, 10, 15}, chain inference is still fast (inference time is around a decimal of a second). For schema d10, featuring an extremely complex form of recursion, inference time is around five seconds for e5, while for e10 the time exceeds ten seconds. The same happens for more complex cases.

These test results show that even for forms of recursions that are unlikely to occur in practice (like the d5-e5 case), chain inference is still fast, while it takes more than one second for extremely complex cases. Figure 3.d also report test results on chain inference of expressions em over the XMark DTD. As it can be seen, if we make a comparison with the d3 case (recall that the largest clique has size 3 in the XMark schema) the number of type definitions (76 in this case) have an impact on inference time, since the query expressions make a massive use of descendant::node() steps. As already discussed, when such step is not used, inference time drastically reduces, as often happens in practice, and in particular for many XMark/XPathMark expressions.

EXTENSIONS

Queries and updates. While we have considered all update operators made available by XQuery Update Facility, the XQuery fragment we have considered (the same as the one considered in the related approaches [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF][START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF]) leaves out several query mechanisms. These can be handled by means of two possible methods. The first one is based on query rewriting. A basic form has been used in [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF], as well as in our experiments (see Section 6). The second method is based on providing new inference rules. The two methods can be used together, and are both easy to develop, except for user defined recursive functions, whose treatment is beyond the scope of this work since they introduce Turing completeness.

For space reason, details about extensions are given in the full version [START_REF] Bidoit | Detecting XML Query-Update Independence[END_REF]. Here, we would like to stress that what makes them easy to develop is our static concept of C-independence, based on the notions of used, return and element nodes (Section 3). These are universal and essential notions, in the sense that, for any kind of query construct that one could think of adding to the framework, analyzing the role of a node with respect to this construct makes the node fall in one of these three categories. Thus, generalizing our framework for a new query construct mainly consists of identifying how used, return and element nodes are determined. This simply requires understanding the standards concerning the query construct semantics, and reusing principles followed in the treatment of the core language in Section 2.

Schemas. Concerning schemas, our technique can be extended in order to deal with Extended DTD [START_REF] Gelade | Optimizing schema languages for XML: Numerical constraints and interleaving[END_REF], capturing XML Schema and RelaxNG types. A tree t is valid wrt (Σ, Σ , s, d, µ) if and only if t =µ(t) and t is valid wrt the DTD (Σ , s, d). Following [START_REF] Gelade | Optimizing schema languages for XML: Numerical constraints and interleaving[END_REF], in an EDTD we can assume Σ ={ai|a∈Σ} and µ(aj)=a for all aj∈Σ . This implies that two types differently indexed produce the same label but possibly different content models. That said, it is sufficient to change Definition 2.1, and the definition of T C ( c, a ) with a∈ . Both changes are straightforward. Notice that precision of the inference as well as complexity results remain unchanged for the EDTD case.

Concerning attributes, extensions are straightforward, and actually implemented in our prototype (a simple rule for dealing with the attribute axis is needed). Concerning ID/IDREF constraints in DTDs, and key/keyref constraints in XSDs (studied in [START_REF] Arenas | On verifying consistency of XML specifications[END_REF]), we assume they are preserved by updates, as we assume that validity is preserved (Section 2). So, in order to ensure precise and sound independence analysis, chain inference does not need to consider these constraints. Our notion of C-independence only concerns the type component of the schema, while these constraints pose restrictions on the values of attributes and elements in a document, and do not impact its structure.

RELATED WORK

Besides [START_REF] Ghelli | Commutativity analysis for XML updates[END_REF] and [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF], already discussed, another work quite close to ours is that recently presented by Benedikt and Cheney in [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF]. An important contribution of this work was a schema-less framework that factors the problem of independence analysis into two subproblems: i) statically inferring a set of destabilizers queries from a query, and ii) checking whether destabilizers overlap with the target nodes of an update. Precision of the technique highly depends on the kind of destabilizers that are inferred from XPath steps. To this regard, the inferred destabilizers for steps of the form x/child::b include x/child:: * (a similar inference is made for other downward axes). As a consequence any update touching a non-b node which is a sibling of a b node selected by x/child::b would not be detected as independent of x/child::b, while it should. In the presence of a schema, our technique detects independence for these cases, thus ensuring a much higher degree of precision. It is worth observing that precision of this destabilizer-based approach could be improved by adopting a different destabilizer inference system, but yet ensuring high precision could be hard since, as shown in [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF], there is non elementary algorithm for constructing a minimal static destabilizer.

Type-based projection techniques [START_REF] Benzaken | Type-based XML projection[END_REF][START_REF] Baazizi | Projection for XML update optimization[END_REF] could be extended to detect query-update independence. However, as type-projectors resemble to types inferred by [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF], the extension would not be as precise as our technique. Also, both techniques [START_REF] Benzaken | Type-based XML projection[END_REF][START_REF] Baazizi | Projection for XML update optimization[END_REF] only consider DTDs, while chain-based analysis works for EDTDs too.

Raghavachari and Shmueli [START_REF] Raghavachari | Conflicting XML updates[END_REF] considered a downward subset of XPath, and found fragments for which independence turns out to be either a polynomial or an NP-hard problem; schema information was not considered.

CONCLUSIONS

We presented a type system able to statically detect XML queryupdate independence. One of the main feature of the type system is the chain inference component, allowing to infer information at the basis of an highly precise analysis. One of the key contributions of the work is a method to restrict the analysis to a finite set chains in the presence of recursive schemas. As shown by examples and experiments our technique ensures high improvements in terms of precision wrt the state-of-the art schema-based technique [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF].

Figure 1 :

 1 Figure 1: Document and store

DEFINITION 2 . 1 (

 21 REACHABILITY AND CHAINS). Let d be a DTD, α ⇒ d β holds iff α, β∈ Σ∪{S} and β occurs in the regular expression d(α). A chain c over d is a sequence of labels α1.α2 . . .αn such that αi ⇒ d α (i+1) for i=1 . . . n-1. The set of chains associated with the DTD d is denoted C d . For the DTD of Figure 1, the set C d includes the chains doc.a, a.c, doc.a.c, doc.b, b.c, and doc.b.c, because we have doc ⇒ d a, a ⇒ d c, doc ⇒ d b and b ⇒ d c.

  , we have: typ(l1)= typ(l2) = typ(l4) = doc.a and typ(l 1 ) = typ(l 2 ) = typ(l 4 ) = doc.a.c. PROPOSITION 2.3. Given a tree t=(σ, lt)∈d, for each location l∈dom(σ), we have c σ l ∈C d .

  < a,(b | c) * = {(a, b), (a, c), (b, c), (c, b), (c, c), (b, b)}.

THEOREM 4 . 2 (

 42 SOUNDNESS OF C d INDEPENDENCE).

  Sibling axes are managed as child and parent axes. Let us consider the recursive schema { a←(b, f * ), b←(b|c) * , f ←(e, g) } and the navigational path /descendant::c/ following-sibling::b. For this path, the used 1-chain a.b.c and the return 2-chain a.b.b are the needed chains. The presence of the /descendant::c step entails k=2.

THEOREM 5 . 1 (

 51 SOUDNESS OF C k d INDEPENDENCE).

Figure 2 :

 2 Figure 2: CDAG for q1, q2

Figure 3 :

 3 Figure 3: Test results

DEFINITION 7 . 1 .

 71 An Extended DTD is specified by a tuple (Σ, Σ , s, d, µ) where (Σ , s, d) is a DTD and µ is a function from Σ ∪ {S} to Σ ∪ {S} such that µ(S)=S.

Table 2 :

 2 Chain Inference Rules for Updates corresponds to inserted data. Rule (INSERT-2) is similar, and deals with insert-before/after updates. Inference for delete expressions is defined by the (DELETE) rule, which simply puts the separator ':' just before the last symbol of a return chain of the target query.

A delete chain c:α captures that a node typed by c has a child labeled by α which may be deleted. Similarly, the (RENAME) rule infers chains c:α where α is the type of the target node before renaming, but it also produces chains c:b typing renamed nodes. The rule for replace expressions (REPLACE) is built on the same principles as (INSERT-1) and (DELETE) rules.

  then t t |L t r∪v 2. If t is the subtree of σq rooted at l ∈Lq\dom(σ) then t t |L t

	e

  max{ F(a, exp i ) } if exp is (exp 1 ,exp 2 ) or (if exp 0 then exp 1 else exp 2 ) exp i ) if exp is (for/let x exp 1 return exp 2 ) or (delete exp 1 ) or (insert/replace exp 1 exp 2 ) } if if exp is (exp 1 ,exp 2 ) or (if exp 0 then exp 1 else exp 2 ) ) if exp is (for/let x exp 1 return exp 2 ) or (delete exp 1 ) or (insert/replace exp 1 exp 2 ) or (rename exp 1 as b)

	F(a, exp)

def = 0 if exp is () or s or exp is x/axis :: φ and axis recursive or φ / ∈{a, node()} 1 if exp is x/axis :: φ and axis not recursive and φ∈{a, node()} i F(a, F(a, exp) if exp is (exp) or (rename exp as b) and b =a 1 + F(a, exp) if exp is (exp) or (rename exp as b) and b=a R(exp) def = 0 if exp is () or s or x/axis :: φ and axis not recursive 1 if exp is x/axis :: φ and axis recursive max{ R(exp i ) i R(exp i

Table 3 :

 3 F(, ) and R() definition.

This technique deals with update-commutativity detection for a language with side effects and can be directly extended to queryupdate independence detection without side effects.

This is reminiscent of the well known Finite Model Property technique used in the context of finite model theory[START_REF] Blackburn | Modal Logic[END_REF].

3.2 Chain Inference for QueriesInference rules for queries are presented in Table1. As usual, a variable environment Γ associates each query free-variable x with a set Γ(x) of chains, typing nodes that can be assigned to the variable during query evaluation.Query rules prove judgements of the form:Γ C q : (r; v; e)meaning that starting from Γ and C, the chain inference produces the sets r, v and e, respectively containing the return, used and element chains for q.5 Notice here that step evaluation does not change σ.

As seen before, update chains are of the form c:c . Essentially, the prefix c types updated nodes, that are nodes whose children are modified by the update, while the suffix c types modified children or new descendants. Update chains are inferred by rules in Table2(only main rules are reported; see[START_REF] Bidoit | Detecting XML Query-Update Independence[END_REF] for the full set of rules). Chain inference for insert-into expressions (position ranges over into, first and last) is specified by the rule (INSERT-1). For any chain c:c inferred, the prefix c is a return chain of the target query q0 (typing the insertion point), while the suffix c is either a return or element chain of the source expression q typing a branch of a node element returned by q itself; this element can either be a new one or a sub-element of the input document; in both cases the suffix chain[START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF] For simplicity, we preferred not to use a 5th class of chains.

This happens for schemas that make heavy use of recursive definitions, but also for non-recursive ones, like for instance d = { ai ← (bi, ci) * bi, ci ← ai+1 , i = 1..n } (for a query q = //an the number of inferred chains is 2 n ).

http://homepages.inf.ed.ac.uk/jcheney/programs

Acknowledgments. We would like to thank George Katsirelos, Asterios Katsifodimos and Carlo Sartiani for helpful discussions and comments on this work. We would also like to thank the VLDB anonymous referees for their useful feedback and suggestions. This work has been partially funded by Agence Nationale de la Recherche, decision ANR-08-DEFIS-004.