Abderrahim Lamara
email: abderrahim.lamara@d2t.fr

Guillaume Colin
email: guillaume.colin@univ-orleans.fr

Patrick Lanusse
email: patrick.lanusse@ims-bordeaux.fr

Yann Chamaillard
email: yann.chamaillard@univ-orleans.fr

Alain Charlet
email: alain.charlet@univ-orleans.fr

Decentralized robust control-system for a non-square MIMO system, the air-path of a turbocharged Diesel engine

Keywords: Diesel engine air path, Robust control, CRONE, Multivariable control, Non-square system

The targeted purpose here is the control of a nonlinear and non-square system with three inputs and two outputs in order to reduce soot and greenhouse gas pollutants. In this paper, a non-square multivariable controller for the air-path system of a turbocharged Diesel engine is proposed. The controller is designed using the CRONE (Commande Robuste d'Ordre Non Entier) Control-System-Design approach to maintain performance and robust stability for a wide set of operating points. In this research, we focused on the multi-input multi-output system identification problem, and test-bench data were processed to find a nominal linear model. The controller was then designed via an open-loop transfer function optimization. Finally, simulation results from a simulation model show the performance of the proposed control-system.

I -INTRODUCTION

With increasing environmental concerns and ever stricter emission standards [START_REF] Michael | L'évolution des émissions des véhicules[END_REF], current Diesel engine control research focuses on simultaneous Soot and Nitrogen Oxides (NOx) reduction, while maintaining reasonable fuel economy and drivability.

Improvements in the air system control can succeed in meeting stricter emission regulations and customer demands. The hardware component of Exhaust Gas Recirculation (EGR), integrated in the air path system, complicates the engine configuration. This advanced hardware component may result in significant nonlinearities and interactions [START_REF] Wang | Quantitative feedback design of air and boost pressure control system for turbocharged diesel engines[END_REF][START_REF] Larsen | Coordinated passivation designs[END_REF], so that advanced control methods are required. Usually EGR, throttle (Th) and turbocharger valves (Wastegate, WG) are used as actuators (inputs) to ensure boost or manifold pressure and air flow (output) as shown on figure 1. In the literature, different approaches have been proposed for this Diesel engine control problem. In [Alberer, D. et al, 2010] a virtual reference design approach was used to evaluate the choice of actuators, before applying the method to the fuel path and air path subsystems. The virtual variables can be seen as local mappings of the target variables onto an input space, and provide a valuable insight into the contribution of the different input quantities [Alberer, D. et al, 2010].

Most recent Diesel engine control research uses a physical model [START_REF] Leroy | Transient Burned Gas Rate Control on VVA equipped Diesel Engines[END_REF]] [Chauvin J. et al, 2008] [Stefanopoulou, A.G. et al] to simulate controller efficiency, before testing the controller performance and robustness on a test bench. In [START_REF] Kocher | Control-Oriented Modeling of Diesel Engine Gas Exchange[END_REF], a reduced order model of the air handling system of a modern diesel engine was developed based on physical equations. This model-based control is intended for the development of the closed-loop control and estimation strategy.

