R Beuton

B Chimier

J Breil

D Hébert

K Mishchik

J Lopez

P H Maire

G Duchateau

Thermo-elasto-plastic simulations of femtosecond laser-induced multiple-cavity in fused silica

The formation and the interaction of multiple cavities, induced by tightly focused femtosecond laser pulses, are studied by using a developed numerical tool, including the thermo-elasto-plastic material response. Simulations are performed in fused silica in cases of one, two, and four spots of laser energy deposition. The relaxation of the heated matter, launching shock waves in the surrounding cold material, leads to cavity formation and emergence of areas where cracks may be induced. Results show that the laser-induced structure shape depends on the energy deposition configuration and demonstrate the potential of the used numerical tool to obtain the desired designed structure or technological process.

INTRODUCTION

Modifying the properties of dielectric materials, by inducing designed structures on the surface or in the bulk, is interesting for various industrial and technological applications [1,2,3,4,5,6,7,8,[START_REF] Kumkar | Proc. SPIE[END_REF][START_REF] Buividas | [END_REF]11,[START_REF] Hendricks | Proc. SPIE[END_REF]. Due to the nonlinear mechanisms of the laser energy absorption and the low thermal diffusion during the laser irradiation, femtosecond laser pulses are an attractive tool for microprocessing such kind of materials.

By using tightly focused femtosecond laser pulses, 3D nano-structures such as cavities can be induced in the bulk of dielectrics [START_REF] Glezer | [END_REF]14,15,16,17,18,19,20]. During the laser-matter interaction, nonlinear processes lead to a significant absorption of the laser energy in the focal volume. The heated material is confined, creating a warm dense matter surrounded by a non-modified solid cold material. The induced high pressure and temperature, in the heated volume, then launche a shock wave which propagates in the surrounding matter, followed by rarefaction waves which dig the material. Plastic and elastic deformations are then induced in the surrounding matter depending on the irradiation conditions. For absorbed energy densities above the material damage threshold, a significant permanent structural modification may appear due to the generated plastic deformations induced by the compression and traction waves in the solid matter [21,22,23,24].

To understand the physical processes taking place during the heated volume relaxation, in the particular case of tightly focused beams, a thermo-elasto-plastic model has been recently implemented in a lagrangian hydrodynamic code [25]. A model for the predictions of the critical areas, where cracks may appears, has been also presented. Results have shown the importance of the solid response (the elasto-plastic behavior) in the cavity generation process and the effect of the energy deposition geometry on the potential cracks formation.

In the present paper, this previous work and the developed numerical tools are used to simulate the generation of multiple-cavity structures in the bulk of fused silica. A short description of the theoretical model [START_REF] Wilkins | Methods in Computational Physics, volume 3, chapter Calculation of Elastic-Plastic Flow[END_REF][START_REF] Maire | [END_REF] is presented in Section 2. The simulations are performed by assuming an instantaneous energy deposition. The single-cavity case is first considered, as it corresponds to the simplest configuration, to understand the main phenomena at play. It is then generalized to the study of double-and multiple-cavity generation, where the interaction between sub-structure is investigated. Especially, various cases will be studied to highlight the cooperative mechanisms responsible for the formation of particular nano-structures and micro-structures, useful in many applications [28,29,30,31]. The case of two cavities, separated by a few tenth of micrometers, shows an increase of the compressive and shear stresses, compared to the single cavity generation, which leads to critical areas by compression during a time larger than the single spot one. This case also induces critical areas associated to shear. Furthermore, the influence of the distance between these two cavities is studied. Finally, the interaction between multiple cavities is presented in two different cases (simultaneous and delayed energy depositions). Different shapes of the formed cavities and spatial repartitions of the critical areas are obtained, depending on the considered case. The results and discussions, for the different studied cases, are presented in Section 3. Conclusions and perspectives are drawn in Section 4.

THERMO-ELASTO-PLASTIC MODEL

The hydrodynamic response of the material, locally submitted to a fast heating, can be described by a generalized lagrangian form of the hydrodynamic conservation laws [START_REF] Maire | [END_REF]25], where the thermodynamic pressure is substituted by the Cauchy stress tensor σ [START_REF] Irgens | Continuum Mechanics[END_REF]:

ρ d dt ( 1 ρ ) -∇.V = 0 (1) ρ dV dt -∇. σ = 0 (2)
ρ dE dt -∇.( σ.V) = 0 (3)
ρ, V and E are the density, the velocity and the specific total energy, respectively. The Cauchy stress tensor can be decomposed into two terms:

σ = -P I d + S ( 4
)
where the first term, depending on the thermodynamic pressure P , accounts for the fluid response of the matter (I d is the identity matrix). The second term, depending on the deviatoric part of the Cauchy stress tensor S, accounts for the solid behavior, especially by including the shear stresses. The thermodynamic pressure is evaluated through an equation of state (EOS), while S is evaluated by solving a differential equation depending on the shear modulus, the strain rate tensor and the antisymmetric part of the velocity gradient [START_REF] Maire | [END_REF]. Since the strain rate tensor depends on the regime of deformation, a yield criterion is required. In the present study, the von Mises yield criterion is used [START_REF] Mises | [END_REF]. In this case, an equivalent stress can be defined as:

σ eq = 3 2 T r( S. S) (5)
By comparing this local effective stress to the yield strength of the material, i.e. its elastic limit, the regime of deformation is deduced. The plastic regime takes place for equivalent stresses exceeding the yield strength, while the elastic regime occurs for equivalent stresses lower than the yield strength [25].

From the knowledge of the Cauchy stress tensor, the present thermo-elasto-plastic model allows one to perform the laser induced principal stresses in compressiontraction and the maximum shear stresses, in each spatial position. That permits to determine different critical areas where potential cracks (fractures) may appear by comparing them to the intrinsic mechanical limits. The strength limits of the material can be defined by the resistance in compression L c , traction L t and shear L t /2 (the shear stress is the most efficient mechanism to induce cracks in materials) [START_REF] Spenlé | Guide du calcul en mécanique[END_REF]. If the principal stresses or maximum shear stress exceeds the associated previous limits, then the material may break, i.e. cracks may appear [25].

Finally, a thermal softening is introduced in the model to account for the solid-liquid phase transitions, depending on the specific internal energy. For an internal energy larger than the energy of melting, the solid behavior is removed ( S is canceled) and the classical Euler's equations are retrieved.

Based on this model, a second order cell-centered Lagrangian numerical scheme has been developed in a 2D planar geometry [START_REF] Maire | [END_REF]. It has been implemented in a hydrodynamic code [START_REF] Breil | [END_REF] to study the formation of cavity, induced by tightly focused femtosecond laser pulse, in dielectrics [25].

RESULTS AND DISCUSSION

In the present study, the formation of different nanostructures, based on the generation of cavities in the bulk of fused silica, are considered. For each energy deposition, a gaussian shape is assumed with a radius set to 0.13 µm at half maximum [15] (such a small size for the energy deposition is possible due to nonlinear effects). A single absorbed energy is set to 6 nJ to get a final cavity radius around 0.4 µm, according to the experimental observations. Note that a change in the amount of energy deposition leaves unchanged the general trends provided hereafter, the main influence being to modify as usually the amplitude of waves, their dynamics, etc... The EOS used in the simulations, giving the pressure and the temperature from the knowledge of the density and the specific internal energy, is the SESAME table 7386 [START_REF] Boettger | SESAME equation of state number 7386, fused quartz[END_REF] for fused silica. Within these conditions, the EOS predicts initial pressure and temperature around 0.3 TPa and 10 5 K, respectively, for each energy deposition area. The initial density is equal to 2.2 g/cm 3 . The yield strength and the shear modulus, for initial standard conditions, are Y 0 = 7.1 GPa and µ 0 = 22.6 GPa, respectively [25]. The strength limit in traction L t and in compression L c are set to characteristic values (microscopic scale) of 8 GPa and 10 GPa, respectively [START_REF] Pedone | [END_REF] (resistance in compression is generally larger than resistance in traction for brittle materials as fused silica [START_REF] Fanchon | Guide de mecanique : Sciences et technologies industrielles[END_REF]). The full cartesian mesh size for simulations is set to 18 µm×18 µm, with initial cell size set to 50 nm×50 nm. All the previous parameters are used throughout the paper.

