Claude Hammecker

The Importance of the Petrophysical Properties and External Factors in the Stone Decay on Monuments

Keywords: Salt crystallisation, capillary imbibition kinetics, evaporation, water activity, unsaturated porous media

In this paper it is proposed to quantify the importance of some physical parameters responsible for stone decay on monuments. The most common decay process is the crystallisation of salt near the surface of the rocks or inside their porous network. Therefore, the water balance in rocks submitted to these special saturation and position conditions has been studied specifically, using the general concepts of water transfer in unsaturated porous media, and using the capillary imbibition kinetics of different rocks. Different parameters have been taken into account for the calculation of the salt crystallisation position: on one hand, several external parameters such as relative humidity, air convection and the presence of solute in solution, and on the other hand, the intrinsic water transfer properties of the rocks. Their relative importance is discussed, considering the potential values that each parameter can reach in nature.

Introduction

The rocks used on buildings are subjected to several types of decay processes [START_REF] Amoroso | Stone Decay and Conservation[END_REF]): physical, chemical, or microbiological, etc. Nevertheless, considering the kinetics and extension of the decay processes of rocks on monuments, it is admitted that the most important factors are physical. Except for the dissolution of carbonate rocks in leached areas, no genuine mineralogical alteration is observed. Rocks are however affected by mechanical desegregation and superficial modifications which are mainly due to frost and salt crystallisation [START_REF] Winkler | Crystallization Pressure of Salts in Stone and Concrete[END_REF]. This paper is especially focused on the study of this latter process, which affects stones in all types of climates. The water balance in stones that determines the crystallisation of salts has been calculated versus different parameters: external, such as relative humidity, wind velocity and the presence of Centre de G6ochimie de la Surface (CNRS), 67084 Strasbourg Cedex, France. 2 Present address: ORSTOM, BP 1386, Dakar, Senegal. PAGEOPH, salts in solution, and internal, such as the intrinsic water transfer properties of the stones. In this paper only isothermal conditions have been taken into account.

General Context

The rocks on monuments often show several types of decay morphologies depending on their petrographical characteristics, on their position on the monument, and on the type of salts involved [START_REF] Jeannette | Importance des structures de porositk dans l'altOration des pierres des monuments, Coll. S6dimentologie et Gaochimie de la Surface[END_REF]. The most common salt occurrence on monuments, especially in urban areas, is gypsum resulting from the reaction of H2SO 4 with calcite present either in the rocks or in the surrounding mortars. Gypsum may form superficial black crusts on the surface of stones or it can also lead to contour scaling as it crystallises inside the porous network of the rocks. The crust formation, at least in the first stages, is not damaging to the rock, whereas the crystallisation of gypsum at a few millimetres or sometimes centimetres underneath the surface of the stone, can provoke the breakdown of the external part, which is lightly impregnated with gypsum (ZEHNDER, 1982).