The tuning, however, is often based on ad-hoc trial and error methods. In [Chauvin, J. et al, 2006[START_REF] Larsen | Coordinated passivation designs[END_REF] an open-loop control law was applied as a feedforward, to control both intake manifold pressure and exhaust pressure. An estimator was also proposed to estimate the measurements which are not available, in order to ensure the closed-loop control. A coordinated passivation design in [Kocher, L. et al, 2003] was applied to control a simplified third-order engine model. [START_REF] Murilo | Multivariable Control Strategy Based on a Parameterized NMPC for a Diesel Engine Air Path[END_REF] proposed a multivariable control strategy based on a parameterized nonlinear model predictive control approach. Nonlinear continuous-time generalized predictive control was presented in [START_REF] Dabo | NCGPC with dynamic extension applied to a Turbocharged Diesel Engine[END_REF] [START_REF] Wang | Model-Based Quantitative Feedback Control of EGR Rate and Boost Pressure for Turbocharged Diesel Engines[END_REF]. Most works presented above use not the throttle as a third actuator. As in [START_REF] Colin | Multi-SISO Robust Crone Design for the Air Path Control of a Diesel Engine[END_REF] a Multi-SISO robust CRONE design was proposed to control both EGR and wastegate (WG) valves. Here we extend [START_REF] Colin | Multi-SISO Robust Crone Design for the Air Path Control of a Diesel Engine[END_REF] and the throttle valve (Th) will be taken into account.

The paper is organized as follows. In section II, system description, identification and the physical model are presented. Section III gives, an introduction to the CRONE MIMO approach is proposed. Section IV addresses the open-loop optimization and the design of a decentralized controller. In the last section, results are shown and discussed.

II -SYSTEM DESCRIPTION

The system is a 4 cylinders with 2.0L turbocharger Diesel Engine, and 80.9 KW. The three air path actuators, that is wastegate (WG), EGR valve (EGR) and intake throttle (Th) are pneumatic (use compressed air). The air path system of the turbocharged Diesel engine is described by Fig. 2.1. The fresh air coming from the atmosphere is compressed and warmed up by compressor. The exchanger cools it down which increase the density of flow (

) and decreasing the boost pressure (p boost ). The throttle valve (Th) controls the flow before the intake and EGR system. The mixture of intake flow and exhaust flow decreases the mean combustion temperature and reduces NO x production, but at the same time it decreases engine efficiency. In the end of combustion, a part of the burned gases can be recirculated through the EGR valve and cooled down by the EGR cooler. The exhaust flow can also flow through the turbine, and speed it up. This energy is transmitted by a shaft to the compressor which adjusts the boost pressure. The turbine speed can be tuned by adjusting the wastegate (WG) position. Finally the exhaust gas returns to the atmosphere.

II.1 System-Identification

Complex plant structures often require complex technologies to meet performance requirements. Robust control can be used to achieve high levels of disturbance rejection. The CRONE approach requires to models the frequency response of the system around its different possible operating points. The frequency-domain identification of the linear dynamic model of the air path (which is a non-minimum phase and MIMO system) could be achieved using various excitation signals including random noise, burst random noise, pulse-impact, multisine [START_REF] Jesse | Sequential multisine signals for system identification of large structures[END_REF][START_REF] Thomas | Frequency domain identification of synchronous machines by multisine excitation[END_REF][START_REF] Colin | Multi-SISO Robust Crone Design for the Air Path Control of a Diesel Engine[END_REF], and chirp and pseudo-random binary (PRBS) [START_REF] Wang | Quantitative feedback design of air and boost pressure control system for turbocharged diesel engines[END_REF] signals.

The goal of frequency domain system identification is to obtain a linear time-invariant model that approximates the dynamics of an unknown plant. Generally, the plant may have nonlinear time-varying dynamics. Plant nonlinearities often induce harmonic responses to sinusoidal input signals [START_REF] Jesse | Sequential multisine signals for system identification of large structures[END_REF].

A multisine excitation signal is used here to identify the air path system. The use of this broadband signal allows faster frequency domain identification. The choice of operating points for air path system identification (green cross in Fig. 2.2) is based on the high pollutant area (pink area in Fig. 2.2), where The EGR flow can reduce NOx production.

II.2 Identification process

The identification step requires multisine signal specifications. This signal is a linear combination of sinusoids which is often given by: where N is the number of harmonics in the signal, is a harmonic frequency, is a harmonic amplitude, and the initial phase of each harmonic.

The amplitude is chosen in such way that system remains at the same operating point during identification, and also gives a linear response. Frequencies are selected to provide enough information about system dynamics within a given frequency range. With chirp and PRBS, part of the frequency response is outside the window defined by the signal frequencies specifications.

Those frequencies are chosen such that the timeinvariant nominal model approximates the most important linear dynamics of the real system. The max frequency must be greater than the desired cut-off frequency of the system. To design a controller must be at least ten times larger than the required frequency bandwidth given by the disturbance rejection specifications.

The identification of each element of the transfer matrix consists in exciting only one input, and each element of the matrix is calculated using the Fourier transform (FFT) of the ratio of the cross-correlation between output and input divided by the autocorrelation of the input :

Each input-output transfer is then described: The signal excitation was chosen with a sampling frequency at 1 kHz, a frequency range from 0.1 to 20 Hz and contains 200 frequencies. Fig. 2.4 presents the Bode diagram computed from (2). A triangular window was used to reduce the noise effect. Despite the use of windowing the noise effect is still important. The noise problem will be discussed in section III.

G 11 : from EGR (%)
As multisine frequency domain identification provides a non-parametric model, second order with delay transfer functions are used to obtain a nominal parametric model of the plant:

As shown on Fig. 2.4, the nominal plant (black curve) is defined from the average gains and phases. The nominal transfer function matrix expression is given by: Fig. 2.4: Bode diagram of nominal plant frequency response (solid black curve) and all operating point frequency responses (green curves).

III -MIMO CRONE DESIGN METHODOLOGY

The CRONE control-system design methodology is a frequency-domain approach that has been used since the eighties [START_REF] Oustaloup | Systèmes asservis linéaires d'ordre fractionnaire[END_REF][START_REF] Oustaloup | La commande CRONE[END_REF][START_REF] Oustaloup | The CRONE control of resonant plants: application to a flexible transmission[END_REF][START_REF] Lanusse | De la commande CRONE de première génération à la commande CRONE de troisième generation[END_REF][START_REF] Lanusse | Control Of Time-Delay Systems Using Robust Fractional-Order Control And Robust Smith Predictor Based Control[END_REF] Åström, K.J. 1999].

The objective of the CRONE control system design is to robustify the closed loop dynamic performance through either a robust damping factor, or a robust resonant peak control based on the unity-feedback configuration (Fig. 3.1).

Fig. 3.1: Unity-feedback configuration for CRONE approach.

The aim of the CRONE MIMO design is to find a diagonal open-loop transfer matrix. Each element is defined by a fractional order transfer function. Fractional differentiation is used to define the nominal and optimal open-loop:

For non-square systems [START_REF] Gruel | Decentralized CRONE control of mxn multivariable system with time-delay[END_REF][START_REF] Dabo | Dynamic Feedback Linearization applied to Asymptotic Tracking: generalization about the Turbocharged Diesel Engine outputs choice[END_REF], the optimization of makes it possible to calculate the controller which is given by the expression.

where (s) is the Moore-Penrose pseudo-inverse of nominal plant G 0 (s). Moore and Penrose show that a solution can exist for the equation where and and . Using Graybill's theorem [START_REF] Graybill | Introduction to matrices with applications in statistics[END_REF] the matrix of rank r can be calculated as: Each element of the diagonal open-loop matrix is based on the third generation CRONE single-input single-output (SISO) methodology, the principle of this methodology is to optimize the parameters of a nominal open-loop transfer function that includes a band-limited complex fractional order integration over a frequency range . The complex fractional order, n = a+ib enables a straight line of any direction to be created in the Nichols chart which is called the generalized template (Fig. 3.3).

The SISO nominal open loop transfer function is defined by: -where is a set of band-limited generalized templates: -where with:

for and -where is an integer order proportional integrator -where is the low-pass filter of integer

The gains and are such that is the closed-loop resonant frequency. Order has to be set to manage the accuracy provided by the control-system. Order has to be set to obtain a proper or bi-proper control-system. When useful, and are different from 0 to increase the number of tuning parameters used for the open-loop shaping.

For time-delay, non-minimum phase or unstable SISO systems, the open-loop transfer function must include the nominal time-delay and right half plane zeros and poles of G 0 to make the controller achievable and the closed loop fully stable [START_REF] Lanusse | De la commande CRONE de première génération à la commande CRONE de troisième generation[END_REF][START_REF] Lanusse | Control Of Time-Delay Systems Using Robust Fractional-Order Control And Robust Smith Predictor Based Control[END_REF]. The optimal approach allowed by the generalized template ensures an optimal positioning of the frequency uncertainty domains (Fig. 3.3) which reduce the resonant peak variations (strongly correlated to overshoot variations) of the complementary sensitivity function . The robustness cost function is given by:

 cg M r0 M r max1 (a) (-180°,0dB)  cg M r0 (b) M r max2 M r max2
nominal one) of the complementary sensitivity transfer function matrix and the controller elements are obtained from relations ( 5) and ( 7):

As β jj (s) are fractional order transfer functions, the rational transfer functions K Rij (s) are obtained by identifying the ideal frequency responses K ij (j) by low-order transfer functions:

      s A s B s K ij  R (15)
where B(s) and A(s) are polynomials of specified integer degrees n B and n A . All the frequency-domain systemidentification techniques can be used [START_REF] Oustaloup | The CRONE toolbox for Matlab[END_REF][START_REF] Oustaloup | Frequency synthesis of filter using the functions of Viète's roots[END_REF]. Whatever the complexity of the control problem, it is easy to find satisfactory values of n B and n A generally about 6 without a reduction in performance. For non-square systems, the Block Relative Gain (BRG) array method [START_REF] Kariwala | Block Relative Gain: Properties and Pairing Rules[END_REF][START_REF] Jesse | Sequential multisine signals for system identification of large structures[END_REF] is used to evaluate different block interactions. A system is weakly interacting if BRG is close to the identity matrix. If the singular values of the BRG are very different from unity, the closed-loop system has large interactions. Thus the BRG method is used to allocate inputs to outputs. Then to simplify the use of the proposed MIMO methodology, all the blocks with a weak BRG are assumed equal to zero and a new nominal plant is defined:

IV -DESIGN OF A DECENTRALIZED CRONE CONTROLLER

From ( 5) the controller will be a decentralized controller. This phenomenon can be explained by the existence of numerical noise. Thus, the corrupted phase of G 23 was approximated with a shifted phase which has the same appearence as the nominal plant phase (Fig. 4.3). In this work, the set of specifications was not fully defined, so the optimal specifications are required in order to find the best general template position.

K 11 K 21 K 32 0 0 0 G 13 G 12 G 11 G 21 G 22 G 23 y 1 (s) y 2 (s) y 1ref (s) y 2ref (s ) K(s) G (s) e 1 (t) e 2 (t ) u 1 (t) u 2 (t) u 3 (t)
The greatest values of the diagonal element of T are 1.99 for T 11 and 2.1 for T 22 . From the complementary sensitivity function T 21 , we can note that each 1 mbar could generate a noise of 0.1 g/s at the airflow output. Also from T 12 , each 1 g/s could generate a noise of 0.3 mbar at the boost pressure output. So could be more affected by pressure, than could be affected by . As explained in section III, low order rational transfer functions were used to approximate the desired frequency response of each element of the decentralized controller:

V -SIMULATION RESULTS

In this section, only simulation results are presented. Indeed, the controller was tested before on the linear nominal plant controller performance hence, using the simulation physical (nonlinear) model, the controller is assessed in several operating points in order to check controller performance and robustness.

V-1 Anti wind up problem

In order to include an anti-windup strategy in the controller, each element of ( 17) is written: Using a model of the system saturation and a gain, Fig. 5.1 shows how the integrator part is fed back to manage the actuators saturation problem.

V.2 Simulation

The simulation model is based on physical equations and on look-up tables. It was calibrated with engine test bench results. The controller was tested with this nonlinear model which is able to simulate the motor behavior on 96 operating points (blue points on Fig. 2.2). As the AMEsim model can be integrated in a real-time target, it allows us to run a real time simulation. The other advantage of AMEsim is the co-simulation with Simulink, which means that the AMEsim simulation results can be analyzed using the Matlab workspace. As explained by section II.3 the model has been calibrated with our engine test bench results. In such way it gives the same mean values and a close dynamical behavior of the real engine. A particular attention has been payed for actuator dynamics. The simulation model allows us to assess the controller performance in several operating points (different values of torque and engine speed). Fig. 5.2 and Fig. 5.3 show, respectively, the system response and valves positions. In this test a speed at 3000rpm has been chosen, with torque variation from 50Nm to 100Nm, and from 100Nm to 150Nm.

Fig. 1

 1 Fig. 1.1: Air path system representation.

Fig. 2

 2 Fig. 2.1: Air path scheme of a turbocharged Diesel engine with Exhaust Gas Recirculation (EGR).

Fig. 2

 2 Fig. 2.2: All the operating points used for system identification and model building.

Fig. 2

 2 Fig. 2.3: Time and frequency responses comparison for different excitation signals.

  -zero polynomial of s with timedelay, and .

Fig. 3

 3 Fig. 3.3: (a) any generalized template, (b) optimal template as M r max2 (maximum resonant peak) is closer to M r0 than M r max1 is.

  value of the resonant peak. Its minimization is accomplished while respecting closed loop constraints for all plants and for . with The frequency uncertainty domains are defined from the multiplicative uncertainty of the open-loop frequency response in the Nichols chart. This multiplicative uncertainty is invariant and equal to the plant uncertainty: plant and open-loop transfer function, and where is the multiplicative uncertainty model. For MIMO systems, the resonant peaks taken into account in the cost function to be minimized are those of the diagonal elements of the perturbed values (not only the a b (-180°,0dB)

Fig. 4

 4 Fig. 4.1: Decentralized control of a 3x2 MIMO plant.

  However the elements of the nominal (and diagonal) open loop transfer function matrix are optimized by taking into account the full MIMO transfer function frequency response defined by G (Fig. 2.4). As shown by Fig. 2.4, the computed phase of is very uncertain and would prevent a good optimization of the nominal open loop transfer function. Here an example of identification of a known transfer function using a triangular window is performed. As shown by Fig. 4.2, the phase (blue curve) differs from the true phase from 16 rad/s.

Fig. 4

 4 Fig. 4.2: Identification of a known transfer function (green) using a triangular window.

Fig. 4

 4 Fig. 4.3: Bode diagram of the new template of the frequency response. Taking into account this corrected phase, the equivalent open loop frequency responses (computed from the perturbed frequency response of the diagonal elements of the complementary sensitivity transfer function) are not uncertain in the extreme and optimization of the parameters of nominal  10 (s) and  20 (s) is achievable.

Fig. 4

 4 Fig. 4.4: Optimization of open-loop for air flow control -left) and for boost pressure control -right). Fig. 4.4 presents the nominal optimized open loop frequency responses (red). The multiplicative uncertainty (green) resulting from all the perturbed equivalent openloop frequency responses has been placed outside the low stability area of the Nichols chart.

  Fig. 4.5 and Fig. 4.6 present the closed loop sensitivity functions T(s) and KS(s).

Fig. 4

 4 Fig. 4.5: Complementary sensitivity function T(s).

Fig. 4

 4 Fig. 4.5: Sensitivity function KS(s).

Fig. 5

 5 Fig. 5.1: Anti-windup controller with feedback gain.

Fig. 5

 5 Fig. 5.2: Airflow and boost pressure response in simulation.

Fig. 5

 5 Fig. 5.3: Valve positions in simulation.

Fig. 5.2 presents both Q air and p boost responses (closed loop response). The setpoints (red curves) have been filtered by a low-pass filter with a time constant of 0.5s. Despite of filtering one can note an overshoot of airflow at 23s due to p boost influence (see T sensitivity). Fig. 5.3 shows engine's valves positions, the wastegate variation appears more important comparing with the others valves, which can explains the influence of the p boost on the Q air outputs. The used filter can cause a setpoint tracking problem during driving [Dabo,K et al. 2009]. On Fig. 5.4, co-simulation results on a short part of the European driving cycle are shown in order to check controller tracking performances. Fig. 5.4 shows engine torque and engine speed operating points. Based on this two coordinates, the airflow and boost pressure set-points are generated automatically from a lookup table to set the engine operating point.

Two responses are drawn (Fig. 5.5) in order to compare the CRONE controller performance with and without feedforward, it (Fig. 5.5) presents the airflow and boost pressure reference tracking. In co-simulation, a filter with time constant of 0.2s is used here to filter the sharp variation of the set point.

Respectively the curves in green and blue, where one note in the rising phase, the controller performs better with feedforward. Contrary in the falling phase, the controller without feedforward performs better. As shown on airflow response, at time 64s, the green curve undershoot is less than the blue one. From Fig. 5.4 both EGR and Throttle valves need more effort to be controlled, which can reduce valves life and consume much energy. From the Fig. 5.3 and Fig. 5.4 (crone) at 60s and 70s, one note that the controller, with and without feed-forward, gives different mean values of the throttle position, which agree with our case, number of inputs greater than outputs.

The decentralized non square CRONE approach allows us to control the airpath of a Diesel engine with three pneumatic actuators and two sensors only. Despite the change of the operating point (Fig. 5.4, engine speed and engine torque) the controller tracks the airflow and boost pressure setpoint (Fig. 5.5), which confirms the controller robustness.

VI -CONCLUSIONAND FUTURE WORKS

In this paper, we propose a systematic method to design a non square and robust control, which is applied here to the air path of a turbocharged Diesel engine. The computationally inexpensive control is thus obtained faster than the usual look-up table based control. Indeed, after frequency-domain system identification, a decentralized (3x2) CRONE control-system is designed by optimizing open-loop behaviors, while ensuring a good frequencydomain closed-loop specifications. Control performance of the proposed method has been demonstrated on a nonlinear model in co-simulation. Future works extend this paper to more complex technologies and apply it on our engine test bench. The global objectives to obtain the best compromise NOx/PM already stay our goal in future works, NOx emission will be checked by smoke-meter on the entire driving cycle, in order to evaluate the controller performances. Alberer, D et al. (2010)

VI -REFERENCES


Florent Jacquemard
email: florent.jacquemard@inria.fr

Michael Rusinowitch