Single energy deposition

Here is considered a single energy deposition in the center of the 2D domain. Figure 1 presents the 2D spatial map of the density (Fig. 1(a)) and its associated radial density profile (Fig. 1(b)), given by the simulation at 1 ns after the energy deposition. Within these conditions, a cavity with a radius around 0.4 µm is formed, surrounded by an overdensity shell, stabilized at this time. The void and the overdensity have a density lower than 0.25 g/cm 3 and larger than 2.25 g/cm 3 , respectively.

The temporal evolution of the cavity radius is presented in Fig. 2. It is mainly composed of three steps: an expansion, a contraction (shrinking) and a stabilization [25]. The first step is due to the formation of a strong shock, followed by rarefaction waves which form the void. In the same time, plastic and elastic deformations are induced (elasto-plastic wave) in the surrounding material and stresses are accumulated. When the shock transforms into a pure elastic wave (stresses has decreased after the shock), the expansion stops and the cavity radius reaches its maximum value (which does not correspond to the maximum stressed state). Then, corresponding to the above-mentioned second step, the decompression of the previously compressed material by the shock, i.e. the relaxation of the elastic deformations, close partially the cavity. Finally, the cavity stabilizes (third step) due to the previously induced permanent deformations (plastic deformations).

Within these conditions, an evaluation of the principal stresses has been performed. Maximum stresses are observed 200 ps after the energy deposition, during the expansion of the cavity. However, only compressive stresses can induce a critical area, where their values are greater than the strength limit in compression L c . Shear stresses are not high enough to induce a critical zone due to the homogeneous distribution of the compressive wave in the present case. Principal stress in compression σ II , with its associated critical area, are presented in Fig. 3. Due to the isotropic energy deposition, the compression is homogeneously distributed around the created void (Fig. 3(a)) and the associated critical region is a ring (Fig. 3(b)). Finally, this critical region disappears around 220 ps, when the amplitude of the shock wave is lower than L c .

Double energy deposition

The case of a simultaneous double energy deposition is now considered. The total energy is set to 12 nJ, which is twice the previous absorbed energy, distributed within two main spots separated by 0.72 µm. In this two cavities, separated by a slightly denser region, are created. The interaction between the two shock waves, launched by each energy deposition, leads to a particular behavior. In the horizontal direction outwards the cavities, the shock waves mainly propagate as in the previous single cavity case. In the inward direction, the shock waves collide, leading to a daughter wave in the perpendicular direction with a larger amplitude. Figures 4 presents the 2D density map and the density profile along the x axis, at 270 ps after the energy deposition. The two formed cavities are surrounded by an inhomogeneous overdense zone, where two symmetric regions are highly compressed in the vertical direction due to the daughter wave. Moreover, the asymmetric propagation and shape of the shock waves lead to an elongation of the two cavities in the vertical direction, as observed experimentally by Zimmermann et al. [START_REF] Zimmermann | [END_REF]. In this case, shear stresses may be high enough to induce potential cracks.

The evaluation of the principal stresses in compression and the maximal shear stresses, with their associated critical areas, are presented in Figs. 5 and6, respectively. Two different times are considered for the principal stresses in compression. At 200 ps after the energy deposition (Figs. 5(a) and(b)), the contributions of both the mother and the daughter waves are visible, leading to a critical area by compression in Fig. 5(b) relatively isotropic, as in Fig. 3(b). However, as discussed in the previous section, the mother wave amplitude is lower than L c after around 220 ps and no longer contributes to induce potential cracks. At 270 ps after the energy deposition (Figs. 5(c) and (d)), only the contribution of the daughter wave induces a high enough compressive stress in the vertical direction, resulting in both the upper and lower regions of maximal stress in excess of the strength limit, as shown in Fig. 5(d). Moreover, the asymmetric distribution of compressive stresses, at this time, leads to an elongation of the cavities in the vertical direction. It induces strong enough shear stresses (maximal at 270 ps) on the left and right sides (Fig. 6(a)) to create two symmetric associated critical areas in the horizontal direction, as depicted by Fig. 6(b).

The evolution of the critical regions depends on the distance d between the two centers of the energy deposition spots. If the two spots are too close (d ≤ 0.43 µm within the present conditions), the two generated cavities merge during their growth, ultimately leading to only one cavity. The distribution of the compressive stresses, in the surrounding matter, is almost homogeneous as in Fig. 3. The amplitude of the shear stresses becomes too low to induce any associated critical area. If the distance d is too large (d ≥ 0.81 µm), the amplitude of the daughter wave, resulting from the two shock waves collision, is not high enough to lead to an important inhomogeneous repartition of compressive stresses. The resulting shear stress is then not high enough to induce any critical area and potential cracks.

Application to laser-induced multiple cavities

The double cavities are now generalized to the multiplecavity case. The formation of four cavities is investigated here, this number being sufficiently large to exhibit complex waves interaction. The total energy is set to 24 nJ and the distance between two neighbor spots is 0.72 µm. In a first case, four simultaneous energy depositions are considered. Four shock waves are then launched simultaneously. Their interaction leads to various daughter waves, with a larger amplitude than the double-cavity case, propagating in the vertical direction. In a second case, the four energy depositions are absorbed with a delay of 100 ps between two subsequent spots. This delay value ensures that each energy deposition takes place in the non-modified material. In this case, the four shock waves, which are launched at different times, interact mainly in the horizontal direction with an accumulation of compression waves in this direction. In the vertical direction, the formation of daughter waves cannot appear due to the delayed launching of the shock waves.

Figure 7 shows the 2D spatial maps of the final density profiles in the case of the simultaneous (Fig. 7(a)) and the delayed (Fig. 7(b)) four energy depositions. In the first case (Fig. 7(a)), four elongated cavities are formed, with roughly the same size and the same aspect ratio. They are surrounded by an inhomogeneous overdensity area, larger in the vertical direction. As explained previously, the interacting shock waves induce daughter waves with a larger amplitude in the vertical axis. Thus the matter is more strongly compressed in this direction, leading to the observed overdensity zone.

In the second case (Fig. 7(b)), four elongated cavities are also generated (from the left to the right as indicated by the arrow). However, their sizes and aspect ratios are slightly different. The first cavity (on the left), which expand freely during 100 ps, is roughly similar to the single energy deposition case, but the last cavity (on the right) is smaller and more elongated in the vertical direction. This is due to the progressive accumulation of shock waves, leading to a stressed state more important for each new forming cavity. Indeed, the expansion is more strongly slowed down because each new cavity is submitted to the shock waves of the previous energy depositions. Furthermore, for the same reasons (accumulation of compressive stresses), the overdensity regions, around each cavity, slightly increase from the left to the right.