Other types of salts, usually more soluble: halite (NaC1), niter (KNO3), thenardite (Na2SO4), mirabilite (NaaSO 4 -10H20), syngenite (K2Ca(SO4) 2 -H20), etc., are also commonly found on monuments [START_REF] Arnold | Behaviour of Some Soluble Salts in Stone Deterioration, 2nd Internat. Syrup. on the Deterioration of Building Stones[END_REF]. They form salt efflorescence on the surface of the stone such as the niter crystals which frequently cover the walls in cellars, or they may also develop efflorescence on previous superficial gypsum crusts. However these kinds of salts can also be associated with desegregation and alveolization of stone on monuments (HAMMECKER and JEAN-NEOn'E, 1988). In the lower part of buildings, submitted to capillary rise of water, soluble salts sometimes crystallise in the porous network of the stones, provoking internal stress and desegregation.

The description of these decay mechanisms can be simplified by considering two extreme conditions: either salts crystallise on the surface of the rocks, without really damaging them, or they crystallise in the rocks causing actual decay [START_REF] Amoroso | Stone Decay and Conservation[END_REF][START_REF] Jeannette | La conservation de/a pierre monumentale en France[END_REF]. As the position of salts crystallisation is governed by water balance in rocks, this study centres more specifically on the water transfer processes in unsaturated porous media.

Water Transfer Processes

Two different conditions are usually observed for the transfer of water through the rocks on monuments: 1--alternate imbibition and drying in rain-exposed positions on monuments, 2--simultaneous water supply by capillary imbibition and loss by evaporation (steady state, wick condition), in the lower part of the buildings submitted to capillary rise [START_REF] Hammecker | Importance des transferts d'eau dans la d@radation des pierres en oeuvre[END_REF].

Experiments

Capillary imbibition, and evaporation kinetics can be measured experimentally on rock samples. Usually cylindrical cores of 4 cm in diameter and 10 to 15 cm in height are used for these experiments.

I. I Capillary imbibition kinetics

The previous oven-dried (60~ rock samples are placed on a thick wet filter paper, providing a continuous and regular water supply. This apparatus is enclosed in a tight container in order to prevent evaporation.

The height of the wetted fringe and the weight of the sample are recorded for increasing time intervals. When plotted versus the square root of time, both show a linear evolution (Figure la). Hence two kinetic parameters can be measured:

;.5~[kg/(v/s " m2)] = V~/(S ~)
For homogeneous porous media: ~d/(~.p)= N,, where N, is the porosity freely invaded by capillary imbibition, and p the fluid density (kg/m3). Nevertheless these kinetic parameters can be defined as easily, only if the effect of gravity is negligible: with very fine pores or for low capillary rise distances or in the case of horizontal capillary flow. Considering the conditions of stone decay on monuments, in this paper gravity has been neglected. Moreover, in this paper d is expressed in cm/x~ for convenience despite being used in SI unit in the calculations (SI = [cm -h -I/2]/6000).

Evaporation kinetics

Water-saturated rock samples are wrapped in polyethylene sheath with an open and regular surface, through which evaporation is allowed. The samples are placed in closed containers where saturated brines control the relative humidity [START_REF] Acheson | Vapor Pressure of Saturated Aqueous Salt Solutions. Humidity and Moisture[END_REF]SCHLONDER, 1963;WYLIe, 1963). Thereafter the weight is recorded regularly. As shown in Figure lb, two stages with different kinetics can be observed. The first stage of drying, corresponding to the superficial evaporation of water, is linear versus time. Water is drawn by capillary forces from the inner parts of the porous network toward the surface [START_REF] Pearse | The Mechanisms of Drying of Solids: L The Forces giving Rise to Movement of Water in Granular Beds during D;2ving[END_REF]HALLAIRE and H~NIN, 1958). A constant rate of evaporation can be measured:

W/S qc~--- -GP, (1)
t where q~ is the volumic flow rate. When the first stage of drying ends, the critical water saturation is reached 0,. at t = t(Oc).

The second stage of drying, with a much slower rate of evaporation, corresponds to the diffusion of water vapour inside the porous network toward the surface. Liquid water is immobile during this stage of drying because pendular saturation has been reached or because the capillary pressures are not high enough to pull water at the surface [START_REF] Pearse | The Mechanisms of Drying of Solids: L The Forces giving Rise to Movement of Water in Granular Beds during D;2ving[END_REF]BOND and WILLIS, 1969). The rate (2)

In the case of stone degradation on monuments, the most favourable case is reached when the major part of the porous volume is desaturated by superficial evaporation (0c-~ 0). Hence if salt crystatlisation occurs, it mainly takes place on the surface of the rock, without damaging its coherence.

Transfer in Unsaturated Porous Media

Water transfer in unsaturated conditions is governed by both the relative permeability (or hydraulic conductivity) K(~) and the matrix potential ~, referring to capillary pressure and gravitational components. The flow is described by the generalised Darcy law in one direction (x) q = -K(0)v0

(3) d0 q = -K(0) dxx (4) mass conservation expressed in the continuity law, determines the evolution of the water content 0: 00 0qx

- (5) 0t 3x
The introdution of the diffusivity D(O) = K(O).(dtp/dO) simplifies the mathematical treatment of the equations ( 4) and ( 6) for unsaturated flow (C~ILDS and COLLIS-GEORGE, 1950): (8)

00 q = -D(O) ~- (7)
The solution for this diffusion-like flow equation can either be calculated numerically or semi-analytical solutions are proposed for given initial and limit conditions. Diffusivity is usually expressed by the empirical relation of GARDNER and MAY-HUGH (1958):

D(O) = D i exp(fi(0 -0i)) = D~ exp(fi(0a -0)), ( 9
)
where Di is the diffusivity for the initial water content 0i, D~ the diffusivity for air-dry water content 0a, and fi an empirical constant. The water content profile can be calculated at any moment during the drying of a rock sample. Nevertheless, the most important moment occurs when superficial evaporation ceases and the critical water content is reached. GARDNER and HILLEL (1962), give an approximate analytical solution for this case. The following initial and limit conditions must be respected during the first stage of drying: For a core with a length L:

0=0~, x>0, t=0 (
Claude Hammecker PAGEOPH, 80 qv (11) 8t L

Taking into account the conditions (a), (b) and (c), and deriving twice, the following equation is obtained:

x 2

The duration of the first stage of drying can be calculated from the average water content 0-(SWARTZENDRUBER, 1969):

t(Oc) =1. (0,-0-) (13) qv with b2 ,/b2+15 0-= Oc = -2 9 fi + ~--m~,b~ 1_ 1 ~ (14) b2 = ,/(bl + 1)/b, b, = ft. L . qv/(2 . Di).
The evolution of the different parameters governing the superficial evaporation of water such as the data related to diffusivity (Di and fi) and the external rate of evaporation (G), is shown in Figure 2.

Simultaneous Evaporation and Water Supply

In the case of wick-like water transfer conditions, the steady-state equilibrium is reached when capillary imbibition flow is equal to the evaporation flow. As the critical position for salt crystallisation is the surface (z = 0) it is important to know the total water balance Q at this position

Q(o,o = qc -qe, ( 15
)
which is the algebraic sum of the capillary imbibition (qc) and the evaporation (qe) flOWS.

Capillary imbibition

Taking the cylindrical tube model described by the WASHBURN law (1921), the imbibition kinetics can be calculated versus a hypothetical hydraulic radius ....

. (18)

q" P d7 =p 2-y Considering a cylindrical tube partially filled with water, the evaporation flow can be expressed as a function of: the isothermal rate of diffusion for water vapour in pure air 9, the difference in water vapour concentration between air near the water and the bulk air volume outside the tube (c o -c~), and the distance between the meniscus and the tube end h: qe = _@. c0-cl (19) h Nevertheless this relation deriving from F~CK'S first law, cannot apply directly to diffusion in a mixture of air and water vapour. DE GROOT and MAZUR (1962) introduced a mixing term in equation ( 19) and expressed it as a function of partial water vapour pressure

M

P~ dp qe = --9 R. r(P--p,)dx' (20) where P is the atmospheric pressure, Pr the reference pressure (1.013 -10-5 Pa), Pt the fixed water vapour pressure, M the molecular mass of water (1.8.10 .2 kg/mol), R the universal gas constant, and T (K) the temperature. For simplification qe =k'P~ (21) h DE VR~ES and KRUGER (1967) give an empirical relation for k which in SI units is 1.013. 10 5 M ( T ']~.s8 kEsl=--2"17' l0 5 (P--p~) R--T\273~.15] " (22) In order to avoid the indetermination of equations ( 19) and ( 21) when: limh~0 qe = C~, a supplemental parameter depending on air convection e must be added [START_REF] Jouany | Transfert d'eau par kvaporation dans les milieux argileux[END_REF]

' qe =k'P~ (23) h+8
The value of e is obtained experimentally by measuring the evaporation flow on the free water surface (h =0), submitted to the same evaporating conditions (k, po-pl). Hence e represents the thickness of the layer of air over the water surface, in which p~ <p < Po (Figure 3). When air convection increases, e decreases. In a cylindrical tube the evaporation flux is also

dx q~ = tit p' ( 24
)
where p is the water density. Hence

(x +~).dx=y.(h2-xZ)+e.h+g.h+e. Xoo P

In this case, only the positive solution of this second-order equation, is considered

•/ / x 2. k . (Po -Pl) h = -~+ 2+~2q -(t-to), (26)
P where x 0 is the initial height of the meniscus. When air convection is important, e can be neglected, hence the kinetic of migration of the meniscus is the function of the square root of time. This phenomenon is then comparable to the kinetic of the second stage of drying of rocks (q*).

~Vater balance

Although the structure of the porous media in rocks cannot be compared to cylindrical tubes, the imbibition and evaporation kinetics are similar and easily PAGEOPH, calculated with this model. The steady-state equilibrium is reached for lO "--qc=qc ,~2

(Po --Pl =k"

2"y

L+e-y

The equilibrium position is In Figure 4 the evolution of equilibrium height feq is plotted versus different parameters, such as the capillary imbibition kinetic N, the "wind velocity" e, the relative humidity P/Po and the length of the capillary tube L.

(L + s) ' ~2. p Y*q = 2 " k . (Po--Pl) +( N'2 P)' (27) (28)

The Presence of Salts

In nature, and especially on monuments, the rocks do not contain distilled water but rather solutions which form brines by concentrating under evaporation and finally form salts. The presence of ions, especially near the surface where they are concentrated by the evaporation of water, may influence the water activity a~,,. As the evaporation rate depends on the partial water vapour pressure gradient, the modification of the water activity and the partial vapour pressure just above the water surface will alter the water balance in the rock:

q~v =k .PS-Pl h ' ( 30
)
where p~ = a,, "Po. The evolution of water activity depends on the concentration and the type of ions. In order to calculate the water activity in the presence of ions, the ionic interaction model of PITZER (1973,1979) has been chosen, rather than DEBYE-HUCKEL 'S model (1923), because of the high ionic strengths in the brines (I > 1), which are necessary for the crystallisation of the previously mentioned soluble salts. Hence for a given type of salt and molality the water activity can be calculated (Appendices A1 and A2). Nevertheless the main problem is the calculation of the evolution of the ion concentration at the air-solution interface. In order to solve this problem two cases have been taken into account:

No chemical diffusion: Considering that the diffusion of ions in solution is slow compared to water transfer processes, space under the meniscus has been divided into layers of determined thickness 2 (Fig. 5a). In this study an arbitrary thickness of 10 #m has been chosen, because it represents the main salt-crystal size observed on monuments. When 10 #m of water at the top of the meniscus evaporates, the ions remain in the water layer previously situated underneath.

Hence concentration in the upper layer situated underneath the meniscus evolves as follows:

to, Co tube (Fig. 5b):

C(to) = v(O-' ) c(O-' ) ,
(32) v(0 ,)-qev t where V(ty) = V(tj_l) + (qoap-qev)' t. TO solve this system, numerical resolution has been used in order to relate the height of the meniscus in the tube, the global flow, and the concentration. Equilibrium height is obtained by incrementing dx, calculated from the capillary imbibition and evaporating flux at each new position x and new concentration, hence p* : (34)

To perform this calculation, a small increment of time (dr = 100 s) has been chosen. In order to simplify the calculation, only aqueous solutions of some binary salts have been tested. Nevertheless these salts have been chosen for their possibility to crystallise in rocks on monuments, and in order to cover a wide range of water activity in the corresponding saturated brines (Appendix A3). The results displayed in Figure 6 can be described as follows: 9 as the concentration of the solution near the interface evolves faster with the no chemical diffusion model than with the instant chemical diffusion model, the calculated equilibrium heights heq are slightly higher with the first model than with the latter. Nevertheless both models converge toward the same tendencies. 9 The initial concentration of the solution Co is an important factor governing the equilibrium height: an aqueous solution with a high concentration pro-PAGEOPH, motes the hydrodynamical equilibrium position to be nearer the surface than with a dilute solution. 9 Equilibrium height depends on the initial position of the meniscus: in these chosen conditions, for upward flow (x 0 = 0 cm), heq is higher than for the downward flow (x0 = 20 cm). 9 The influence of the most soluble salts such as NaC1, Na2SO 4 . 10H20 or KC1 is considerably more important than for less soluble salts like CaCO 3 or CaSO2.2H20. 9 The influence of the capillary imbibition kinetic is predominant over the other parameters because moderate variations for ~) lead to important variations for heq.