Rewrite Closure and CF Hedge Automata ⋆

We introduce an extension of hedge automata called bidimensional context-free hedge automata. The class of unranked ordered tree languages they recognize is shown to be preserved by rewrite closure with inverse-monadic rules. We also extend the parameterized rewriting rules used for modeling the W3C XQuery Update Facility in previous works, by the possibility to insert a new parent node above a given node. We show that the rewrite closure of hedge automata languages with these extended rewriting systems are context-free hedge languages.

Introduction

Hedge Automata (HA) are extensions of tree automata to manipulate unranked ordered trees. They appeared as a natural tool to support document validation since the number of children of a node is not fixed in XML documents and the structural information (type) of an XML document can be specified by an HA.

A central problem in XML document processing is static typechecking. This problem amounts to verifying at compile time that every output XML document which is the result of a specified query or transformation applied to an input document with a valid input type has a valid output type. However for transformation languages such as the one provided by XQuery Update Facility (XQUF), the output type of (iterated) applications of update primitives are not easy to predict. Another important issue for XML data processing is the specification and enforcement of access policies. A large amount of work has been devoted to secure XML querying. But most of the work focuses on read-only rights, and very few have considered update rights for a model based on XQUF operations [START_REF] Fundulaki | Formalizing XML access control for update operations[END_REF][START_REF] Bravo | ACCOn: checking consistency of XML writeaccess control policies[END_REF][START_REF] Jacquemard | Rewrite-based verification of XML updates[END_REF]. These works have considered the sensitive problem of access control policy inconsistency, that is, whether a forbidden operation can be simulated through a sequence of allowed operations. For instance [START_REF] Jacquemard | Rewrite-based verification of XML updates[END_REF] presents a hospital database example where it is forbidden to rename a patient name in a medical file but the same effect can be obtained by deleting this file and inserting a new one. This example illustrates a so-called local inconsistency problem and its detection can be reduced to checking the emptiness of a HA language.

In formal verification of infinite state systems several regular model checking approaches represent sets of configurations by regular languages, transitions by rewrite rules and (approximations of) reachable configurations as rewrite closure of regular languages see e.g. [START_REF] Feuillade | Reachability Analysis over Term Rewriting Systems[END_REF][START_REF] Bouajjani | On computing reachability sets of process rewrite systems[END_REF]. Regular model checking [START_REF] Bouajjani | Regular model checking[END_REF] is extended from tree to hedge rewriting and hedge automata in [START_REF] Touili | Computing transitive closures of hedge transformations[END_REF], which gives a procedure to compute reachability sets approximations. Here we compute exact reachability sets when the configuration sets are represented by context-free hedge automata, hence beyond the regular (HA) ones. These results are interesting for automated verification where reachability sets are not always regular.

To summarize, several XML validation or infinite-state verification problems would benefit from procedures to compute rewrite-closure of hedge languages. We also need decidable formalisms beyond regular tree languages to capture rewrite closures. Contributions. In [START_REF] Jacquemard | Rewrite-based verification of XML updates[END_REF] we have proposed a model for XML update primitives of XQUF as parameterized rewriting rules of the form: "insert an unranked tree from a regular tree language L as the first child of a node labeled by a". For these rules, we give type inference algorithms, considering types defined by several classes of unranked tree automata. In particular we have considered contextfree hedge automata (CFHA, e.g. [START_REF] Jacquemard | Closure of Hedge-automata languages by Hedge rewriting[END_REF]), a more general class than regular hedge automata and obtained by requiring that the sequences of sibling states under a node to be in a context-free language. In this submission we first introduce a non-trivial extension of context-free hedge languages defined by what we call bidimensional context-free hedge automata (Section 2). This class is more expressive as shown by examples. The class is also shown to be preserved by rewrite closure when applying inverse-monadic rules that are more general than the rules that were considered in [START_REF] Jacquemard | Closure of Hedge-automata languages by Hedge rewriting[END_REF](Section 3).

Then we extend the parameterized rewriting rules used for modeling XQUF in [START_REF] Jacquemard | Rewrite-based verification of XML updates[END_REF] by the possibility to insert a new parent node above a given node. We show in Section 4 how to compute the rewrite closure of HA languages with these extended rewriting systems. Although the obtained results are more general than [START_REF] Jacquemard | Rewrite-based verification of XML updates[END_REF] the proofs are somewhat simpler thanks to a new uniform representation of vertical and horizontal steps of CFHA. A full version is available at [START_REF] Jacquemard | Rewrite Closure and CF Hedge Automata[END_REF]. Related work. [START_REF] Solimando | Automata-based Static analysis of XML Document Adaptation[END_REF] presents a static analysis of XML document adaptations, expressed as sequences of XQUF primitives. The authors also use an automatic inference method for deriving the type, expressed as a HA, of a sequence of document updates. The type is computed starting from the original schema and from the XQuery Updates formulated as rewriting rules as in [START_REF] Jacquemard | Rewrite-based verification of XML updates[END_REF]. However differently from our case the updates are applied in parallel in one shot.

Preliminaries

We consider a finite alphabet Σ and an infinite set of variables X . The symbols of Σ are generally denoted a, b, c . . . and the variables x, y. . . The sets of hedges and trees over Σ and X , respectively denoted H(Σ, X ) and T (Σ, X ), are defined recursively as the smallest sets such that: every x ∈ X is a tree, if t 1 , . . . , t n is a finite sequence of trees (possibly empty), then t 1 . . . t n is a hedge and if h is a hedge and a ∈ Σ, then a(h) is a tree. The empty hedge (case n ≥ 0 above) is denoted ε and the tree a(ε) will be simply denoted by a. We use the operator . to denote the concatenation of hedges. A root (resp. leaf) of a hedge h = (t 1 . . . t n ) is a root node (resp. leaf node, i.e. node without child) of one of the trees t 1 , ..., t n . The root node of a(h) is called the parent of every root of h and every root of h is called a child of the root of a(h).

We will sometimes consider a tree as a hedge of length one, i.e. consider that T (Σ, X ) ⊂ H(Σ, X ). The sets of ground trees (trees without variables) and ground hedges are respectively denoted T (Σ) and H(Σ). The set of variables occurring in a hedge h ∈ H(Σ, X ) is denoted var (h). A hedge h ∈ H(Σ, X ) is called linear if every variable of var (h) occurs once in h. A substitution σ is a mapping of finite domain from X into H(Σ, X ), whose application (written with postfix notation) is extended homomorphically to H(Σ, X ). The set C(Σ) of contexts over Σ contains the linear hedges of H Σ, {x} . The application of

a context C ∈ C(Σ) to a hedge h ∈ H(Σ, X ) is defined by C[h] := C{x → h}.
A hedge rewriting system (HRS) R over a finite unranked alphabet Σ is a set of rewrite rules of the form ℓ → r where ℓ ∈ H(Σ, X ) \ X and r ∈ H(Σ, X ); ℓ and r are respectively called left-and right-hand-side (lhs and rhs) of the rule. Note that we do not assume the cardinality of R to be finite. A HRS is called ground, resp. linear, if all its lhs and rhs of rules are ground, resp. linear.

The rewrite relation --→ R of a HRS R is the smallest binary relation on H(Σ, X ) containing R and closed by application of substitutions and contexts. In other words, h --→ R h ′ , iff there exists a context C, a rule ℓ → r in R and a substitution σ such that h = C[ℓσ] and