Figure 8 shows the 2D maps of the evaluated principal stresses in compression (Fig. 8(a)) and the maximum shear stresses (Fig. 8(c)), with their associated critical areas (Fig. 8(b) and (d)), in the case of the simultaneous energy depositions, at 280 ps after the energy deposition (time exhibiting the largest shear stress). As in the double cavities case, the formation of daughter waves leads to two symmetric highly compressed zone in the vertical direction (Fig. 8(a)), inducing a large critical regions by compression (Fig. 8(b)). This is followed by an increase of the shear stresses in the horizontal direction (Fig. 8(c)), leading to two critical areas induced by shear (Fig. 8(d)). No shear stresses appear between the cavities due to the presence of softened glass removing the solid behavior. An increase of the distance between the energy deposition spots should conserve more solid matter between the cavities and should lead to the apparition of shear stresses in these regions. However, as seen in the previous section, for too large distances (d ≥ 0.81 µm within the present conditions), the effect of the daughter waves is not important enough to induce shear stresses greater than the material resistance in shear L t /2 and potential cracks between the cavities cannot appear. Figure 9 presents the principal stresses in compression and the maximum shear stresses, with their associated critical area, for the case of the delayed en-ergy depositions, at 550 ps after the first energy deposition (time exhibiting the largest shear stress). The accumulated compression waves in the horizontal direction (Fig. 9(a)), leads to create only one critical area by compression, located on the right side of the last cavity (Fig. 9(b)). An increase of the shear stresses in the vertical direction is induced (Fig. 9(c)) and two symmetric critical areas by shear stresses are generated in this direction (Fig. 9(d)). Cracks are then expected in these zones, perpendicular to the formation direction of the cavities, as experimentally observed [START_REF] Zimmermann | [END_REF].

Thus, by only changing one parameter, here the dynamics of energy deposition, the interactions between the generated cavities can be controlled and tuned in order to obtain the desired designed structures.

CONCLUSION

An application of a developed numerical tool, including a thermo-elasto-plastic model, has been carried out to study the formation of complex nano-structures, as multiple-cavity, induced by femtosecond laser tightly focused in the bulk of fused silica. First, the case of a single deposition has been presented to explain the dynamics of a cavity formation. The evolution of the cavity radius, closely linked to the surrounded solid response, is defined by mainly three steps. The evaluation of the principal stress in compression and the maximum shear stress, during the cavity formation, has shown that cracks may only be induced by compression during the first step. The shear stress is not high enough in this case, due to the spherical symmetry of the system.

The case of a simultaneous double deposition has then been investigated. It turns out that the collision of the two shock waves between the cavities leads to a daughter wave, with a larger amplitude in the perpendicular direction. The latter induces an inhomogeneous distribution of compressive stresses and two elongated cavities, surrounded by an inhomogeneous overdense region. Within these conditions, due to the formation of daughter waves, the shear stress is high enough to induce critical areas where cracks may form. Furthermore, the principal stress in compression is larger than the strenght limit in compression of the material during a longer time. This behavior is observed as soon as the distance between the two energy deposition areas is not too close or too far.

The multiple-cavity case is also considered by simulating four energy depositions. First, the four energy depositions are simultaneous. That leads to the interaction and collision of four shock waves generating daughter waves. Within these conditions, four slightly similar elongated cavities are formed, surrounded by an inhomogeneous overdense region. As in the previous case, high compressive stresses are induced in the perpendicular direction to the energy depositions line, inducing two symmetric critical areas by compression in this direction and two symmetric critical areas by shear in the perpendicular direction. Then, the four energy depositions are delayed. This regime has shown that the shock waves interact mainly in the direction of alignment of the energy depositions with an accumulation of compressive stresses in this direction. Four cavities are then generated, with slightly different sizes and with a different aspect ratios due to the increase of stress (accumulation of compressive stresses) around each new cavity. The high compressive stresses accumulated induces only one critical area by compression in the front of the scanning direction. An increase of the shear stresses in the perpendicular direction leads to two symmetric critical areas. Thus, depending on the energy deposition configuration, the location of critical areas changes significantly.

The results obtain in this study can be generalized to other dielectric materials. They show the importance of the choice of energy deposition setup to obtain a desired structuration of a dielectric material. Depending on the configuration, elongated or spherical cavities can be formed, while cracks may appear in different localized areas. They highlight also the strong potential of a numerical tool including hydrodynamic and thermoelasto-plastic material responses, to predict and design laser-induced nano-structures.

ACKNOWLEDGMENTS

Vladimir Tikhonchuk and Jocelain Trela are acknowledged for fruitful discussions. The CEA and the Région Aquitaine (MOTIF project) are acknowledged for supporting this work.

Fig. 1

 1 Fig. 1 (a) 2D density map and (b) associated radial density profile at 1 ns.

Fig. 2

 2 Fig. 2 Evolution of the cavity radius as a function of time. It can be decomposed into three steps as shown by the horizontal arrows.

Fig. 3

 3 Fig. 3 (a) 2D map of principal stresses in compression σ II . (b) Critical area in compression around the cavity.

Fig. 4

 4 Fig. 4 (a) 2D map of the density and (b) the density profile along the x axis at 250 ps.

Fig. 5

 5 Fig. 5 2D spatial profiles of the principal stresses in compression with their associated critical areas at (a,b) 200 ps and (c,d) 270 ps.

Fig. 6

 6 Fig. 6 2D spatial profiles of (a) the maximum shear stresses with (b) its associated critical area at 250 ps.

Fig. 7

 7 Fig. 7 2D maps of the final density profiles in the case of (a) the simultaneous and (b) the delayed energy depositions.

Fig. 8

 8 Fig. 8 In the case of the simultaneous energy depositions: 2D spatial profiles at 280 ps for (a) the principal stress in compression with (b) its associated critical area; (c) the maximum shear stress with (d) its associated critical area.

Fig. 9

 9 Fig.9In the case of the delayed energy depositions: 2D spatial profiles at 550 ps for (a) the principal stress in compression with (b) its associated critical area; (c) the maximum shear stress with (d) its associated critical area.


Felix Klaedtke
email: felixkl@inf.ethz.ch

EHRENFEUCHT-FRA ÏSS É GOES AUTOMATIC FOR REAL ADDITION

Keywords: 1998 ACM Subject Classification: F.1.1, F.4.1 automata theory, automata-based decision procedures for logical theories, upper bounds, minimal sizes of automata, linear arithmetic over the reals, first-order equivalence, complexity

Various logical theories can be decided by automata-theoretic methods. Notable examples are Presburger arithmetic FO(Z, +, <) and the linear arithmetic over the reals FO(R, +, <), for which effective decision procedures can be built using automata. Despite the practical use of automata to decide logical theories, many research questions are still only partly answered in this area. One of these questions is the complexity of such decision procedures and the related question about the minimal size of the automata of the languages that can be described by formulas in the respective logic. In this paper, we establish a double exponential upper bound on the automata size for FO(R, +, <) and an exponential upper bound for the discrete order over the integers FO(Z, <). The proofs of these upper bounds are based on Ehrenfeucht-Fraïssé games. The application of this mathematical tool has a similar flavor as in computational complexity theory, where it can often be used to establish tight upper bounds of the decision problem for logical theories.

Introduction

Various logical theories admit automata-based decision procedures. The idea of using automata-theoretic methods to decide logical theories goes at least back to Büchi [START_REF] Büchi | Weak second-order arithmetic and finite automata[END_REF]. The elements of the domain of the logical theory are encoded by words over some alphabet in such a way that equality and the relations of the logical theory correspond to regular languages. In order to decide whether a formula is satisfiable, one constructs an automaton that precisely accepts the representatives of the elements that satisfy the formula. This automaton can be constructed by recursion over the formula structure, where standard automata constructions handle the boolean connectives and quantifiers. The satisfiability problem is thus reduced to the emptiness problem for automata.