Discussion

The Models

It must be borne in mind that the mathematical models used for this study are based on several assumptions constraining their application. The concept of diffusivity in the CHmDS and COLLIS-GEORGE equation assumes an initial uniform water profile in the stone which implies a homogeneous nonstratified porous medium. Moreover, the use of diffusivity is valid only in nonhysteretic porous media free of any temperature gradient (HmLEL, 1971). These conditions are realised with the sample in the laboratory where water profile, sample homogeneity and internal temperature gradient are precisely controlled. In the case of hysteretic rock samples, as only evaporation is considered, diffusivity is calculated by taking into account the drainage branch of the hysteresis in the capillary pressure curve (~ -0). The CHmDS and COLLIS-GEORGE equation is validated for these conditions for which the importance of elemental external parameters has been tested. As the purpose of this study is to quantify the influence of some internal and external parameters on the water transfer processes governing the rock decay, and not to describe the entire and complex system of rocks on monuments, the use of these equations is justified.

On the other hand, the validity of the WASHBURN equation ( 16) is restrained to the capillary imbibition into straight cylindrical tubes. Obviously, the geometry of the porous network in natural rocks is dissimilar to this simple model. However, based on this equation, some authors extended its application to less monotonous pore shapes [START_REF] Szekely | The Rate of Capillary Penetration and the Applicability of the Washburn Equation[END_REF][START_REF] Dullien | Porous Media Fluid Transport and Pore Structure[END_REF]LEV~NE, et al., 1980;HAM MECKER et al., 1993). In any case, the capillary imbibition kinetic described by these models and the experimental data, are similar to the Washburn equation, despite the hydraulic radius (r) in the latter having no physical reality. Hence, for this study, based on water transfer processes, the use of this equation is satisfactory.

The Results

Many parameters govern the water balance in rocks and consequently the position of potential salt crystallisation. However, considering that this entire study has been performed in ideal isothermal conditions, the most influential external parameter is certainly the air convection or wind velocity formulated by e whereas relative humidity has less important effects.

Nevertheless, it is clear that in the case of simple drying, the internal parameters related to the diffusivity such as Di and /~, are more important in determining the critical water content 0 C than the external rate of evaporation (qc,). Considering that some of the highest potential evaporation rates measured in arid inhabited areas (Agadez, Niger), are about 2.4 cm/day [START_REF] Brunel | Evaporation des nappes d'eau libres en Afrique Sahelienne et Tropicale[END_REF], their influence on critical water content are negligible compared to the diffusivity. On the other hand, the potential range of diffusivity for different rocks used on monuments is very wide. The results shown in Table 1 for some common sedimentary rocks used on monuments are very explicit, because their diffusivity (Da and D;) are seen to range over four orders of magnitude. More generally their petrophysical properties, can show severe differences. Despite the average grain size varying widely (20-750 #m), it is not a determining factor for the petrophysical properties such as porosity (N~), saturated hydraulic conductivity (Ko), or capillary kinetic imbibition. The coarsest rock (Gueberschwihr sandstone) is at the same time the less porous and the Jess permeable, whereas the finest rock (Laspra limestone) is more porous and 1000 times more permeable than the former. The important secondary silicification features present in the Gueberschwihr sandstone are responsible for these petrophysical parameters. As observed on the mercury porosimetry curves (Fig. 7), half of the porous volume of this sandstone is connected through necks narrower than 0.1 #m, whereas in the other rocks, including the micrite, the pore threshold shows far higher interconnection sizes. The saturated hydraulic conductivity and diffusivity values of these rocks are coherent with the corresponding pore size distributions.

For high diffusivity, regardless of the external evaporation conditions, the critical water content (0c/0i ~ 0) is very low, which means that evaporation preferentially takes place on the surface of the rock. On the other hand, for very low diffusivity, evaporation occurs mainly inside the porous network of the rock (Oc,/Oi ~ 1). External conditions influence the evaporation of water in a rock only for intermediate diffusivity values.

In the wick-like conditions, the influence of the capillary imbibition kinetic N is predominant, because very slight variations for ~ lead to an important alteration in the hydrodynamical equilibrium position (heq). As shown in Table 1, the variation of this coefficient is also important in sedimentary rocks. It is monitored by the pore size distribution determined by mercury porosimetry. Nevertheless, depending on petrographical features, such as clayey coating, or superficial rugosity on grains, in some cases the specific surface area can provide better information on the capillary imbibition kinetic (HAMMECKER and JEANNETTE, 1995).

Considering the presence of salts in solution, it has been shown, especially for the most soluble ones, that they tend to restrain the evaporation flux q~v, and hence increase the probability of superficial salt crystallisation (beq is higher). In the case of a low capillary imbibition kinetic (~), the presence of salts for which in the saturated brines the water activity drops under 0.9 (Appendix A.3), the hydrodynamical equilibrium position of the meniscus is raised toward the surface. Hence, sub-superficial salt crystallisation is promoted. On the other hand, for salts such as calcite or gypsum the effect on water activity is negligible, but as their solubilities are very low, they crystallise promptly, before reaching the hydrodynamical equilibrium position. Consequently, while the meniscus is moving from the surface toward the equilibrium position, crystallites of salts are left in the superficial part. This mathematical result can be directly related to the features observed on rocks affected by contour scaling in monuments: the external part of the rock which falls off, is partially impregnated with gypsum, whereas the highest gypsum concentration is observed at the point of the fracture, for which it is responsible (Figure 8).

Nevertheless, for the simple drying condition and the wick-like condition, the intrinsic parameters of water transfer in the porous network of the rocks mainly govern the water balances and the position of salt crystallisation. Hence, the potential form and magnitude of the decay of the rock depend basically on the rock's pore structures influencing the water transfer. The optimal conditions for rocks used on monuments are those of high diffusivity, which guarantees a significant drainage of the rocks during the superficial stage of evaporation, and those of high capillary imbibition kinetics allowing a positive flux of water at the evaporating surface. An ideal theoretical pore size distribution can be proposed to satisfy these conditions of maximum liquid transfer toward the surface, with three types of pores (Figure %) organised in layers parallel to the evaporating surface of the rock:

9 fine driving pores, situated near or on the evaporating surface of the rock, in which high capillary pressure allows water to drain from internal parts, 9 intermediate conducting pores, permitting the transfer of water towards the surface with a satisfactory hydraulic conductivity, 9 coarse reservoir pores, situated inside the rock, with low capillary pressure being easily drained and representing the main porous volume. This distribution favourable to high diffusivity is also suitable for high capillary imbibition kinetic, as in conical shaped pores, the meniscus accelerates towards the narrowest end [START_REF] Hammecker | Modelling the Capillary' Imbibition in Sedimentary Rocks: Role of Petrographical Features[END_REF].

On the other hand, contrary to this theoretical "layered" pore distribution, a natural ideal pore structure, enhancing the probability for superficial evaporation, can be observed. In fact the example of Darney sandstone is very explicit of this pore structure: its wide pores and interconnections allow a high hydraulic conductivity, whereas at the same time, the superficial roughness on the grains represented by its uniform clayey coating, can be considered as a microporous network (DULLIEN et al., 1989) which is responsible for high capillary pressures, able to drive the water toward the surface (Figure 9b) The coexistence of two parallel porous networks, one macroporous and the other microporous, allows to combine high hydraulic conductivity to high capillary pressure, which are apparently antangonistic properties, in order to achieve important diffusivity.