h ′ = C[rσ]. The reflexive and transitive closure of --→ R is denoted --→ * R . Given L ⊆ H(Σ, X ) and a HRS R, we define the rewrite closure of L under R as post * R (L) := {h ′ ∈ H(Σ, X ) | ∃h ∈ L, h --→ * R h ′ }.

Bidimensional Context-Free Hedge Automata

A bidimensional context-free hedge automaton

(CF 2 HA) is a tuple A = Σ, Q, Q f , ∆ where Σ is a finite unranked alphabet, Q is a finite set of states disjoint from Σ, Q f ⊆ Q is a set of final
states, and ∆ is a set of rewrite rules of one of the following form, where p 1 , . . . , p n ∈ Q ∪ Σ, q ∈ Q and n ≥ 0

p 1 (x 1 ) . . . p n (x n ) → q(x 1 . . . x n ) called horizontal transitions, p 1 p 2 (x) → q(x) called vertical transitions.

The move relation --→

A between ground hedges of H(Σ ∪ Q) is defined as the rewrite relation defined by ∆. The language of a CF 2 HA A in one of its states q, denoted by L(A, q), is the set of ground hedges h ∈ H(Σ) such that h --→ * A q (we recall that q stands for q(ε)). A hedge is accepted by A if there exists q ∈ Q f such that h ∈ L(A, q). The language of A, denoted by L(A) is the set of hedges accepted by A. We shall also consider below the following kind of transitions, which have the same expressiveness as CF 2 HA.

p 1 (δ 1 ) . . . p n (δ n ) → q(δ 1 . . . δ n ) p 1 (p 2 (δ 1 )) → q(δ 1 ) n > 0 every δ i is either a variable x i or ε Example 2. The language of T-patterns over Σ = {a, b, c}, see Example 1, is recognized by Σ, {q 0 , q 1 , q 2 }, {p 0 }, ∆ with ∆ = {b(x 1 ) → q 0 (x 1 ), a.q 0 (x 2 ) → q 1 (x 2 ), q 1 (x 1 ).c → q 2 (x 1 ), q 2 (b(x)) → q 0 (x)}.

Related Models

The CF 2 HA capture the expressiveness of two models of automata on unranked trees: the hedge automaton [START_REF] Murata | Hedge automata: a formal model for XML schemata[END_REF] and the lesser known extension of [START_REF] Ohsaki | Recognizing boolean closed a-tree languages with membership conditional rewriting mechanism[END_REF] that we call CFHA. A hedge automaton (HA), resp. context-free hedge automaton

(CFHA) is a tuple A = Σ, Q, Q f , ∆
where Σ, Q and Q f are as above, and the transitions of ∆ have the form a(L) → q where a ∈ Σ, q ∈ Q and L ⊆ Q * is a regular word language (resp. a context-free word language). The language of hedges accepted is defined as for CF 2 HA, using the rewrite relation of ∆.

The CFHA languages form a strict subclass of CF 2 HA languages. Indeed every CFHA can be presented as a CF 2 HA with variable-free transitions of the form p 1 . . . p n → q a(q 1 ) → q 2 where a ∈ Σ and q 1 , q 2 are states.

It can be shown that the set of T-patterns of Example 2 is not a CFHA language, using a pumping argument on the paths labeled by b.

The HA languages, also called regular languages, also form a strict subclass of CF 2 HA languages. Every HA can indeed be presented as a CF 2 HA A = (Σ, Q, Q f , ∆) with variable-free transitions constrained with a type discipline:

Q = Q h ⊎ Q v and every transition of ∆ has one of the forms ε → q h q h .q v → q ′ h a(q h ) → q v where q h , q ′ h ∈ Q h , q v ∈ Q v , a ∈ Σ.
From now on, we shall always consider HA and CFHA presented as CF 2 HA.

The following example shows that CF 2 HA can capture some CF ranked tree languages. Capturing the whole class of CF RTL would require however a further generalization where permutations of variables are possible in the horizontal transitions of CF 2 HA. Such a generalization is out of the scope of this paper.

Example 3. The language {h n (g(a n (0), b n (0))) | n ≥ 1} is generated by the CF ranked tree grammar [START_REF] Comon | Tree automata techniques and applications[END_REF] with non-terminals A and S (S is the axiom) and productions A(

x 1 , x 2 ) → h A(a(x 1 ), b(x 2 )) , A(x 1 , x 2 ) → g(x 1 , x 2
) and S → A(0, 0). It is also recognized by the CF 2 HA with transition rules a(x 1 ).b(x 2 ) → q(x 1 .x 2 ), g(x 1 ) → q 0 (x 1 ), q 0 (q(x)) → q 1 (x), h(q 1 (x)) → q 0 (x) (q 0 is final).

Properties

The class of CF 2 HA language is closed under union (direct construction by disjoint union of automata) and not closed under intersection or complementation (because CF word languages are defined by CF 2 HA without vertical transitions).

Property 4. The membership problem is decidable for CF 2 HA.

Proof. Let h ∈ H(Σ) be a given hedge and A be a given CF 2 HA. We assume wlog that A is presented as a set ∆ of transitions in the above alternative form p 1 (δ 1 ) . . . p n (δ n ) → q(δ 1 . . . δ n ), with n > 0, and p 1 (p 2 (δ 1 )) → q(δ 1 ).

Moreover, we assume that every transition of the form q 1 (x 1 ) → q 2 (x 1 ), where q 1 and q 2 are states, has been removed, replacing arbitrarily q 1 by q 2 in the rhs of the other transitions. Similarly, we remove q 1 → q 2 , replacing arbitrarily rhs's of the form q 1 by q 2 . All these transformations increase the size of A polynomialy.