The logical theories that admit such automata-based decision procedures are often called automatic and they have been systematically studied, e.g., in [START_REF] Blumensath | Finite presentations of infinite structures: Automata and interpretations[END_REF][START_REF] Khoussainov | Automatic presentations of structures[END_REF][START_REF] Khoussainov | Definability and regularity in automatic structures[END_REF]. Prominent and practically relevant examples are the weak monadic second-order theory of one successor WS1S, Presburger arithmetic FO(Z, +, <), and the linear arithmetic over the reals FO(R, +, <), see, e.g., [START_REF] Boigelot | An effective decision procedure for linear arithmetic over the integers and reals[END_REF][START_REF] Boigelot | Representing arithmetic constraints with finite automata: an overview[END_REF][START_REF] Büchi | Weak second-order arithmetic and finite automata[END_REF]. Tools like MONA [START_REF] Klarlund | MONA implementation secrets[END_REF] and LIRA [START_REF] Becker | LIRA: Handling constraints of linear arithmetics over the integers and the reals[END_REF], which have been applied to various verification problems, implement such automata-based decision procedures for logical theories such as WS1S, Presburger arithmetic, and the linear arithmetic over the reals. Furthermore, model checkers for counter systems like FAST [START_REF] Bardin | FAST: Fast acceleration of symbolic transition systems[END_REF][START_REF] Bardin | FAST extended release[END_REF] use an automatabased representation of sets definable in Presburger arithmetic.

A crude complexity analysis of an automata-based decision procedure leads to a nonelementary worst-case complexity. Namely, for every quantifier alternation there is a potential exponential blow-up in the state space of the automaton. For WS1S, this wost-case scenario actually exists, since the decision problem for WS1S has a non-elementary worst-case complexity [START_REF] Meyer | Weak monadic second-order theory of successor is not elementary-recursive[END_REF][START_REF] Stockmeyer | The complexity of decision problems in automata theory and logic[END_REF]. However, for many other automatic logical theories, the non-elementary complexity upper bounds of automata-based decision procedures often contrasts with the known computational complexity upper bounds on the decision problems for the logical theories. Moreover, such exponential blow-ups in the state spaces of the automata are rarely observed in practice in automata-based decision procedures for Presburger arithmetic and the linear arithmetic over the reals. In fact, in many cases, one obtains a smaller automaton after eliminating a quantifier. However, only partial answers exist that explain this phenomenon.

In [START_REF] Klaedtke | On the automata size for Presburger arithmetic[END_REF], it is shown that the size of the minimal deterministic automaton that represents a Presburger definable set is triply exponentially bounded with respect to the formula length. This upper bound is established by comparing the automata for Presburger arithmetic formulas with the formulas produced by Reddy and Loveland's quantifier-elimination method for Presburger arithmetic [START_REF] Reddy | Presburger arithmetic with bounded quantifier alternation[END_REF]. The proof on the upper bound in [START_REF] Klaedtke | On the automata size for Presburger arithmetic[END_REF] is rather tedious in the sense that several auxiliary upper bounds on the formulas that are generated by the quantifier-elimination method need to be established. These additional upper bounds depend on Reddy and Loveland's quantifier-elimination method. With the slightly different quantifier-elimination method by Cooper [START_REF] Cooper | Theorem proving in arithmetic without multiplication[END_REF], we obtain an upper bound on the automata size that has at least one additional exponent.

For the linear arithmetic over the reals, the approach of using quantifier-elimination methods to establish upper bounds on the automata sizes does not lead to a satisfactory result: an application of this approach establishes only a triple exponential upper bound on the automata size when using the quantifier-elimination method for the linear arithmetic over the reals described in [START_REF] Ferrante | A decision procedure for the first order theory of real addition with order[END_REF]. The author is not aware of any quantifier-elimination method for the linear arithmetic over the reals that would lead to a upper bound on the automata size that is smaller than triple exponential. However, since there are decision procedures for the linear arithmetic over the reals that run in double exponential deterministic time [START_REF] Ferrante | A decision procedure for the first order theory of real addition with order[END_REF], one might conjecture that the automata size is also doubly exponentially bounded.

The main result of this paper proves this conjecture. The presented proof of the double exponential upper bound is based on Ehrenfeucht-Fraïssé games (EF-games, for short from now on). It relates the states of a minimal automaton for a formula and the equivalence classes of a refinement of the equivalence relation determined by EF-games played over (R, +, <). This proof technique can also be used for other automatic logical theories to establish tight upper bounds on the automata sizes. As another example, we establish an exponential upper bound on the automata size for FO(Z, <). Note that the best known deterministic algorithms that decide FO(Z, <) run in exponential time [START_REF] Ferrante | The Computational Complexity of Logical Theories[END_REF]. In summary, the results presented in this paper shed light on the complexity of automata-based decision procedures for logical theories by identifying a relationship to EF-games.

It is worth pointing out that EF-games have already been used in similar contexts. Closely related to our work is Ladner's work [START_REF] Ladner | Application of model theoretic games to discrete linear orders and finite automata[END_REF]. He uses EF-games to show decidability of monadic second-order theories of one successor and first fragments of it. Similar to this paper, he relates the equivalence classes determined by EF-games to automata states. However, Ladner does not focus on the automata sizes and he does not consider FO(R, +, <).

The use of EF-games in computational complexity theory [START_REF] Ferrante | The Computational Complexity of Logical Theories[END_REF] and constraint databases [START_REF] Paredaens | First-order queries on finite structures over the reals[END_REF] is reminiscent of their use in this paper by partitioning the domain and connecting such a partition to the definable sets. Roughly speaking, the use EF-games for establish upper bounds on the decision problem for logical theories is as follows: The key ingredient for obtaining an upper bound for the respective logical theory is to show that the quantifiers, which can range over an infinite domain, can be relativized to a finite subset. Usually, one uses EF-games here to establish upper bounds on the sizes of such sets by analyzing the information that the formulas of a certain quantifier depth can convey. Given such a result on relativizing the quantifiers, satisfiability of a formula can be checked by an exhaustive search. The upper bounds on the sizes of the sets over which the relativized quantifiers range in turn yield upper bounds on the time and space that is needed to perform this search. For several logical theories, this use of EF-games yield tight upper bounds on the computational complexity for their decision problem.

The remainder of the paper is organized as follows. In §2, we give preliminaries. In §3, we illustrate our method by analyzing the languages that are FO(Z, <)-definable. In §4, we analyze the languages that are FO(R, +, <)-definable and establish the double exponential upper bound on the automata size. Finally, in §5, we draw conclusions. Due to space restrictions some proofs are omitted or sketched. They can be found in the full version of the paper, which is available from the author's web-page.

Preliminaries

We assume that the reader is familiar with first-order logic and automata theory over finite and infinite words. Here, we recall the needed background in these areas and fix the notation and terminology that we use in the remainder of the text.

Words and Languages

Let Σ be an alphabet. We denote the set of all finite words over Σ by Σ * and Σ + denotes the set Σ * \ {ε}, where ε is the empty word. Σ ω is the set of all ω-words over Σ. The concatenation of words is written as juxtaposition. We write |w| for the length of w ∈ Σ * . We often write a word w ∈ Σ * of length ≥ 0 as w(0) . . . w( -1) and an ω-word α ∈ Σ ω as α(0)α(1)α(2) . . . , where w(i) and α(i) denote the ith letter of w and α, respectively.

For a language L ⊆ Σ * , the Nerode relation

∼ L ⊆ Σ * × Σ * is defined as u ∼ L v iff for all w ∈ Σ * , it holds that uw ∈ L ⇔ vw ∈ L. Analogously, for an ω-language L ⊆ Σ ω , we define ∼ L ⊆ Σ * × Σ * as u ∼ L v iff for all γ ∈ Σ ω , it holds that uγ ∈ L ⇔ vγ ∈ L.

First-order Logic