Conclusion

The physical decay processes affecting the rocks on monuments, and related to water transfer and associated salt crystallisation, have been studied quantitatively in isothermal conditions. This study has been based on two different approaches. On one hand, traditional water transfer concepts and equations in unsaturated porous media, usually used in soil science, have been adapted to this specific problem. On the other hand, some calculation models have been designed, based on simple capillary and evaporation kinetic measurements. Although the geometry of the porous networks of rocks cannot be compared to cylindrical tubes, their hydrodynamical behaviours are very similar [START_REF] Dullien | Porous Media Fluid Transport and Pore Structure[END_REF][START_REF] Hammecker | A Geometrical Model Jar Numerical Simulation of Capillary Imbibition in Sedimentary Rocks[END_REF]. Hence the kinetics of these phenomena have been treated as theoretical cylindrical tubes. The physical influence of the presence of solute on the evaporation fluxes has been quantified by introducing the evolution of water activity calculated with the model of PlTZER (1973). The most important external factor governing the water transfer in rocks submitted to these conditions, has been determined as being the air convection (wind velocity), whereas the influence of relative humidity is less important. Contrastingly, it has been shown that the presence of solute in solution modifies efficiently the water balance in rocks, especially for those leading to the crystallisation of the most soluble salts (NaC1, Na2SO4, KCI, etc.). For calcium sulphate solutions, the effect on water balance is almost negligible, but the mechanism of contour scaling has been demonstrated quantitatively.

Nevertheless, this study shows that the intrinsic parameters of the rocks, diffusivity D and capillary imbibition kinetic coefficient N, are the actual determining factors for the water balance, for the crystallisation position and consequently for the decay forms. In fact when different rocks are submitted to the same environmental conditions on a monument, and they evolve differently, it is regardless of their chemical and mineralogical composition, but rather depends on their petrophysical properties which manage the water transfer (quantities and kinetics).

Finally, an ideal pore structure and an ideal pore distribution have been proposed in order to optimise the diffusivity and the imbibition kinetic, hence to promote the transfer of liquid water toward the surface of the rock. PAGEOPH, WYLIE, R. G., The properties of salt-water systems in relation humidity. In Humidity and Moisture, (Rheinhold Publ. Corp., New York 1963) 3, pp. 507-517. ZEHNDER, K. (1982)

  Figure 1Capillary imbibition: la experiment and lb curve, Evaporation: 2a experiment and 2b curve.

  D OO/Ox=q~, x=O, t>O (c).

  Figure 2 E,~otution of the critical water content 0~. versus external (q~.~) and internal parameters (D:, and fi).

where 7 :

 7 surface tension (0.072 N/m for water at 25~ 7: viscosity (1.019. l0 -3 PI for water at 25~ Y0: height of the meniscus at t = 0.When the initial height of the meniscus Yo is equal to 0, the migration of the meniscus in the tube can be formulated as a simple square root of time function y = ~' ,//t, (17) PAGEOPH, where cg is equivalent to the experimental ~ kinetic parameter. Hence the capillary imbibition

  Figure 3Tube model for evaporation. L: length of the tube, h: distance from the opening, P0: vapour pressure over the water surface, p~: vapour pressure in air, g: distance from the water surface where p =p~.

Figure 4

 4 Figure 4Evolution of the equilibrium height in wick-like conditions.

}

  t,, C,=2Co ~ C(t)=Co.(l+h(t)/2).

  Figure 5Chemical diffusion models: 1. instant diffusion, 2. no diffusion.

  Figure 6Evolution of equilibrium height taking into account the presence of" salt.

  Figure 7 Mercury porosimetry curves,

  Figure 8Schematic representation of the formation of contour scaling.

  Figure 9Theoretical porous geometry for high diffusivity: a. pore distribution in the rock, b. pore structure.

Table 1

 1 Examples of petrophysical properties and diffusivity values in some sedimentary rocks

			Gueberschwihr
	Rock	Darney sandstone	sandstone	Laspra limestone	Hontoria limestone
	Petrography	Coarse sandstone	Coarse sandstone	Fine	Coarse
		clayey coating	highly silicified	homogeneous	heterogeneous
				dolomicrit	bioclastic Iimestone
	GS (/~m)	250	450 750	20	250
	N, (%)	25	6	32	20
	K o (111 9 S -l)	2.4 " 10 -s	6 " 10 lO	2.4 " 10 .7	2.4 ' 10 .6
	Ssa (m2/kg)	2.53" 103	0.27' 103	4.6" 103	0.8" 103
	D a (m2/s)	1.2. 10 7	6.9. 10 -11	5.5. l0 s	4.1 9 10 8
	/3	34	156	60	45
	D i (mZ/s)	2.6, 10 4	2. 10 .8	7.2. 10 .5	1.4. 10 .4
	0,,/0 i (%)	30	83	42	32
	,~ (cm. h -~/2)	5.2	0.3	2.4	7.1

m GS: average grain size PAGEOPH,

,

  Verwitterung yon Molassesandsteinen an Bauwerken und in Naturaufsehliissen, Beitr/ige z. Geologie d. Schweiz, Geotech. Kommission 61, Kiimmerly and Frey, Bern.distance of the meniscus from the evaporating end of the tube initial distance of the meniscus from the evaporating end of the tube height of the meniscus in a tube above the free water level air layer over the water surface where Pl <P <Po

	x:
	x o:
	y:
	Yo:	initial height of the meniscus
	P:	(Received October 31, 1994, accepted April 4, 1995) empirical constant
	7:	surface tension
	2:	thickness of the superficial concentrated layer
	~/:	dynamic viscosity	List of Symbols
		matrix potential
	0:	weight increase by capillary imbibition water content
		capillary imbibition kinetic coefficient (experimental) air-dry water content
	c~ 0 c :	concentration in air critical water content
	C:	concentration in solution initial water content
	p:	capillary imbibition kinetic coefficient (= N) fluid density
	D(0):	diffusivity thickness of the
	Da :	air dry diffusivity
	D~:	initial diffusivity
	9:	isothermal rate of diffusion for water vapour in air
	h:	distance of the meniscus from the evaporating end of the tube
	k:	water vapour conductivity in air
	K(~):	hydraulic conductivity
	Ko:	saturated hydraulic conductivity
	L:	length of the sample, tube
	N,:	porosity freely invaded in capillary imbibition
	N,:	total porosity
	M:	molecular mass of water
	Q(o, t)	water balance at the surface of the rock
	P:	atmospheric pressure
	Po:	saturated vapour pressure
	Pl:	fixed water pressure
	qc :	capillary imbibition flow
	qe :	evaporation flow
	qct :	constant rate of drying (massic)
	q~ :	constant rate of drying (volumic)
	q*:	falling rate of drying
	R:	universal gas constant
	r:	hydraulic radius
	S:	macroscopical area through which water transfer occurs
	S~a :	specific surface area
	T:	temperature
		time
		volume

t:

V:

Eq. Pitzer : aw(i)=f(C i, SALT)] Qevp(i)=f(aw(i)) < q(i): Qeap(i) -qev(i) 1


Bernard Boigelot

Pascal Fontaine

Baptiste Vergain

Universal First-Order Quantication over Automata ⋆

Keywords: Innite-word automata, rst-order logic, quantier elimination, satisability

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

Introduction