Then all the horizontal transitions with n = 1 have the form a(δ 1 ) → q(δ 1 ), with a ∈ Σ. It follows that the application of every rule of ∆ strictly reduces the measure on hedges defined as pair (# of occurrences of symbols of Σ, # of occurrences of state symbols), ordered lexicographically. During a reduction of h by ∆, each of the two components of the above measure is bounded by the size of h. It follows that the membership h ∈ L(A) can be tested in PSPACE.

⊓ ⊔ Property 5. The emptiness problem is decidable in PTIME for CF 2 HA.

Proof. Let A = Σ, Q, Q f , ∆ .
We use a marking algorithm with two marks: h and v. First, for technical convenience, we mark every symbol in Σ with v. Then we iterate the following operations until no marking is possible (note that the marking is not exclusive: some states may have 2 marks h and v). For all transition p 1 (x 1 ) . . . p n (x n ) → q(x 1 . . . x n ) in ∆ such that every p i is marked, if at least one p i is marked with v, then mark q with v, otherwise mark q with h. For all transition p 1 p 2 (x) → q(x) in ∆ such that p 1 is marked v, if p 2 is marked with v, then mark q with v, otherwise, if p 2 is marked with h, then mark q with h.

The number of iterations is at most 2.|Q| and the cost of each iteration is linear in the size of A. Then q ∈ Q is marked with h only iff there exists h ∈ H(Σ) such that h --→ * ∆ q, and it is marked with v iff there exists

C[ ] ∈ C(Σ) such that for all h ∈ H(Σ), C[h] --→ * ∆ q(h). Hence L(A) = ∅ iff no state of Q f is marked. ⊓ ⊔
For comparison, for both classes of HA and CFHA, the membership and emptiness problems are decidable in PTIME, the class of HA languages is closed under Boolean operations and the class of CFHA languages is closed under union but not closed under intersection and complementation, see [START_REF] Murata | Hedge automata: a formal model for XML schemata[END_REF][START_REF] Ohsaki | Recognizing boolean closed a-tree languages with membership conditional rewriting mechanism[END_REF][START_REF] Comon | Tree automata techniques and applications[END_REF].

Inverse Monadic Hedge Rewriting Systems

A rewrite rule ℓ → r over Σ is called monadic (following [START_REF] Salomaa | Deterministic tree pushdown automata and monadic tree rewriting systems[END_REF][START_REF] Coquide | Bottom-up tree pushdown automata : Classification and connection with rewrite systems[END_REF]) if r = a(x) with a ∈ Σ, x ∈ X , inverse-monadic if r → ℓ is monadic and r / ∈ X ∪ {ε}, and

1-childvar if it contains at most one variable and this variable has no siblings in ℓ and r. Intuitively, every finite, linear, inverse-monadic, 1-childvar HRS can be transformed into a HRS equivalent wrt reachability whose rules are inverse of transitions of CF 2 HA. It follows that such HRS preserve CF 2 HA languages.

Example 6. The HRS of Example 1 is linear, inverse-monadic, and 1-childvar.

The closure of the language {p 0 } is the CF 2 HA language of T-patterns.

Theorem 7. Let L be the language of A L ∈ CF 2 HA, and R be a finite, linear, inverse-monadic, 1-childvar HRS. There exists an effectively computable CF 2 HA recognizing post * R (L), of size polynomial in the size of R and A L . Proof.

Let A L = Σ, Q L , Q f L , ∆ L , we construct a CF 2 HA A = Σ, Q, Q f , ∆ .
The state set Q contains all the states of Q L , one state h for every non-variable sub-hedge of a rhs of rule of R, one state a for each a ∈ Σ and one new state

q / ∈ Q L . For each p ∈ Q L ∪ Σ, we note p = a if p = a ∈ Σ and p = p otherwise. Let Q f = Q f
L and let ∆ 0 contain the following transition rules, where a ∈ Σ, t ∈ T (Σ, {x}) and h ∈ H(Σ, {x}) \ {ε}.

p 1 (x 1 ) . . . p n (x n ) → q(x 1 . . . x n ) if p 1 (x 1 ) . . . p n (x n ) → q(x 1 . . . x n ) ∈ ∆ L p 1 p 2 (x) → q(x) if p 1 p 2 (x) → q(x) ∈ ∆ L t(x).h → t.h(x) if x ∈ var (t), t.h ∈ Q t(x).h → q(x) if x ∈ var (t), t.h / ∈ Q t.h(x) → t.h(x) if x / ∈ var (t), t.h ∈ Q t.h(x) → q(x) if x / ∈ var (t), t.h / ∈ Q a(x) → a(x) a(h(x)) → a(h)(x) if a(h) ∈ Q a(h(x)) → a(x) if a(h) / ∈ Q a(q(x)) → a(x) Finally let ∆ = ∆ 0 ∪ {h(x) → a(x) | a(x) → h ∈ R}. Let ℓ ∈ H(Σ) be such that ℓ --→ * ∆ s(u) (⋆), with s ∈ Q and u ∈ H(Q ∪ Σ).
We show by induction on the number N of applications of rules of ∆ \ ∆ 0 in (⋆) that there exists ℓ ′ ∈ H(Σ) such that ℓ ′ --→ * R ℓ and moreover, if s = h, then h matches ℓ ′ , if s = q then ℓ ′ is not matched by a non-variable subhedge of rhs of rule of R and if s ∈ Q L , then ℓ ′ ∈ L(A L , s).

If N = 0, then the property holds with ℓ ′ = ℓ (this can be shown by induction on the length of (⋆)). If N > 0, we can assume that (⋆) has the following form.

ℓ = C[k] --→ * ∆0 C[h(v)] ----→ ∆\∆0 C[a(v)] --→ ∆ s(u) It follows that h matches k, i.e. there exists w such that k = h[w], and w --→ * ∆0 v. Hence ℓ ′ = C[a(w)] --→ R ℓ, and ℓ ′ --→ * ∆0 C[a(v)] --→ ∆0 C[a(v)] --→ ∆ s(u).
We can then apply the induction hypothesis to ℓ ′ , and immediately conclude for ℓ. ⊓ ⊔

The following Example 8 illustrates the importance of the 1-childvar and condition in Theorem 7.

Example 8. With the following rewrite rule a(x) → c a(e x g) d we generate from {a} the language {c n a(e n g n ) d n | n ≥ 1}, seemingly not CF 2 HA.

In [START_REF] Jacquemard | Closure of Hedge-automata languages by Hedge rewriting[END_REF] it is shown that the closure of a HA language under rewriting with a monadic HRS is a HA language. It follows that the backward rewrite closure of a HA language under an inverse-monadic HRS is HA.

Update Hedge Rewriting Systems

In this section, we turn to our motivation of studying XQuery Update Facility primitives modeled as parameterized rewriting rules.

Let A = Σ, Q, Q f , ∆ be a HA. A hedge rewriting system over Σ parametrized by A (PHRS) is given by a finite set, denoted R/A, of rewrite rules ℓ → r where ℓ ∈ H(Σ, X ) and r ∈ H(Σ ⊎ Q, X ) and symbols of Q can only label leaves of r (⊎ stands disjoint union, hence we implicitly assume that Σ and Q are disjoint sets). In this notation, A may be omitted when it is clear from context or not necessary. The rewrite relation ----→ R/A associated to a PHRS R/A is defined as the rewrite relation ----→ R[A] where the HRS R[A] is the (possibly infinite) set of all rewrite rules obtained from rules ℓ → r in R/A by replacing in r every state p ∈ Q by a ground hedge of L(A, p). Note that when there are multiple occurrences of a state p in a rule, each occurrence of p is independently replaced with a hedge in L(A, p), which can generally be different from one another. Given a set L ⊆ H(Σ, X ), we define post * R/A (L) to be post * R[A] (L). We call updates parametrized rewrite rules of the following form

a(x) → b(x) node renaming (ren) a(x) → a(u 1 x u 2 ) u 1 , u 2 ∈ Q * addition of child nodes (ac) a(x) → v 1 a(x) v 2 v 1 , v 2 ∈ Q * addition of sibling nodes (as) a(x) → b a(x) addition of parent node (ap) a(x) → u u ∈ Q * node replacement/recursive deletion (rpl) a(x) → x single node deletion (del)
Note that the particular case of (rpl) of rpl with u = ε corresponds to the deletion of the whole subtree a(x). In the rest of the paper, a PHRS containing only updates will be called update PHRS (uPHRS).

Loop-free uPHRS

In order to simplify the proofs we can reduce to the case where there exists no looping sequence of renaming. This motivates the following definition: Definition 9. An uPHRS R/A is loopfree if there exists no sequence a 1 , . . . , a n (n > 1) such that for all 1 ≤ i < n, a i (x) → a i+1 (x) ∈ R and a 1 = a n .

Given a uPHRS R/A, we consider the directed graph G whose set of nodes is Σ and containing an edge a, b iff a(x) → b(x) is in R. For every strongly connected component in G we select a representative. We denote by â the representative of a in its component and more generally by ĥ the hedge obtained from h ∈ H(Σ) by replacing every function symbol a by its representative â. We define R to be R where every rule ℓ → r is replaced by l → r (if the two members get equal we can remove the rule). We define  analogously.

Lemma 10. Given an uPHRS R/A the uPHRS R/ Â is loopfree and for all h, h ′ ∈ H(Σ) we have h ----→ * R/A h ′ iff ĥ ---→ * R/ Â ĥ′ . Proof. By induction on the length of derivations.

⊓ ⊔

Rewrite Closure

The rest of the section is devoted to the proof of the following theorem of construction of CF 2 HA for the forward closure by updates.

Theorem 11. Let A be a HA over Σ, and L be the language of A L ∈ CFHA, and R/A be a loop-free uPHRS. There exists an effectively computable CFHA recognizing post * R/A (L), of size polynomial in the size of R/A and A L and exponential in the size of the alphabet Σ.

The construction of the CFHA works in 2 steps: construction of an initial automaton and completion loop. We shall use the following notion in order to simplify the proof: a CFHA Σ, Q, Q f , ∆ is called normalized if for all a ∈ Σ and q ∈ Q, there exists one unique state of Q denoted q a such that a(q a ) → q ∈ ∆, and moreover, q a does neither occur in a left hand side of an horizontal transition of ∆ nor in a right hand side of a vertical transition of ∆. With some state renaming, every CFHA A can be transformed in PTIME into a normalized CFHA A ′ , of size linear in the size of A, and such that L(A ′ ) = L(A).

Initial automaton. Let

A = Σ, Q A , Q f A , ∆ A and A L = Σ, Q L , Q f L , ∆ L .
We assume that the state sets Q A and Q L are disjoint.

First, let us merge A and A L into a CFHA B = Σ, P, P f , Γ obtained by the normalization of

Σ, Q A ⊎ Q L , Q f L , ∆ A ⊎ ∆ L .
Below, the states of P will be denoted by the letters p or q. Let P in be the subset of states of P of the form q a (remember that q a is a state of P uniquely characterized by a ∈ Σ, q ∈ P , since B is normalized). We assume wlog that P in and P f are disjoint and that B is clean, i.e. for all p ∈ P , L(B, p) = ∅.

Next, in a preliminary construction step, we transform the initial automaton B into a CFHA A 0 = Σ, Q, Q f , ∆ 0 . Let us call renaming chain a sequence a 1 , . . . , a n of symbols of Σ such that n ≥ 1 for all 1 ≤ i < n, a i (x) → a i+1 (x) ∈ R. Since R is loop-free, the length of every renaming chains is bounded by |Σ|. The fresh state symbols of Q are defined as extensions of the symbols of P \ P in with renaming chains. We consider two modes for such states: the push and pop modes, characterized by a chain respectively in superscript or subscript. Q = P ∪ {q a | q a ∈ P in } ∪ q a1...an q ∈ P \ P in , n ≥ 2, q a1...an a 1 , . . . , a n is a renaming chain Let Q f = P f be the subset of final states. Intuitively, in the state q a1...an , the chain of Σ + represents a sequence of renamings, with R/A, of the parent of the current symbol, starting with a 1 and ending with a n . Note that the states of P in are particular cases of such states, with a chain of length one. A state q a1...an will be used below to represent the tree a n (q a1...an ). The initial set of transitions ∆ 0 is defined as follows

∆ 0 = Γ h ∪ {q a1 → q | q a1 ∈ Q} ∪ {a n q a1...an → q a1...an | q a1...an , q a1...an ∈ Q, n ≥ 1}
where Γ h is the subset of horizontal transitions of Γ . Note that A 0 is not normalized. The following lemma is immediate by construction of Γ and A 0 .

Lemma 12. For all q ∈ Q A (resp. q ∈ Q L ) L(A 0 , q) = L(A, q) (resp. L(A L , q)).

Proof. Every vertical transition in Γ has the form a(q a ) → q and can be simulated by the 2 steps a(q a ) → q a → q. Moreover, all the states q a1...an and q a1...an with n ≥ 2 are empty for A 0 .

⊓ ⊔

For the construction of A ′ , we shall complete incrementally ∆ 0 into ∆ 1 , ∆ 2 ,... by adding some transition rules, according to a case analysis of the rules of R/A.

For each construction step i ≥ 0, we let

A i = Σ, Q, Q f , ∆ i .
Automata completion. The construction of the sequence (∆ i ) works by iteration of a case analysis of the rewrite rules of R/A, presented in Table 1. Assuming that ∆ i is the last set built, we define its extension ∆ i+1 by application of the first case in Table 1 such that ∆ i+1 = ∆ i . In the rules of Table 1, a 1 , . . . , a n , b are symbols of Σ, and u, v are sequences of Q * A .

R/A contains ∆i+1 = ∆i∪ (ren) an(x) → b(x) {q a 1 ...an → q a 1 ...anb | q a 1 ...anb ∈ Q} ∪ {q a 1 ...anb → qa 1 ...an | q a 1 ...anb ∈ Q} (ac) an(x) → an(u x v) {u q a 1 ...an v → q a 1 ...an | q a 1 ...an ∈ Q} ..an → qa 1 ...an | q a 1 ...an ∈ Q} Table 1. CFHA Completion