The (first-order) formulas over a signature are defined as usual: they are built from variables v 0 , v 1 , . . . , the symbol ≈ for equality, the atomic formulas over the signature, the boolean connectives ¬ and ∨, and the quantifier ∃. In this paper, we only consider signatures that consist of relation symbols. The signature, its relation symbols, and the arities of its relation symbols are always clear from the context. We write ϕ(x 1 , . . . , x r ) when at most the variables x 1 , . . . , x r occur free in the formula ϕ. The quantifier depth of a formula ϕ is recursively defined as

qd(ϕ) :=          qd(ψ) if ϕ = ¬ψ, max{qd(ψ), qd(ψ )} if ϕ = ψ ∨ ψ , 1 + qd(ψ)
if ϕ = ∃xψ, and 0 otherwise.

A (first-order) structure over a signature consists of a nonempty universe U and it associates with each relation symbol in the signature a relation over U r , where r is the arity of the relation symbol. We use R and Z to denote the structures (R, +, <) and (Z, <), respectively, where + is the ternary addition relation and < is the ordering relation over the reals or the integers, respectively.

Let A be a structure over some signature and with the universe A. For a 1 , . . . , a r ∈ A and a formula ϕ(x 1 , . . . , x r ), we write A |= ϕ[a 1 . . . , a r ] if ϕ is satisfied in A when the variable x i is interpreted as a i , for all 1 ≤ i ≤ r. For the sake of brevity, we often write x and ā instead of x 1 , . . . , x r and a 1 , . . . , a r , respectively.

Let

m, r ∈ N, ā ∈ A r and b ∈ A r . We write ā ≡ r m b if for all formulas ϕ(x 1 , . . . , x r ) with qd(ϕ) ≤ m, it holds that A |= ϕ[ā] ⇔ A |= ϕ[ b]. Note that the relation ≡ r
m partitions the elements of A r . The equivalence classes of ≡ r m can be game-theoretically characterized by socalled Ehrenfeucht-Fraïssé games. For details on these games, see, for instance, [START_REF] Ebbinghaus | Mathematical Logic[END_REF]. Instead of working directly with ≡ r m , we work with refinements of it, since the reasoning about a well-chosen refinement of ≡ r m simplifies matters. In particular, it might be difficult for ≡ r m to directly establish an upper bound on the index of ≡ r m , to identify elements ā, b ∈ A r that are in the same equivalence class, and to find a representative of an equivalence class.

Representation of Sets Definable in Real Addition

Boigelot, Jodogne, and Wolper have shown in [START_REF] Boigelot | An effective decision procedure for linear arithmetic over the integers and reals[END_REF] that every first-order definable set X ⊆ R r in R determines an ω-language L that is in the Borel class F σ ∩ G δ . In other words, L can be accepted by a so-called weak deterministic Büchi automaton. In fact, Boigelot, Jodogne, and Wolper have established in [START_REF] Boigelot | An effective decision procedure for linear arithmetic over the integers and reals[END_REF] a stronger result. First, they have proved the result for an extension of R with the additional predicate Z. Second, for a formula ϕ(x 1 , . . . , x r ) over this extended structure, they have shown how to effectively construct a weak deterministic Büchi automaton that represents the set {ā ∈ R r : R |= ϕ[ā]}.

We recall the representation of subsets of R r by ω-languages from [START_REF] Boigelot | An effective decision procedure for linear arithmetic over the integers and reals[END_REF]. In the remainder of the text, let > 1 and Σ := {0, . . . , -1} be fixed. is called the base. Let r ≥ 1. (a) V r denotes the set of all ω-words over the alphabet Σ r ∪ { } of the form v γ, where v ∈ (Σ r ) + and γ ∈ (Σ r ) ω . (b) Let v γ be an ω-word in V r with v(0) = (v 1 , . . . , v r ). The ω-word v γ represents the vector of real numbers with r components

v γ := -|v|-1 • b 1 . . . br + 0<i<|v| |v|-i-1 • v(i) + i≥0 -i-1 • γ(i)
,

where b i := v i , for 1 ≤ i ≤ r. Observe that b i = 0 if v i = 0, and b i = 1, otherwise.
Here, scalar multiplication is as usual and vector addition is componentwise. Note that we do not distinguish between vectors and tuples. (c) For a formula ϕ(x 1 , . . . , x r ), we define L(ϕ)

:= {α ∈ V r : R |= ϕ[ α ]}.
Note that the encoding v γ ∈ V 1 of a real number is based on the 's complement representation. The symbol plays the role of a decimal point, separating the integer part v from the fractional part γ. Furthermore, the first letter determines whether a "track" represents a number that is greater than or equal to 0, or a number that is less than or equal to 0. Note that the ω-words 0 0 ω and ( -1) ( -1) ω both represent the number 0, where b ω denotes the infinite repetition of the letter b ∈ Σ.

We overload the notation • by using it also for finite nonempty prefixes in V r . For v ∈ (Σ r ) + and v ∈ (Σ r ) * , we write v and v v for v 0ω and v v 0ω , respectively, where 0 denotes the vector (0, . . . , 0) ∈ Σ r .

Automata Upper Bound for the Ordering over the Integers

Before looking at the ω-languages that can be described by the first-order logic over R, we look at a simpler case. Namely, we investigate the languages that can be described by formulas over Z. We establish an exponential upper bound on the automata size for these languages. The purpose of investigating this simpler case first is twofold. First, it introduces the main concepts, which we also use in §4 for the ω-languages definable in the first-order logic over R. Second, it demonstrates the generality of the approach. The results in this section illustrate the relationship between the equivalence classes of a refinement of the equivalence relation ≡ r m and the equivalence classes of the Nerode relation of a language described by a formula ϕ(x 1 , . . . , x r ) over Z with qd(ϕ) ≤ m.

Throughout this section, formulas are over Z's signature, and m and r range over the natural numbers. We start with some definitions. For a formula ϕ(x 1 , . . . , x r ), we define the language K(ϕ) := {v ∈ (Σ r ) + : Z |= ϕ[ v ]} . We partition Z r by the equivalence relation E r m that is defined as

ā E r m b iff sign(a i -a j -c) = sign(b i -b j -c), for all c, i, j ∈ N with c ≤ m and 1 ≤ i, j ≤ r ,
where ā, b ∈ Z r , and sign(x) := 0 if x < 0 and sign(x) := 1, otherwise, for x ∈ R. Intuitively speaking, ā, b ∈ Z r are in the same equivalence class of E r m if the distances between their components are equal up to the threshold m.

Before we launch into the proof of establishing an upper bound on the size of the minimal deterministic automaton for a formula ϕ(x 1 , . . . , x r ), we give an outline: (i) We show that E r 2 qd(ϕ) refines ≡ r qd(ϕ) . (ii) We establish an upper bound on the index of E r 2 qd(ϕ) . (iii) We show that E r 2 qd(ϕ) has a congruence property with respect to word concatenation. (iv) By using (i) and (iii), we show that E r 2 qd(ϕ) determines an equivalence relation on (Σ r ) + that refines the Nerode relation ∼ K(ϕ) . Finally, from (ii) we derive an upper bound on the index of ∼ K(ϕ) . Note that the equivalence classes of ∼ K(ϕ) can be viewed as the states of the minimal deterministic finite automaton that accepts K(ϕ). The properties (i) to (iv) correspond to the Lemmas 3.1 to 3.4, respectively, which are given below. Lemma 3.2. The index of E r m is at most r! • (m + 1) r . Proof. There are at most r! many possibilities to order the r elements increasingly. If in such an ordering the distance between the ith element x and the (i + 1)st element y is greater than or equal to m, we have that sign(yxc) = 1, for all c ∈ N with c ≤ m. We obtain that the index is at most r! • (m + 1) r .