Automated reasoning with arithmetic theories is of primary importance, notably for verication, where Satisability Modulo Theories (SMT) solvers are regularly used to discharge proof obligations. It is well known however that mixing arithmetic with uninterpreted symbols quickly leads to undecidable languages. For instance, extending Presburger arithmetic, i.e., the rst-order additive theory of integer numbers, with just one uninterpreted unary predicate makes it undecidable [START_REF] Downey | Undecidability of Presburger arithmetic with a single monadic predicate letter[END_REF][START_REF] Halpern | Presburger arithmetic with unary predicates is Π 1 1 complete[END_REF][START_REF] Speranski | A note on denability in fragments of arithmetic with free unary predicates[END_REF]. There exist decidable fragments mixing arithmetic and uninterpreted symbols that are expressive enough to be interesting, for instance, the monadic second-order theory of N under one successor (S1S).

The decidability of S1S has been established thanks to the concept of inniteword automaton [START_REF] Büchi | On a decision method in restricted second order arithmetic[END_REF]. In order to decide whether a formula φ is satisable, the approach consists in building an automaton that recognizes the set of its models, encoded in a suitable way, and then checking that this automaton accepts a non-empty language. Such an automaton has one separate input tape for each rst-order and second-order free variable of φ. It is constructed by starting from elementary automata representing the atoms of φ, and then translating the effect of Boolean connectives and quantiers into corresponding operations over automata. For instance, applying an existential quantier simply amounts to removing from the automaton the input tape associated to the quantied variable. Universal quantication reduces to existential quantication thanks to the equivalence ∀x φ ≡ ¬∃x ¬φ.

Even though this approach has originally been introduced as a purely theoretical tool, it is applied in practice to obtain usable decision procedures for various logics. In particular, the tool MONA [START_REF] Klarlund | Mona & Fido: The logic-automaton connection in practice[END_REF] uses this method to decide a restricted version of S1S, and tools such as LASH [START_REF] Boigelot | Counting the solutions of Presburger equations without enumerating them[END_REF] and Shasta [START_REF] Shiple | A comparison of Presburger engines for EFSM reachability[END_REF] use a similar technique to decide Presburger arithmetic. The LASH tool also generalizes this result by providing an implemented decision procedure for the rst-order additive theory of mixed integer and real variables [START_REF] Boigelot | An eective decision procedure for linear arithmetic over the integers and reals[END_REF].

A major issue in practice is that the elimination of universal quantiers relies on complementation, which is an operation that is not easily implemented for innite-word automata [START_REF] Safra | On the complexity of omega-automata[END_REF][START_REF] Vardi | The Büchi complementation saga[END_REF]. Actual implementations of automata-based decision procedures elude this problem by restricting the language of interest or the class of automata that need to be manipulated. For instance, the tool MONA only handles Weak S1S (WS1S) which is, schematically, a restriction of S1S to nite subsets of natural numbers [START_REF] Büchi | Weak second-order arithmetic and nite automata[END_REF]. The tool LASH handles the mixed integer and real additive arithmetic by working with weak deterministic automata, which are a restricted form of innite-word automata admitting an easy complementation algorithm [START_REF] Boigelot | An eective decision procedure for linear arithmetic over the integers and reals[END_REF].

The contribution of this paper is to introduce a direct algorithm for computing the eect of universal rst-order quantication over innite-word automata. This is an essential step towards practical decision procedures for more expressive fragments mixing arithmetic with uninterpreted symbols. The considered automata are those that recognize models of formulas over natural numbers encoded in unary notation. This algorithm does not rely on complementation, and can be implemented straightforwardly on unrestricted innite-word automata.

As an example of its potential applications, this algorithm leads to a practically implementable decision procedure for the rst-order theory of natural numbers with the order relation and uninterpreted unary predicates. It also paves the way to a decision procedure for SMT solvers for the UFIDL (Uninterpreted Functions and Integer Dierence Logic) logic with only unary predicates.

Basic notions 2.1 Logic

We address the problem of deciding satisability for formulas expressed in rstorder structures of the form (N, R 1 , R 2 , . . .), where N is the domain of natural numbers, and R 1 , R 2 , . . . are (interpreted) relations over tuples of values in N. More precisely, each R i is dened as a relation R i ⊆ N αi for some α i > 0 called the arity of R i .

The formulas in such a structure involve rst-order variables x 1 , x 2 , . . . , and second-order variables X 1 , X 2 , . . . Formulas are recursively dened as ⊤, ⊥, x i = x j , X i = X j , X i (x j ) or R i (x j1 , . . . , x jα i ), where i, j, j 1 , j 2 , . . . ∈ N >0 (atomic formulas), φ 1 ∧ φ 2 , φ 1 ∨ φ 2 or ¬φ, where φ 1 , φ 2 and φ are formulas, or ∃x i φ or ∀x i φ, where φ is a formula.

We write φ(x 1 , . . . , x k , X 1 , . . . , X ℓ ) to express that x 1 , . . . , x k , X 1 , . . . , X ℓ are the free variables of φ, i.e., that φ does not involve other unquantied variables.

An interpretation I for a formula φ(x 1 , . . . , x k , X 1 , . . . , X ℓ ) is an assignment of values I(x i ) ∈ N for all i ∈ [1, k] and I(X j ) ⊆ N for all j ∈ [1, ℓ] to its free variables. An interpretation I that makes φ true, which is denoted by

I |= φ, is called a model of φ.
The semantics is dened in the usual way. One has In the two last rules, the notation

I |= ⊤ and I ̸ |= ⊥ for every I. I |= x i = x j and I |= X i = X j i (respectively) I(x i ) = I(x j ) and I(X i ) = I(X j ). I |= X i (x j ) i I(x j ) ∈ I(X i ). I |= R i (x j1 , . . . , x jα i ) i (I(x j1 ), . . . , I(x jα i )) ∈ R i . I |= φ 1 ∧ φ 2 , I |= φ 1 ∨
I[x i = n],
where n ∈ N, stands for the extension of the interpretation I to one additional rst-order variable x i that takes the value n, i.e., the interpretation such that

I[x i = n](x j ) = I(x j ) for all j ∈ [1, k] such that j ̸ = i, I[x i = n](x i ) = n, and I[x i = n](X j ) = I(X j ) for all j ∈ [1, ℓ].
A formula is said to be satisable if it admits a model.

Automata

A nite-word or innite-word automaton is a tuple

A = (Σ, Q, ∆, Q 0 , F ) where Σ is a nite alphabet, Q is a nite set of states, ∆ ⊆ Q × (Σ ∪ {ε}) × Q is a transition relation, Q 0 ⊆ Q is a set of initial states, and F ⊆ Q is a set of accepting states.
A path of A from q 0 to q m , with q 0 , q m ∈ Q and m ≥ 0, is a nite sequence π = (q 0 , a 0 , q 1 ); (q 1 , a 1 , q 2 ); . . . ; (q m-1 , a m-1 , q m ) of transitions from ∆. Thenite word w ∈ Σ * read by π is w = a 0 a 1 . . . a m-1 ; the existence of such a path is denoted by q 0 w → q m . A cycle is a non-empty path from a state to itself. If A is a nite-word automaton, then a path π from q 0 to q m is accepting if q m ∈ F . A word w ∈ Σ * is accepted from the state q 0 if there exists an accepting path originating from q 0 that reads w.

For innite-word automata, we use a Büchi acceptance condition for the sake of simplicity, but the results of this paper straightforwardly generalize to other types of innite-word automata. If A is an innite-word automaton, then a run of A from a state q 0 ∈ Q is an innite sequence σ = (q 0 , a 0 , q 1 ); (q 1 , a 1 , q 2 ); . . . of transitions from ∆. This run reads the innite word w = a 0 a 1 . . . ∈ Σ ω . The run σ is accepting if the set inf (σ) formed by the states q i that occur innitely many times in σ is such that inf (σ) ∩ F ̸ = ∅, i.e., there exists a state in F that is visited innitely often by σ. A word w ∈ Σ ω is accepted from the state q 0 ∈ Q if there exists an accepting run from q 0 that reads w.