Only a bounded number of rules can be added to the ∆ i 's, hence eventually, a fixpoint ∆ k is reached, that we will denote ∆ ′ . We also write A ′ for A k .

The following Lemma 13 shows that the automata computations simulate the rewrite steps, i.e. that L(A ′ ) ⊆ post * R/A (L). Let us abbreviate R/A by R. We use the notation h -----→ R a1...an h ′ , for a renaming chain a 1 , . . . , a n (n ≥ 1), if there exists h 1 , . . . h n ∈ H(Σ) such that

h = a 1 (h 1 ) --→ * R a 1 (h 2 ) --→ ren a 2 (h 2 ) --→ * R . . . --→ * R a n-1 (h n ) --→ ren a n (h n ) --→ * R h ′
where the reductions denoted --→ ren are rewrite steps with rules of R/A of type (ren), applied at the positions of a 1 ,. . . , a n , and all the other rewrite steps (denoted --→ * R ) involve no rule of type (ren). Lemma 13 (Correctness). For all h ∈ H(Σ), i. if h --→ * A ′ q a1...an , with n ≥ 1, then there exists h 1 ∈ H(Σ) such that a 1 (h 1 ) -→ * B q and a 1 (h 1 ) -----→ R a1...an h, ii. if h --→ * A ′ q a1...an , with n ≥ 1, then there exists h 1 ∈ H(Σ) such that h 1 -→ * B q a1 , and a 1 (h 1 ) -----→ R a1...an a n (h),

iii. if h --→ * A ′ q ∈ P \ P in , then there exists h ′ ∈ H(Σ) such that h ′ -→ * B q and h ′ --→ * R h. Proof. (sketch) Let s ∈ Q be such that h --→ * A ′ s and let us call ρ this reduction. With a commutation of transitions, we can assume that ρ has the following form,