n (a i -a j ) + d i -d j -c = sign n (b i -b j ) + d i -d j -c . (3.2)
Case a ia j = 0. We have that sign(a ia j ) = 1 = sign(a ja i ). From the assumption ā E r m b, it follows that sign(a ia j ) = sign(b ib j ) and sign(a ja i ) = sign(b jb i ), and hence, b ib j = 0. Obviously, the equality (3.2) holds. Case b ib j = 0. This case is symmetric to the case a ia j = 0 above. Case a ia j = 0 and b ib j = 0. For showing (3.2), it suffices to show the equality sign a ia j +

d i -d j -c n = sign b i -b j + d i -d j -c n . (3.3)
-If m = 0, we have that c = 0 and thus

d i -d j -c n ≤ |d i -d j | n ≤ n -1 n < 1.
Since a ia j = 0 and b ib j = 0 and by the assumption ā E r 0 b, we conclude that the equality (3.3) holds. -If m > 0, we have that

d i -d j -c n ≤ |d i -d j |+|c| n ≤ n -1+|c| n ≤ m( n -1)+m n = m.
The equality (3.3) follows from the assumption ā E r m b. Lemma 3.4. Let ϕ be a formula with at most r free variables and with quantifier depth at most m. If u E r 2 m v then u ∼ K(ϕ) v, for all u, v ∈ (Σ r ) + . Proof. We prove the lemma by contraposition. Assume that u ∼ K(ϕ) v, i.e., there is a word w ∈ Σ * such that uw ∈ K(ϕ) ⇔ vw ∈ K(ϕ). It follows that uw ≡ r m vw . By Lemma 3.1, we conclude that uw E r 2 m vw does not hold. By Lemma 3.3, we obtain that u E r 2 m v does not hold. Theorem 3.5. Let ϕ be a formula. The index of ∼ K(ϕ) is at most 1 + 2 n 2 , where n is the length of the formula ϕ, i.e., ϕ consists of n symbols.

Proof. Let r be the number of free variables of ϕ and m := qd(ϕ). Note that n ≥ r + m + 1. Without loss of generality, we assume that r > 0. By Lemma 3.2, we have that the index of E r 2 m is at most r! • (2 m + 1) r ≤ 2 r 2 +rm+r ≤ 2 rn ≤ 2 n 2 . From Lemma 3.4, it follows that ∼ K(ϕ) partitions (Σ r ) + in at most 2 n 2 equivalence classes. Note that the empty word can be in an equivalence class that is distinct from all the others.

Automata Upper Bound for Real Addition

In this section, we establish an upper bound on the automata size for the first-order logic over R. The proof has a similar structure as the proof in the previous section §3. However, it is more involved. In §4.1, we define a family (F s n ) s,n∈N of equivalence relations. In §4.1 and §4.2, we show that (F s n ) s,n∈N has similar properties as the family (E s n ) s,n∈N defined in §3. Namely, (1) we show that each F r 2 2 m+2 refines ≡ r m and (2) we establish a relationship between the equivalence classes of the congruence relations determined by the definable ω-languages and equivalences classes of refinements of the equivalence relations (F s n ) s,n∈N . Finally, in §4.3, we derive the double exponential upper bound on the size of a minimal Büchi automaton that accepts the ω-language of a formula of the first-order logic over R.

In the following, formulas are always over R's signature, and r and m range over the natural numbers.

Partitioning the Reals by First-order Formulas

The results, which we use later, and their presentation of this subsection are based on Chapter 22 of Kozen's book [START_REF] Kozen | Theory of Computation[END_REF]. Since subtle modifications are made, we provide proofs in the full version of the paper. At the end of this subsection, we comment on these modifications and their implications.

An integer affine function of arity r is a function f : R r → R defined by a linear polynomial with integer coefficients, i.e., there are c 0 , . . . , c r ∈ Z such that for all x 1 , . . . , x r ∈ R, it holds that f (x 1 , . . . , x r ) = c 0 + 1≤i≤r c i x i . For such a function, f * denotes the function with f * (x 1 , . . . , x r ) = 1≤i≤r c i x i , for all x 1 , . . . , x r ∈ R r . We define ||f || := max{0, |c 1 |, . . . , |c r |}. Let A r be the set of all integer affine functions of arity r and Note that F r m decomposes R r into cells. Each such cell is described by a conjunction of linear inequations, where the absolute values of the coefficients of the inequations are bounded. Moreover, we remark that the technique that we present in the following by connecting such partitions to first-order logic and Ehrenfeucht-Fraïssé games is reminiscent of techniques in computational complexity (see [START_REF] Ferrante | The Computational Complexity of Logical Theories[END_REF]) and constraint databases (see [START_REF] Paredaens | First-order queries on finite structures over the reals[END_REF]). A novel insight is that these partitions are also connected to the relation ∼ L(ϕ) for a formula ϕ. We start with some properties about the family (F s n ) s,n∈N of equivalence relations.

σ ∩ ā, f (ā) c : f ∈ B r 2m 2 and c ∈ Z \ {0} with |c| ≤ 2m 2 = ∅ . Remark 4.6.
Before we proceed to establish the upper bound on the size of the minimal automata representation for the set defined by a formula ϕ, we point out the differences between the family (F s n ) s,n∈N of equivalence relations and the family of equivalence relations defined in Kozen's book [START_REF] Kozen | Theory of Computation[END_REF] in Chapter 22.

In Kozen's book, two elements ā, b ∈ R r are related iff sgn(f (ā)) = sgn(f ( b)), for all integer affine function f ∈ A r with ||f || ≤ m and |f ( 0)| ≤ m. Here, sgn denotes the signum function that is defined as sgn(x) := -1 if x < 0, sgn(x) := 1 if x > 0, and sgn(0) := 0.

There are two differences to our definition. First, we use the function sign instead of the function sgn. This difference is actually irrelevant. Using sign instead of sgn in the definition in Kozen's book would not change the equivalence relations. However, we found the reasoning in the proofs when using the function sign slightly simpler. Second and more relevant, we require |f ( 0)| ≤ rm instead of |f ( 0)| ≤ m. The proofs of the Lemmas 4.2 to 4.5 follow the lines of the proofs of the corresponding lemmas in Kozen's book. However, there are subtle differences, e.g., in Lemma 4.5, we have the special case for m = 1, which is not needed in the corresponding lemma in Kozen's book.

An immediate consequence of only requiring this weaker restriction on the functions f ∈ A r is that the equivalence relation F r m refines the corresponding equivalence relation as defined in Kozen's book. The purpose for having finer equivalence relations is the following: For a formula ϕ(x 1 , . . . , x r ), we show in §4.2 that the equivalence classes of ∼ L(ϕ) are related to the equivalence classes of a certain relation in the family (F s n ) s,n∈N . Without the weaker requirement we were not able to establish a similar relationship. The problem can be pinpointed to Lemma 4.8, which is crucial in relating the equivalence relations. The corresponding statement of Lemma 4.8 would not be correct when using the equivalence relations as defined in Kozen's book.

Relationship to Languages

In this subsection, we establish a relationship between the equivalence relation F r 2 2 m+2 +1 and the congruence relation ∼ L(ϕ) , where ϕ(x 1 , . . . , x r ) is a formula with qd(ϕ) ≤ m. Namely, we show that F r 2 2 m+2 +1 determines a refinement of the congruence relation ∼ L(ϕ) . We start with a technical lemma. Its proof is straightforward and we therefore omit it. In the following, we will use it without explicitly referring to it. Lemma 4.7. For f ∈ A r , u ∈ (Σ r ) + , u ∈ (Σ r ) * , and γ ∈ (Σ r ) ω , the following facts hold: [START_REF] Bardin | FAST: Fast acceleration of symbolic transition systems[END_REF]