For both nite-word and innite-word automata, a word w is accepted by A if it is accepted from an initial state q 0 ∈ Q 0 . The set of all words accepted from a state q ∈ Q (resp. by A) forms the language L(A, q) accepted from q (resp. L(A) accepted by A). An automaton accepting L(A, q) can be derived from A by setting Q 0 equal to {q}. The language of nite-words w read by paths from q 1 to q 2 , with q 1 , q 2 ∈ Q, is denoted by L(A, q 1 , q 2 ); a nite-word automaton accepting this language can be obtained from A by setting Q 0 equal to {q 1 } and F equal to {q 2 }. A language is said to be regular (resp. ω-regular ) if it can be accepted by a nite-word (resp. an innite-word) automaton.

3 Deciding Satisability

Encoding Interpretations

In order to decide whether a formula φ(x 1 , . . . , x k , X 1 , . . . , X ℓ ) is satisable, Büchi introduced the idea of building an automaton that accepts the set of all models of φ, encoded in a suitable way, and then checking whether it accepts a non-empty language [START_REF] Büchi | Weak second-order arithmetic and nite automata[END_REF][START_REF] Büchi | On a decision method in restricted second order arithmetic[END_REF].

A simple encoding scheme consists in representing the value of rst-order variables x i in unary notation: A number n ∈ N is encoded by the innite word 0 n 10 ω over the alphabet {0, 1}, i.e., by a word in which the symbol 1 occurs only once, at the position given by n. This leads to a compatible encoding scheme for the values of second-order variables X j : a predicate P ⊆ N is encoded by the innite word a 0 a 1 a 2 . . . such that for every n ∈ N, a n ∈ {0, 1} satises a n = 1 i n ∈ P , i.e., if P (n) holds.

Encodings for the values of rst-order variables x 1 , . . . , x k and second-order variables X 1 , . . . , X ℓ can be combined into a single word over the alphabet Σ = {0, 1} k+ℓ : A word w ∈ Σ ω encodes an interpretation I for those variables i w = (a 0,1 , . . . , a 0,k+ℓ )(a 1,1 , . . . , a 1,k+ℓ ) . . ., where for each i ∈ [1, k], a 0,i a 1,i . . . encodes I(x i ), and for each j ∈ [1, ℓ], a 0,k+j a 1,k+j . . . encodes I(X j ). Note that not all innite words over Σ form valid encodings: For each rst-order variable x i , an encoding must contain exactly one occurrence of the symbol 1 for the i-th

q0 q1 q2 (0), (1) (0), (1) (0), (1)
(0), ( 1) {x1}

(1) {x2}

(a) x1 < x2 ∧ X1(x2) q0 q1 q2 (0), (1) (0), (1) (0), (1)
(0), ( 1) {x1}

(1)

(b) ∃x2(x1 < x2 ∧ X1(x2))
Fig. 1: Automata recognizing sets of models.

component of its tuple symbols. Assuming that the set of variables is clear from the context, we write e(I) for the encoding of I with respect to those variables.

Automata Recognizing Sets of Models

Let S be a set of interpretations for k rst-order and ℓ second-order variables.

The set of encodings of the elements of S forms a language L over the alphabet {0, 1} k+ℓ . If this language is ω-regular, then we say that an automaton A that accepts L recognizes, or represents, the set S. Such an automaton can be viewed as having k + ℓ input tapes reading symbols from {0, 1}, each of these tapes being associated to a variable. Equivalently, we can write the label of a transition (q 1 , (a 1 , . . . , a k+ℓ ), q 2 ) ∈ ∆ as (a k+1 ,...,a k+ℓ )

V where V is the set of the variables x i , with i ∈ [1, k], for which a i = 1. In other words, each transition label distinct from ε species the set of rst-order variables whose value corresponds to this transition, and provides one symbol for each second-order variable. For each x i ∈ V , we then say that x i is associated to the transition. Note that every transition for which V ̸ = ∅ can only be followed at most once in an accepting run. Any automaton recognizing a set of valid encodings can therefore easily be transformed into one in which such transitions do not appear in cycles, and that accepts the same language.

An example of an automaton recognizing the set of models of the formula φ(x 1 , x 2 , X 1 ) = x 1 < x 2 ∧ X 1 (x 2 ) is given in Figure 1a. For the sake of clarity, labels of transitions sharing the same origin and destination are grouped together, and empty sets of variables are omitted.

Decision Procedure

For the automata-based approach to be applicable, it must be possible to construct elementary automata recognizing the models of atomic formulas. This is clearly the case for atoms of the form x i = x j , X i = X j and X i (x j ), and this property must also hold for each relation R i that belongs to the structure of interest; in other words, the atomic formula R i (x 1 , x 2 , . . . , x αi ) must admit a set of models whose encoding is ω-regular. With the positional encoding of natural numbers, this is the case in particular for the order relation x i < x j and the successor relation x j = x i + 1. Note that one can easily add supplementary variables to an automaton, by inserting a new component in the tuples of its alphabet, and making this component read a symbol 1 at any single position of a run for rst-order variables, and any symbol at any position for second-order ones. Reordering the variables is a similarly immediate operation.

After automata recognizing the models of atomic formulas have been obtained, the next step consists in combining them recursively by following the syntactic structure of the formula to be decided. Let us denote by L φ the language of encodings of all the models of a formula φ, i.e., L φ = {e(I) | I |= φ}.

For the Boolean operator ∧, we have L φ1∧φ2 = L φ1 ∩ L φ2 , where φ 1 and φ 2 are formulas over the same free variables. Similarly, we have L φ1∨φ2 = L φ1 ∪L φ2 . The case of the complement operator ¬ is slightly more complicated, since the complement of a language of encodings systematically contains words that do not validly encode an interpretation. The set of models of a formula ¬φ is encoded by the language L φ ∩ L valid , where L valid is the language of all valid encodings consistent with the free variables of φ. It is easily seen that this language is ω-regular.

It remains to compute the eect of quantiers. The language L ∃xiφ can be derived from L φ by removing the i-th component from each tuple symbol, i.e., by applying a mapping Π ̸ =i : Σ k+ℓ → Σ k+ℓ-1 : (a 1 , . . . , a k+ℓ ) → (a 1 , . . . , a i-1 , a i+1 , . . . , a k+ℓ ) to each symbol of the alphabet. Indeed, the models of ∃x i φ correspond exactly to the models of φ in which the variable x i is removed. In the rest of this paper, we will use the notation Π ̸ =i (w), where w is a nite or innite word, to express the result of applying Π ̸ =i to each symbol in w. If L is a language, then we write Π ̸ =i (L) for the language {Π ̸ =i (w) | w ∈ L}.

Finally, universal quantication can be reduced to existential quantication: For computing L ∀xiφ , we use the equivalence ∀x i φ ≡ ¬∃x i ¬φ which yields L ∀xiφ = L ∃xi¬φ ∩ L valid .

Operations over Automata

We now discuss how the operations over languages mentioned in Section 3.3 can be computed over innite-word automata. Given automata A 1 and A 2 , automata A 1 ∩ A 2 and A 1 ∪ A 2 accepting respectively L(A 1 ) ∩ L(A 2 ) and L(A 1 ) ∪ L(A 2 ) can be obtained by the so-called product construction. The idea consists in building an automaton A that simulates the combined behavior of A 1 and A 2 on identical input words. The states of A need to store additional information about the accepting states that are visited in A 1 and A 2 . For A 1 ∩ A 2 , one ensures that each accepting run of A correspond to an accepting run in both A 1 and A 2 . For A 1 ∪ A 2 , the condition is that the run should be accepting in A 1 or A 2 , or both. A complete description of the product construction for Büchi automata is given in [START_REF] Thomas | Automata on innite objects[END_REF].