ρ : h = t 1 . . . t m --→ * A ′ s 1 . . . s m --→ * A ′ s ρ 0
where t 1 , . . . , t m ∈ T (Σ), s 1 , . . . , s m ∈ Q, and for all 1 ≤ i ≤ m, t i --→ * A ′ s i , and the last step of this reduction involves a vertical transition a(q a1...an ) → s i or b(q a1...an ) → s i . The proof is by induction on the length of ρ.

The shortest possible ρ has 2 steps: h = t 1 = a(ε) --→ A0 a(q a ) --→ A0 q = s and (iii) holds immediately with h ′ = h, by Lemma 12.

For the induction step, we consider the length of ρ 0 . If |ρ 0 | = 0, we have necessarily m = 1, and the reduction ρ has one of the two following forms (v ∈ Q * ).

h = t 1 = b(h ′ ) --→ * A ′ b(v) --→ * A ′ b(q a1...an ) --→ A ′ q a1...an = s 1 = s (1)
h = t 1 = a n (h ′ ) --→ * A ′ a n (v) --→ * A ′ a n (q a1...an ) --→ A0 q a1...an = s 1 = s (2)
In the case (1), assume that the vertical transition b(q a1...an ) → q a1...an has been added to A ′ because R/A contains a rule a n (x) → b a n (x) . By induction hypothesis (i) applied to the sub-reduction h ′ --→ * A ′ q a1...an , there exists h 1 ∈ H(Σ) such that a 1 (h 1 ) -→ * B q, and a 1 (h 1 ) -----→ R a1...an h ′ . It follows in particular that there exists h n such that a n (h n ) --→ * R h ′ , and using the above (ap) rewrite rule,

a n (h n ) --→ R b a n (h n ) --→ * R b(h ′ ) = h. Therefore, a 1 (h 1 ) -----→ R a1.
..an h and (i) holds for h and s.

In the case (2), by induction hypothesis (ii) applied to the sub-reduction h ′ --→ * A ′ q a1...an , there exists h 1 ∈ H(Σ) such that h 1 -→ * B q a1 , hence a 1 (h 1 ) -→ * B q, and a 1 (h 1 ) -----→ R a1...an a n (h ′ ) = h. Therefore (i) holds for h and s.

Assume now that |ρ 0 | > 0, and let us analyze the horizontal transition rule used in the last step of ρ 0 . In order to comply with spaces restrictions, we will present only one significant case in this extended abstract (see [START_REF] Jacquemard | Rewrite Closure and CF Hedge Automata[END_REF] for the other cases).

Case (ac). The last step of ρ 0 uses u q a1...an v → q a1...an and this transition has been added to

∆ ′ because R/A contains a rule a n (x) → a n (u x v), with u, v ∈ Q * A .
In this case, the reduction ρ has the following form,

h = ℓ h ′ r --→ * A ′ u q a1...an v --→ A ′ q a1...an = s (3)
where ℓ --→ * A ′ u, h ′ --→ * A ′ q a1...an , and r --→ * A ′ v. By induction hypothesis (ii) applied to h ′ --→ * A ′ q a1...an , there exists h 1 such that h 1 -→ * B q a1 and a 1 (h 1 ) -----→ The proof is by induction on the length of the rewrite sequence h --→ * R h ′ (see [START_REF] Jacquemard | Rewrite Closure and CF Hedge Automata[END_REF]). As another consequence of the result of [START_REF] Jacquemard | Closure of Hedge-automata languages by Hedge rewriting[END_REF] on the rewrite closure of HA languages under monadic HRS, the backward closure of a HA language under an uPHRS is HA.

The rules of type (ren), (as), (ap) and (rpl) can be easily simulated by the HRS of Theorem 11. In particular, the parameters' semantics can be simulated using ground rewrite rules (with such rules, a symbol can generate a HA language). The rules (ac) are not 1-childvar and the rules (del) is not inverse-monadic.

Example 8 shows the problems that can arise when combining in one single rewrite rule two rules of the form (as) and (ac), forcing synchronization of two updates. Note that the rule a(x) → c a(e x g) d of this example can be simulated by the 2 rules a(x) → c a ′ (x) d and a ′ (x) → a(e x g). The former rule is of the type of Theorem 11 (it combines types (as) and (ren)). The latter (which is not 1-varchild) combines types (ac) and (ren). This shows that such combinations can also lead to the behavior exposed in Example 8.

Future Works

As for future works on CF 2 HA languages several directions deserve to be followed. A first direction might be to derive pumping properties for these classes of languages.

A second direction would be to look for an analogous of Parikh characterization for the number of different symbols occurring in the hedges of given CF 2 HA languages. One may define and study HRS with counting constraints on horizontal and vertical paths.

Finally, it would be is worth investigating the parallel rewriting of [START_REF] Solimando | Automata-based Static analysis of XML Document Adaptation[END_REF], on all a-positions, since it is closer to the semantics of XQUF, and get an analogous of Theorem 11 for the parallel rewrite closure.

Example 1 .

 1 Let us consider the following rewrite rules R = {p 0 (x) → a.p 1 (x), p 1 (x) → p 2 (x).c, p 2 (x) → p 0 (b(x)), p 2 (x) → b(x)}. Starting from p 0 = p 0 (ε), we have the following rewrite sequence p 0 → a.p 1 → a.p 2 .c → a.p 0 (b).c → a.a.p 1 (b).c → a.a.p 2 (b).c.c → a.a.p 0 (b(b)).c.c → . . . The trees of the rewrite closure of p 0 under R which do not contain the symbols p 0 , p 1 , p 2 is the set of T-patterns of the form a . . . a.b(. . . b(b)).c . . . c with the same number of a, b and c.

(

  as) an(x) → u an(x) v {u qa 1 ...an v → qa 1 ...an | qa 1 ...an ∈ Q} (ap) an(x) → b an(x) {b qa 1 ...an → qa 1 ...an | qa 1 ...an ∈ Q} (rpl) an(x) → u {u → qa 1 ...an | qa 1 ...an ∈ Q} (del) an(x) → x {q a 1 .

R

  a1...an a n (h ′ ), and by induction hypothesis (iii) applied to ℓ --→ * A ′ u (resp. r --→ * A ′ v), and by Lemma 12, there existsℓ ′ ∈ H(Σ) (resp. r ′ ∈ H(Σ)) such that ℓ ′ --→ * A u (resp. r ′ --→ * A v) and ℓ ′ --→ * R ℓ (resp. r ′ --→ * R r). It follows that a n (h ′ ) --→ R a n (ℓ ′ h ′ r ′ ) --→ * R a n (ℓ h ′ r) = a n (h). Hence a 1 (h 1 ) -----→ R a1...an a n (h) and (ii) holds for h and s. ⊓ ⊔Corollary 14. L(A ′ ) ⊆ post * R/A (L) Proof. By definition of Q f , h ∈ L(A ′ ) iff h --→ * A ′ q ∈ P f = Q f L , and P f ⊆ P \ P in . By Lemma 13, case (iii), it follows that h ∈ post * R/A (L(B, q)) ⊆ post * R/A (L). ⊓ ⊔ Lemma 15 (Completeness). For all h ∈ H(Σ) and s ∈ Q, if h --→ * A0 s and h --→ * R h ′ , then h ′ --→ * A ′ s.

⋆ This work has been partly supported by the ANR ContINT grantINEDIT (2012-15).