f ( uu ) = f ( 0) + |u | f * ( u ) + f * ( 0u ), and (2) f ( u u γ ) = f ( 0) + f * ( u u ) + -|u | f * ( 0 γ ).
The next two lemmas show that the equivalence relations in the family (F s n ) s,n∈N have congruence properties on words with respect to word concatenation and show how their equivalence classes relate to the equivalence classes of the congruence relation ∼ L(ϕ) . We want to point out a technical detail, which is reflected in the (b)-parts of the lemmas, is illustrated by the following example. The words u u and u u 0 represent the same vector of real numbers, i.e., u u = u u 0 . Therefore, u u and u u 0 represent the same equivalence class in F r m . However, u u and u u 0 might not be in the same equivalence class with respect to ∼ L(ϕ) . Observe that appending an ω-word γ ∈ (Σ r ) ω to u u and u u 0 may yield representations of different vectors of real numbers, i.e., u u γ = u u 0γ , and u u γ and u u 0γ may represent different equivalence classes in F r m . Lemma 4.8. For all u, v ∈ (Σ r ) + and u , v ∈ (Σ r ) * , the following two facts hold:

(a) If u F r m v then for all w ∈ (Σ r ) * , uw F r m vw . (b) If u u F r 2m v v and |u | ≥ |v | then for all γ ∈ (Σ r ) ω , u u γ F r m v v 0k γ with k = min{|u | -|v |} ∪ {k ∈ Z : k ≥ rm}.
Proof. For r = 0, there is nothing to prove. In the following, we assume that r > 0. (a) We prove (a) by contraposition. Assume that for some w ∈ (Σ r ) * , it is not the case that uw F r m vw , i.e., there is some f ∈ B r m with sign(f ( uw )) = sign(f ( vw )). Without loss of generality, we assume that f ( uw ) < 0 and hence f ( vw ) ≥ 0. The other cases can be reduced to this case by using the function g ∈ B r m with g(x) = -f (x), for all x ∈ R r . We have that |w| f * ( u -If f * ( v ) < -rm, we obtain a contradiction to the assumption f ( vw ) ≥ 0, since

) + f ( 0w ) < 0 and |w| f * ( v ) + f ( 0w ) ≥ 0. Obviously, it must hold that f * ( u ) = f * ( v ). If sign(f * ( u )) = sign(f * ( v )) then u F r m v
|w| f * ( v ) + f ( 0w ) = |w| f * ( v ) + f * ( 0w ) + f ( 0) < -|w| rm + ( |w| -1)rm + rm ≤ 0 .
-If f * ( v ) > rm, we conclude that f * ( u ) > rm. Analogously, as in the above case, we obtain a contradiction to the assumption f ( uw ) < 0. (b) Let f be an arbitrary function in B r m and γ ∈ (Σ r ) ω . We have to show that sign(f

( u u γ )) = sign(f ( v v 0k γ )). Since B r m ⊆ B r 2m , it follows from the assumption u u F r 2m v v that sign(f ( u u )) = sign(f ( v v )). That means, either (1) f ( u u ), f ( v v ) < 0 or (2) f ( u u ), f ( v v ) ≥
0 holds. Since the case (1) can be reduced to the case (2) by considering the function g(x) = -f (x), for all x ∈ R r , we restrict ourselves to [START_REF] Bardin | FAST extended release[END_REF].

For the sake of readability, we use the abbreviations a := f * ( u u ), b := f * ( v v ), and c := f * ( 0 γ ). Note that