Modifying the alphabet of an automaton in order to implement the eect of an existential quantication is a simple operation. As an example, Figure 1b shows an automaton recognizing the set of models of ∃x 2 (x 1 < x 2 ∧ X 1 (x 2 )), obtained by removing all occurrences of the variable x 2 from transition labels.

Testing whether the language accepted by an automaton is not empty amounts to checking the existence of a reachable cycle that visits at least one accepting state, which is simple as well.

The only problematic operation is complementation, which consists in computing from an automaton A an automaton that accepts the language L(A). Although it preserves ω-regularity, this operation is dicult to perform on Büchi automata [START_REF] Safra | On the complexity of omega-automata[END_REF][START_REF] Vardi | The Büchi complementation saga[END_REF]. In the context of our decision procedure, it is only useful for applying universal quantiers. Indeed, other instances of the negation operator in formulas can be pushed inwards until they are applied to atomic formulas, and it is easy to construct the complement of the elementary automata recognizing the models of those atomic formulas, provided that for each relation R i in the structure of interest, an automaton recognizing {(x 1 , . . . , x αi ) ∈ N αi | ¬R i (x 1 , . . . , x αi )} is available. In order to eliminate the need for complementation, we develop in the next section a direct algorithm for computing the eect of universal quantiers on automata recognizing sets of models.

4 Universal Quantication

Principles

Let φ(x 1 , . . . , x k , X 1 , . . . , X ℓ ), with k > 0 and ℓ ≥ 0, be a formula. Our goal is to compute an automaton A ′ accepting L ∀xiφ , given an automaton A accepting L φ and i ∈ [1, k].

By denition of universal quantication, we have I |= ∀x i φ i I[x i = n] |= φ holds for every n ∈ N. In other words, L ∀xiφ contains e(I) i L φ contains e(I[x i = n]) for every n ∈ N. Conceptually, we can then obtain L ∀xiφ by dening for each n ∈ N the language S n = {e(I) | e(I[x i = n]) ∈ L φ }, which yields L ∀xiφ = n∈N S n .

An automaton A ′ accepting L ∀xiφ can be obtained as follows. Each language S n , with n ∈ N, is accepted by an automaton A n derived from A by restricting the transitions associated to x i to be followed only after having read exactly n symbols. In other words, the accepting runs of A n correspond to the accepting runs of A that satisfy this condition. After imposing this restriction, the variable x i is removed from the set of variables managed by the automaton, i.e., the operator Π ̸ =i is applied to the language that this automaton accepts, so as to get S n = L(A n ). The automaton A ′ then corresponds to the innite intersection product of the automata A n for all n ∈ N, i.e., an automaton that accepts the innite intersection n∈N S n . We show in the next section how to build A ′ by means of a nite computation.

Construction

The idea of the construction is to make A ′ simulate the join behavior of the automata A n , for all n ∈ N, on the same input words. This can be done by making each state of A ′ correspond to one state q n in each A n , i.e., to an innite tuple (q 0 , q 1 , . . .). By denition of A n , there exists a mapping µ : Q n → Q, where Q n and Q are respectively the sets of states of A n and A, such that whenever a run of A n visits q n , the corresponding run of A on the same input word visits µ(q n ).

If two automata A n1 and A n2 , with n 1 , n 2 ∈ N, are (respectively) in states q n1 and q n2 such that µ(q n1 ) = µ(q n2 ), then they share the same future behaviors, except for the requirement to follow a transition associated to x i after having read (respectively) n 1 and n 2 symbols. It follows that the states of A ′ can be characterized by sets of states of A: The innite tuple (q 0 , q 1 , . . .) is described by the set {µ(q i ) | i ∈ N}. Each element of this set represents the current state of one or several automata among the A n . This means that the number of these automata that are in this current state is not counted. We will establish that this abstraction is precise and leads to a correct construction.

During a run of A ′ , each transition with a label other than ε must correspond to a transition reading the same symbol in every automaton A n , which in turn can be mapped to a transition of A. In the automaton A n for which n is equal to the number of symbols already read during the run, this transition of A is necessarily associated to x i , by denition of A n . It follows that every transition of A ′ with a non-empty label is characterized by a set of transitions of A, among which one of them is associated to x i .

We are now ready to describe formally the construction of A ′ , leaving for the next section the problem of determining which of its runs should be accepting or not: From the automaton

A = (Σ, Q, ∆, Q 0 , F ), we construct A ′ = (Σ ′ , Q ′ , ∆ ′ , Q ′ 0 , F ′ ) such that Σ ′ = Π ̸ =i (Σ). Q ′ = 2 Q \ {∅}. ∆ ′ contains
• the transitions (q ′ 1 , (a ′ 1 , . . . , a ′ k+ℓ-1 ), q ′

2 ) for which there exists a set T ⊆ ∆ that satises the following conditions:

* q ′ 1 = {q 1 | (q 1 , (a 1 , . . . , a k+ℓ ), q 2 ) ∈ T }. * q ′ 2 = {q 2 | (q 1 , (a 1 , . . . , a k+ℓ ), q 2 ) ∈ T }.
* For all (q 1 , (a 1 , . . . , a k+ℓ ), q 2 ) ∈ T , one has a ′ j = a j for all j ∈ [1, i-1], and a ′ j = a j+1 for all j ∈ [i, k + ℓ -1]. * There exists exactly one (q 1 , (a 1 , . . . , a k+ℓ ), q 2 ) ∈ T such that a i = 1.

• the transitions (q ′ 1 , ε, q ′ 2 ) for which there exists a transition (q 1 , ε, q 2 ) ∈ ∆ such that

* q 1 ∈ q ′ 1 . * q ′ 2 = q ′ 1 ∪ {q 2 } or q ′ 2 = (q ′ 1 \ {q 1 }) ∪ {q 2 }. Q ′ 0 = 2 Q0 \ {∅}. F ′ = Q ′ for now.
The problem of characterizing more nely the accepting runs will be addressed in the next section.

The rule for the transitions (q ′ 1 , (a ′ 1 , . . . , a ′ k+ℓ-1 ), q ′

2 ) ensures that for each

q 1 ∈ q ′
1 , each automaton A n that is simulated by A ′ has the choice of following any possible transition originating from q 1 that has a label consistent with

{q0} {q0, q1} {q0, q1, q2} (0), (1) (0), (1) (0), (1) (1)
Fig. 2: First step of construction for ∀x

1 ∃x 2 (x 1 < x 2 ∧ X 1 (x 2 )). (a ′ 1 , . . . , a ′ k+ℓ-1
). One such automaton must nevertheless follow a transition associated to the quantied variable x i . The rule for the transitions

(q ′ 1 , ε, q ′ 2 )
expresses that one automaton A n , or any number of identical copies of this automaton, must follow a transition labeled by ε, while the other automata stay in their current state.

As an example, applying this construction to the automaton in Figure 1b, as a rst step of the computation of a representation of ∀x 1 ∃x 2 (x 1 < x 2 ∧ X 1 (x 2 )), yields the automaton given in Figure 2. For the sake of clarity, unreachable states and states from which the accepted language is empty are not depicted.

A Criterion for Accepting Runs

The automaton A ′ dened in the previous section simulates an innite combination of automata A n , for all n ∈ N. By construction, every accepting run of this innite combination corresponds to a run of A ′ .

The reciprocal property is not true, in the sense that there may exist a run of A ′ that does not match an accepting run of the innite combination of automata A n . Consider for instance a run of the automaton in Figure 2 that ends up cycling in the state {q 0 , q 1 , q 2 }, reading 0 ω from that state. Recall that for this example, the automaton A that undergoes the universal quantication operation is the one given in Figure 1b. The run that we have considered can be followed in A ′ , but cannot be accepting in every A n . Indeed, in this example, the transition of A n reading the (n + 1)-th symbol of the run corresponds, by denition of this automaton, to the transition of A that is associated to the quantied variable x 1 . By the structure of A, this transition is necessarily followed later in any accepting run by one that reads the symbol 1, which implies that no word of the form u • 0 ω , with u ∈ {0, 1} * , can be accepted by a run of A n such that n ≥ |u|. This represents the fact that the words accepted by all A n correspond to the encodings of predicates that are true innitely often.

One thus needs a criterion for characterizing the runs of A ′ that correspond to combinations of accepting runs in all automata A n .

It is known [START_REF] Mcnaughton | Testing and generating innite sequences by a nite automaton[END_REF] that two ω-regular languages over the alphabet Σ are equal i they share the same set of ultimately periodic words, i.e., words of the form u • v ω with u ∈ Σ * and v ∈ Σ + . It follows that it is sucient to characterize the accepting runs of A ′ that read ultimately periodic words. The automaton A ′ accepts a word u • v ω i every A n , with n ∈ N, admits an accepting run that reads this word. Note that such a run also matches a run of A, and that this run of A always ends up following a cycle from an accepting state to itself.

Our solution takes the following form. For each state q of A, we dene a language U q ⊆ Σ + of non-empty words u such that A accepts u ω from q, after dismissing the input tape associated to the quantied variable x i . The alphabet Σ is thus equal to {0, 1} k+ℓ-1 . Remember that each state q ′ of A ′ is dened as a subset of states of A, corresponding to the current states in the combination of copies of A that are jointly simulated by A ′ . In order for the word u ω to be accepted by A from q ′ , it should therefore be accepted by A from each state q ∈ q ′ , i.e., u must belong to all the languages U q such that q ∈ q ′ . It must also be possible to read u ω from the state q ′ of A ′ . We impose a stronger condition, by requiring that there exists a cycle from q ′ to itself labeled by u. This condition leads to a correct acceptance criterion.

In summary, the language U ′ q ′ = L(A ′ , q ′ , q ′ ) ∩ q∈q ′ U q characterizes the words u such that u ω must be accepted from the state q ′ of A ′ . Note that for this property to hold, it is not necessary for the language U q to contain all words u such that u ω ∈ Π ̸ =i (L(A, q)), but only some number of copies u p , where p > 0 is bounded, of each such u. In other words, the nite words u whose innite repetition is accepted from q do not have to be the shortest possible ones.

Once the language U ′ q ′ has been obtained, we build a widget, in the form of an innite-word automaton accepting (U ′ q ′ ) ω , along the state q ′ of A ′ , and add a transition labeled by ε from q ′ to the initial state of this widget. This ensures that every path that ends up in q ′ can be suitably extended into an accepting run. Such a widget does not have to be constructed for every state q ′ of A ′ : Since the goal is to accept from q ′ words of the form u ω , we can require that at least one state q ∈ q ′ is accepting in A. We then only build widgets for the states q ′ that satisfy this requirement.

Computation Steps

The procedure for modifying A ′ in order to make it accept the runs that match those of the innite combination of automata A n , outlined in the previous section, can be carried out by representing the regular languages U q and U ′ q ′ by nite-state automata. The construction proceeds as follows:

1. For each state q ∈ Q of A, build a nite-word automaton A q that accepts all the non-empty words u for which there exists a path q v → q of A that visits at least one accepting state q F ∈ F , such that u = Π ̸ =i (v). This automaton can be constructed in a similar way as one accepting Π ̸ =i (L(A, q, q)) (cf. Sections 2.2 and 3.4), keeping one additional bit of information in its states for determining whether an accepting state has already been visited or not. 2. For each pair of states q 1 , q 2 ∈ Q of A, build a nite-word automaton A q1,q2

accepting the language Π ̸ =i (L(A, q 1 , q 2 )) (cf. Sections 2.2 and 3.4). 3. For each state q ∈ Q of A, build an automaton A Uq = r∈Q (A q,r ∩ A r )

accepting the nite-word language U q . {q0} {q0, q1} {q0, q1, q2} q ′ repeat (0), (1) (0), (1)

(0), (1) (1)
(0), (1)

(0), ( 1
) (0), (1) (1)
ε ε ε Fig. 3: Automaton recognizing the set of models of ∀x 1 ∃x 2 (x 1 < x 2 ∧ X 1 (x 2 )).

4. For each state q ′ of A ′ such that q ′ ∩ F ̸ = ∅, where F is the set of accepting states of A, build a nite-word automaton

A ′ U ′ q ′ = A ′ q ′ ∩ q∈q ′ A Uq accepting U ′
q ′ , where A ′ q ′ is an automaton accepting L(A ′ , q ′ , q ′ ) (cf. Section 2.2).

Then, turn each automaton

A ′ U ′ q ′ into an innite-word automaton A ′ (U ′ q ′ ) ω accepting (U ′ q ′ ) ω : (a) Create a new state q ′ repeat . (b) Add a transition (q ′
repeat , ε, q 0 ) for each initial state q 0 , and a transition (q F , ε, q ′ repeat ) for each accepting state q F , of A ′ U ′ q ′ . (c) Make q ′ repeat the only initial and accepting state of A ′ (U ′ q ′ ) ω . 6. For each state q ′ of A ′ considered at Step 4, add the widget A ′ U ′ q ′ alongside q ′ , by incorporating its sets of states and transitions into those of A ′ , and adding a transition (q ′ , ε, q ′ r epeat ). In the resulting automaton, mark as the only accepting states the states q ′ repeat of all widgets. This procedure constructs an automaton that accepts the language L ∀xiφ . Applied to the automaton A ′ in Figure 2, it produces the result shown in Figure 3. For the sake of clarity, the states from which the accepted language is empty have been removed. A detailed description of the computation steps for this example and the proof of correctness of the construction are given in [START_REF] Boigelot | Universal rst-order quantication over automata[END_REF].

Conclusions

This paper introduces a method for directly computing the eect of a rstorder universal quantier on an innite-word automaton recognizing the set of models of a formula. It is applicable when the rst-order variables range over the natural numbers and their values are encoded in unary notation. Among its potential applications, it provides a solution for deciding the rst-order theory ⟨N, <⟩ extended with uninterpreted unary predicates.

The operation on regular languages that corresponds to the eect of a universal rst-order quantier has already been studied at the theoretical level [START_REF] Okhotin | The dual of concatenation[END_REF]. Our contribution is to provide a practical algorithm for computing it, that does not require to complement innite-word automata. This algorithm has an exponential worst-case time complexity, which is unavoidable since there exist automata for which universal quantication incurs an exponential blowup in their number of states (see [START_REF] Boigelot | Universal rst-order quantication over automata[END_REF] for details). The main advantage over the complementationbased approach is however that this exponential cost is not systematic, since only a fraction of the possible subsets of states typically need to be constructed.

Our solution is open to many possible improvements, one of them being to extend the algorithm so as to quantify over several rst-order variables in a single operation. For future work, we plan to generalize this algorithm to automata over more expressive structures, such as the automata over linear orders dened in [START_REF] Bruyère | Automata on linear orderings[END_REF]. This would make it possible to obtain an implementable decision procedure for, e.g., the rst-order theory ⟨R, <⟩ with uninterpreted unary predicates [START_REF] Läuchli | On the elementary theory of linear order[END_REF].

  φ 2 and I |= ¬φ i (respectively) (I |= φ 1 ) ∧ (I |= φ 2 ), (I |= φ 1 ) ∨ (I |= φ 2 ), and I ̸ |= φ. I |= ∃x i φ(x 1 , . . . , x k , X 1 , . . . , X ℓ ) i there exists n ∈ N such that I[x i = n] |= φ(x 1 , . . . , x k , X 1 , . . . , X ℓ ).

	I |= ∀x i φ(x 1 , . . . , x k , X 1 , . . . , X ℓ ) i for every n ∈ N, one has I[x i = n] |=
	φ(x 1 , . . . , x k , X 1 , . . . , X ℓ ).

by an Amazon Research Award, Fall 2022 CFP.