f ( u u γ ) = f ( 0) + a + c -|u | and f ( v v 0k γ ) = f ( 0) + b + c -|v |-k . ( 4
(f ( u u γ )) = sign(f ( v v 0k γ )) = 0. So, we also assume that |c| • -|u | ≤ f ( 0) + a. Observe that f ( u u γ ) ≥ 0. Furthermore, observe that f ( 0) + b ≥ -|v | . We have that f ( v v 0k γ ) ≥ 1 |v | + c |v |+k = k -|c| |v |+k ≥ rm-rm |v |+k ≥ 0.
Lemma 4.9. Let ϕ(x 1 , . . . , x r ) be a formula with qd(ϕ) ≤ m. For all u, v ∈ (Σ r ) + and u , v ∈ (Σ r ) * , the following two facts hold:

(a) If u F r 2 2 m+2 +1 v then u ∼ L(ϕ) v. (b) If u u F r 2 2 m+2 +1 v v and |u | ≥ |v | then u u ∼ L(ϕ) v v 0k with k = min{|u | - |v |} ∪ {k ∈ Z : k ≥ rm}.
Proof. We only show (a). The proof for (b) is analogous and we omit it. From Lemma 4.8(a), it follows that uw F r 2 2 m+2 +1 vw , for all w ∈ (Σ r ) * . With Lemma 4.8(b), we obtain that uw γ F r 2 2 m+2 vw γ , for all w ∈ (Σ r ) * and γ ∈ (Σ r ) ω . By Lemma 4.3, we conclude that uw γ ≡ r m vw γ , for all w ∈ (Σ r ) * and γ ∈ (Σ r ) ω . In particular, we have that uw γ ∈ L(ϕ) ⇔ vw γ ∈ L(ϕ), for all w ∈ (Σ r ) * and γ ∈ (Σ r ) ω . From this it follows that u ∼ L(ϕ) v, since for any ω-word α not in V r , we have that uα, vα ∈ L(ϕ).

Upper Bounds

We establish an upper bound on the index of F r m , from which we then derive an upper bound on the automata size. We start with a simple lemma.

Lemma 4.10. The cardinality of B r m is at most (2rm + 1)(2m + 1) r . Using the Lemmas 4.4, 4.5, and 4.10, we establish an upper bound on the index of F r m . Lemma 4.11. The index of F r m is at most max{1, m 2 3+r • 2 2 3+r }. Theorem 4.12. Let ϕ be a formula. The index of ∼ L(ϕ) is at most 2 2 8+n , where n is the length of the formula ϕ, i.e., the number of symbols of ϕ.

Proof. Let r be the number of free variables in ϕ and m := qd(ϕ). We use F r 2 2 m+2 +1 to define a refinement R of ∼ L(ϕ) . First, the singleton {ε} is an equivalence class of R. Second, the set of words with at least two occurrences of the letter is another equivalence class of R. The equivalence class of a word v ∈

(Σ r ) + of R is {u ∈ (Σ r ) + : v F r 2 2 m+2 +1 u }. It remains to define the equivalence classes of R on F := {v v : v ∈ (Σ r ) + and v ∈ (Σ r ) * }. For v v ∈ F , let S := {u u ∈ F : v v F r 2 2 m+2 +1 u u }. R chops S into equivalence classes, assuming |v | ≤ |u |, for all u u ∈ S: -For k ∈ {0, . . . , log r2 2 m+2 +1 -1}, the equivalence class of v v 0k of R is {u u ∈ S : |u | = |v | + k}. -For k = log r2 2 m+2 +1 , the equivalence class of v v 0k of R is {u u ∈ S : |u | ≥ |v |+k}.
Note that any word u u ∈ S relates to exactly one word v v 0k .

With Lemma 4.9 at hand, it is easy to see that R refines ∼ L(ϕ) . It remains to prove an upper bound on the index of R. Note that n ≥ m + r ≥ 1. By Lemma 4.11, an upper bound on the index of F r 2 2 m+2 +1 is 2 2 m+2 +1 2 3+r

• 2 2 3+r = 2 2 m+2 •2 3+r +2 3+r +2 3+r = 2 2 5+r+m +2 4+r ≤ 2 2 6+n .

Hence, R partitions (Σ r ) + into at most 2 2 6+n equivalence classes and F is partitioned into at most 2 2 6+n • log r2 2 m+2 +1 ≥ 2 2 6+n • r(2 m+2 + 1) ≥ 2 2 6+n • 2 3+n ≥ 2 2 7+n equivalence classes. From this, we derive the upper bound 2 2 8+n on R's index.

Remark 4.13. Since for any formula ϕ, L(ϕ) is an ω-language in the Borel class F σ ∩G δ [START_REF] Boigelot | An effective decision procedure for linear arithmetic over the integers and reals[END_REF], we can-similar to deterministic finite automata-view the equivalence classes of ∼ L(ϕ) as the states of a minimal deterministic Büchi automaton that accepts L(ϕ). For further details, see [START_REF] Maler | On syntactic congruences for omega-languages[END_REF] and [START_REF] Löding | Efficient minimization of deterministic weak ω-automata[END_REF]. Thus, Theorem 4.12 establishes a double exponential upper bound with respect to the formula length on the size of the minimal number of states of any Büchi automaton that accepts L(ϕ).

Remark 4.14. The double exponential upper bound on the automata size is tight, i.e., there is a family of formulas (ϕ n ) n∈N such that for each n ∈ N, the length of ϕ n is linear in n and the index of ∼ L(ϕn) is double exponential in n. An analogous result with a similar proof has already been shown in [START_REF] Klaedtke | On the automata size for Presburger arithmetic[END_REF] for Presburger arithmetic.

Conclusion

This papers presented a new method to reason about the sizes of automata that represent first-order definable sets of automatic structures. The method consists of identifying a relationship between the states of a minimal deterministic automaton for a formula and the equivalence classes of a refinement of the equivalence relation determined by Ehrenfeucht-Fraïssé games. We applied the presented method to establish tight upper bounds on the minimal sizes of automata that represent sets definable in FO(Z, <) and FO(R, +, <). For FO(R, +, <), previously proposed techniques based on quantifier-elimination methods [START_REF] Klaedtke | On the automata size for Presburger arithmetic[END_REF] failed to establish a double exponential upper bound on the automata size.

As future work, we want to investigate how, and to what extent, the upper bounds on the automata sizes depend on how elements of a structure are encoded as words. The word encoding of integers and reals that we have used in this paper is based on the 's complement representation, for some ∈ N with ≥ 2. There are various other word encodings of numbers so that, e.g., FO(Z, <) admits an automata-based decision procedure. For a study on the impact of encodings in automatic structures, see, e.g., [START_REF] Khoussainov | Definability and regularity in automatic structures[END_REF]. We also plan to apply the presented technique to establish further upper bounds on automata sizes for other automatic structures and use it to simplify the proofs of previously established upper bounds. For instance, for Presburger arithmetic, we expect that we can use equivalence relations similar to the ones used in this paper for FO(R, +, <). However, we have to adjust the bounds on the coefficients and take the definable divisibility relations into account.

Lemma 3 . 1 .

 31 The equivalence relation E r 2 m refines the equivalence relation ≡ r m . That means, ā E r 2 m b implies ā ≡ r m b, for all ā, b ∈ Z r . To prove Lemma 3.1, we apply a standard technique from model theory. First, we show that the family (E s n ) s,n∈N of equivalence relations has the following property: If ā E r 2 m+1 b then for every a ∈ Z, there is some b ∈ Z such that (ā, a ) E r+1 2 m ( b, b ). (3.1) Properties of this kind are often called back-and-forth properties in the literature. Note that E r 2 m+1 is symmetric. Second, we complete the proof by an induction over m, where we use the property (3.1) in the induction step for the existential quantifier.

Lemma 3 . 3 .

 33 Let u, v ∈ (Σ r ) + . If u E r m v then uw E r m vw , for all w ∈ (Σ r ) * . Proof. Let n := |w|, ā := (a 1 , . . . , a r ) := u , b := (b 1 , . . . , b r ) := v , and d := (d 1 . . . , d r ) := 0w . We have that uw = n ā + d and vw = n b + d. Furthermore, it holds that d i < n , for all i ∈ {1, . . . , r}. Let i, j, c ∈ N with 1 ≤ i, j ≤ r and c ≤ m. We have to show that sign

  B r m := f ∈ A r : ||f || ≤ m and |f ( 0)| ≤ rm . Definition 4.1. We partition R r by the equivalence relation F r m that is defined as ā F r m b iff for all f ∈ B r m , sign(f (ā)) = sign(f ( b)) , where ā, b ∈ R r .

Lemma 4 . 2 . 2 . 4 . 3 .

 42243 Let ā, b ∈ R r . If ā F r 4m 2 b then for all a ∈ R, there is some b ∈ R such that (ā, a ) F r+1 m ( b, b). Similar to Lemma 3.1, we obtain the following lemma by using Lemma 4.Lemma For all ā, b ∈ R r , it holds that if ā F r 2 2 m+2 b then ā ≡ r m b.The following two lemmas show how to obtain a set R ⊆ R r such that each equivalence class of F r m has at least one representative in R. Let σ be an equivalence class of F r m and let σ be an equivalence class of F r+1 n , where n ∈ N. We say that σ is consistent with σ if (σ × R) ∩ σ = ∅.

Lemma 4 . 4 .

 44 For each equivalence class σ of F 1 m , we have that σ ∩ d c : c, d ∈ Z with c = 0 and |c|, |d| ≤ 2m 2 = ∅ . Lemma 4.5. Let r > 1, ā ∈ R r , where σ is the equivalence class of ā with respect to F r 2m 2 . For every equivalence class σ of F r+1 m that is consistent with σ, we have that σ ∩ ā, f (ā)+d c : f ∈ B r 2 and c, d ∈ Z \ {0} with |c| ≤ 2, and |d| < 2 = ∅ if m = 1, and, for m = 1, we have that

  does not hold and we are done. So, assume that sign(f * ( u )) = sign(f * ( v )). If |f * ( u )| ≤ rm or |f * ( v )| ≤ rm then we are also done by choosing an appropriate function g ∈ B r m with sign(g( u )) = sign(g( v )). So, assume that |f * ( u )|, |f * ( v )| > rm. Note that |f * ( 0w )| ≤ ( |w| -1)rm.

. 1 )

 1 If c ≥ 0 then sign(f ( u u γ )) = sign(f ( v v 0k γ )) = 1. In the following, assume c < 0.Case a = b. With the assumption u u F r 2m v v we conclude that a, b > 2rm. Note that |f * ( 0 α )| ≤ rm, for all α ∈ (Σ r ) ω . It follows that f * ( u u γ ) = a + c -|u | > 2rmrm ≥ rm . The reasoning for f * ( v v 0k γ ) > rm is similar. Since |f ( 0)| ≤ rm, we have that sign(f ( u u γ )) = sign(f ( v v 0k γ )) = 1.Case a = b. For k = |u | -|v |, it immediately follows from the equalities in (4.1) that f ( u u γ ) = f ( v v 0k γ ), and hence sign(f ( u u γ )) = sign(f ( v v 0k γ )). For a = b = -f ( 0), it is also straightforward to see from the two equalities in (4.1) that sign(f ( u u γ )) = sign(f ( v v 0k γ )). For the rest of the proof, assume k = min{k ∈ Z : k ≥ rm} and b = -f ( 0). Moreover, for |c| • -|u | > f ( 0) + a, it follows directly from the equalities (4.1) that sign

This work is licensed under the Creative Commons Attribution-NoDerivs License. To view a copy of this license, visit http://creativecommons.org/licenses/by-nd/3.0/.

Acknowledgments. The author thanks David Basin, Cas Cremers, Matthias Schmalz, and the anonymous reviewers for their comments on earlier versions of the paper.

This work was supported by the Swiss National Science Foundation (SNF).

c F. Klaedtke