Romain Joly

Geneviève Raugel

Generic hyperbolicity of equilibria and periodic orbits of the parabolic equation on the circle

Keywords: Hyperbolicity, genericity, periodic orbits, equilibria, Sard-Smale, lap number AMS subject classification: Primary 35B10, 35B30, 35K57, 37D05, 37D15, 37L45; Secondary 35B40

In this paper, we show that, for scalar reaction-diffusion equations on the circle S 1 , the property of hyperbolicity of all equilibria and periodic orbits is generic with respect to the non-linearity . In other words, we prove that in an appropriate functional space of nonlinear terms in the equation, the set of functions, for which all equilibria and periodic orbits are hyperbolic, is a countable intersection of open dense sets. The main tools in the proof are the property of the lap number and the Sard-Smale theorem.

Introduction

In the local study of the qualitative properties of perturbed dynamical systems, the concepts of non degeneracy and hyperbolicity of equilibria and periodic orbits play a crucial role. Indeed, if one slightly perturbs a continuous dynamical system whose equilibria and periodic orbits are non-degenerate, then at least, the perturbed system still admits equilibria and periodic orbits nearby. If these elements are in addition hyperbolic, then no local bifurcation phenomena occur, which means that the dynamics in the neighborhood of hyperbolic equilibria and periodic orbits is stable under small perturbations. This stability property has practical consequences. For example, it implies that a numerical simulation of the dynamics near a hyperbolic equilibrium or periodic orbit is qualitatively correct. These considerations show that it is important to know if, in a given class of dynamical systems or evolutionary equations, the equilibria and periodic orbits are all hyperbolic or if, at least, this property is generically satisfied. Generic hyperbolicity of equilibrium points and periodic orbits is well-known in the case of 1 diffeomorphisms or vector fields on a compact finite-dimensional manifold (for instance, see Chapter 3 of [START_REF] Palis | Geometric Theory of Dynamical Systems[END_REF] and the references therein). The genericity of hyperbolicity of equilibria and periodic orbits was generalized in 1977 to the case of functional differential equations defined in R n , n ≥ 1, by Mallet-Paret ( [START_REF] Mallet-Paret | Generic periodic solutions of functional differential equations[END_REF]). In the frame of evolutionary partial differential equations, generic hyperbolicity of equilibrium points is also a classical result (see for example, [START_REF] Babin | Attractors of evolution equations[END_REF], [START_REF] Brunovský | Generic properties of stationary state solutions of reaction-diffusion equations[END_REF], [START_REF] Brunovský | The Morse-Smale structure of a generic reactiondiffusion equation in higher space dimension[END_REF], [START_REF] Smoller | Generic properties of steady state solutions[END_REF] for parabolic equations). Notice that this is sufficient for gradient dynamical systems, where no periodic orbits can occur. On the contrary, for autonomous evolutionary partial differential equations, which are not of gradient type, the hyperbolicity of periodic orbits seems to be an open question.

In this paper, we address the question of genericity of hyperbolicity of periodic orbits by considering one of the simplest non-gradient partial differential equations, namely the following scalar reaction-diffusion equation on the one-dimensional torus (or unit circle) S 1 = R/2πZ, given by u t (x, t) = u xx (x, t) + f (x, u(x, t), u x (x, t)) , (x, t) ∈ S 1 × R * + , u(x, 0) = u 0 (x) , x ∈ S 1 , (

where f belongs to the space C 2 (S 1 × R × R, R) and u 0 is given in the Sobolev space H s (S 1 ), with s ∈ (3/2, 2) (so that H s (S 1 ) is continuously embedded into C 1+α (S 1 ) for α = s -3/2). Our purpose is to prove that the equilibria and the periodic orbits of (1.1) are hyperbolic generically with respect to f . We will also consider the more constricting case where the non-linearity is independent of x u t (x, t) = u xx (x, t) + f (u(x, t), u x (x, t)) , (x, t) ∈ S 1 × R * + .

(1.2)

Equations (1.1) and (1.2) are good problems to begin with. Indeed, on one hand these equations may have periodic orbits (see Theorem 2 of [START_REF] Sandstede | Dynamics of periodically forced parabolic equations on the circle[END_REF]) and on the other hand, they are the simplest non-gradient PDE's to study since they admit very special properties as explained below.

In the study of global stability, generic hyperbolicity of closed orbits plays also an important role. Showing genericity of closed orbits is the first step in the proof the genericity of Morse-Smale property. Morse-Smale dynamical systems are systems whose non-wandering set consists only in a finite number of hyperbolic equilibria and hyperbolic periodic orbits and for which the intersections of the stable and unstable manifolds of equilibria and periodic orbits are all transversal. On finite-dimensional compact manifolds, the dynamics of Morse-Smale dynamical systems are globally stable under perturbations, that is, any small regular enough perturbation of a Morse-Smale system is still Morse-Smale and the flows are topologically equivalent (for more details, see [START_REF] Palis | Geometric Theory of Dynamical Systems[END_REF]). In the class of gradient dynamical systems on finite-dimensional compact manifolds, the Morse-Smale property is known to be generic. For the non-gradient dynamical systems, the Morse-Smale property is generic only if the manifold is one-or two-dimensional. In the infinite-dimensional case, the structural stability of Morse-Smale systems remains true under compactness assumptions (for instance, under the assumption that the dynamical systems admit compact global attractors). The genericity of Morse-Smale property has been obtained for some classes of gradient partial differential equations ( [START_REF] Angenent | The Morse-Smale property for a semi-linear parabolic equation[END_REF][START_REF] Henry | Some infinite dimensional Morse-Smale systems defined by parabolic differential equations[END_REF][START_REF] Brunovský | The Morse-Smale structure of a generic reactiondiffusion equation in higher space dimension[END_REF][START_REF] Brunovský | Genericity of the Morse-Smale property for damped wave equations[END_REF][START_REF] Joly | Generic transversality property for a class of wave equations with variable damping[END_REF]). For Morse-Smale non-gradient evolutionary partial differential equations, Equation (1.1) is the right candidate since its asymptotic behaviour in time is analogous to the one of a system of ordinary differential equations in R 2 . Indeed, in [START_REF] Fiedler | A Poincaré-Bendixson theorem for scalar reactiondiffusion equations[END_REF], Fiedler and Mallet-Paret have proved that Equation (1.1) satisfies a Poincaré-Bendixson type property. For non-linearities independent of x, automatic transversality properties have been proved in [START_REF] Fiedler | Heteroclinic orbits between rotating waves of semilinear parabolic equations on the circle[END_REF], by showing that, for (1.2), the Morse-Smale property is equivalent to the hyperbolicity of all closed orbits. The results of the present paper thus imply the genericity of Morse-Smale property for Equation (1.2). In the more general case of Equation (1.1), R. Czaja and C. Rocha have shown in [START_REF] Czaja | Transversality in scalar reaction-diffusion equations on a circle[END_REF] that, if the periodic orbits of (1.1) are all hyperbolic, then their stable and unstable manifolds intersect transversally. Here we will show that this hyperbolicity is generic in the nonlinearity f (x, u, u x ). This shows, together with the results of [START_REF] Czaja | Transversality in scalar reaction-diffusion equations on a circle[END_REF], that the transversality of the stable and unstable manifolds of the periodic orbits of (1.1) is generic with respect to f . Thus, this paper is also a further step towards the proof of genericity of the Morse-Smale property for (1.1). We shall conclude this proof in the forthcoming paper [START_REF] Joly | Generic Morse-Smale property for the parabolic equation on the circle[END_REF].

When the non-linearity f does not explicitly depend on x and is dissipative, the dynamics of Equation (1.2) can be described with more precision. In [START_REF] Angenent | The dynamics of rotating waves in scalar reaction diffusion equations[END_REF], Angenent and Fiedler obtained the following characterization of the closed orbits of (1.2). Proposition 1.1. Any closed orbit u(x, t) of (1.2) is: -either a homogeneous equilibrium point, that is, u(x, t) ≡ e ∈ R where f (e, 0) = 0, -or a rotating wave, that is, u(x, t) = v(xct) with c = 0, -or a frozen wave, that is, u is a non-homogeneous solution of u xx + f (u, u x ) = 0. Moreover, Angenent and Fiedler have proved that the ω-limit set of any element u 0 ∈ H s (S 1 ) contains a rotating wave or a steady state. Under the hypothesis that the rotating waves and equilibria are all hyperbolic, they showed that the ω-limit set consists exactly in one rotating wave or in one equilibrium point and also described the connecting orbits. In [START_REF] Matano | The global attractor of semilinear parabolic equations on S 1[END_REF], Matano and Nakamura proved that there exist neither homoclinic orbits nor heteroclinic cycles. In [START_REF] Fiedler | Heteroclinic orbits between rotating waves of semilinear parabolic equations on the circle[END_REF], Fiedler, Rocha and Wolfrum, using the notion of "adjacency", have characterized connecting orbits under the hypothesis that the rotating waves and equilibria are hyperbolic. They also gave an equivalent characterization of the property of hyperbolicity of rotating waves. Thus, the generic hyperbolicity of the closed orbits of (1.2) is primordial to conclude that the dynamics described in these papers include every possible dynamics, except maybe some exceptional ones.

Finally, let us recall that, if the periodic boundary conditions are replaced by homogeneous Dirichlet or Neumann boundary ones, then the dynamical system S(t) associated with (1.1) is of gradient type and the ω-limit set of any point is exactly one equilibrium point (see [START_REF] Zelenyak | Stabilization of solutions of boundary value problems for a second order parabolic equation with one space variable[END_REF]). Moreover, in these cases, as shown by D. Henry [START_REF] Henry | Some infinite dimensional Morse-Smale systems defined by parabolic differential equations[END_REF] and later by S. Angenent [START_REF] Angenent | The Morse-Smale property for a semi-linear parabolic equation[END_REF], the stable and unstable manifolds of the equilibria intersect transversally, provided they are all hyperbolic. Thus, the Morse-Smale property is generic in the class of one-dimensional scalar parabolic equations on the segment with Dirichlet or Neumann boundary conditions. In a series of papers, Fiedler and Rocha have described the different equivalence classes of attractors and, in particular, the heteroclinic orbits connecting the equilibria (see [START_REF] Fiedler | Heteroclinic orbits of semilinear parabolic equations[END_REF], [START_REF] Fiedler | Orbit equivalence of global attractors of semilinear parabolic differential equations[END_REF], for example). Now we are going to precisely state the genericity results proved in this paper. We set

G = C 2 (S 1 × R × R, R
) and we endow G with the Whitney topology, that is, the topology generated by the neighborhoods

{g ∈ G / |D i f (x, u, v)-D i g(x, u, v)| ≤ δ(u, v), ∀i ∈ {0, 1, 2}, ∀(x, u, v) ∈ S 1 ×R 2 } , (1.3)
where f is any function in G and δ is any positive continuous function (see [START_REF] Golubitsky | Stable mapping and their singularities[END_REF]). It is well known that G is a Baire space, which means that any generic set, that is any countable intersection of open and dense sets, is dense in G (see [START_REF] Golubitsky | Stable mapping and their singularities[END_REF] for instance).

In the general case, when f depends also on the variable x, we prove the following genericity result (for the definition of hyperbolicity we refer the reader to Section 2 below).

Theorem 1.2. There exists a generic subset O of G such that, for all f ∈ O, all the equilibrium points and all the periodic solutions of (1.1) are hyperbolic. Remarks 1.3. 1) The above theorem is also valid if, in the equation (1.1), we replace the Laplacian -∂ xx by the self-adjoint operator -a(x)∂ xx or -a(x) -1 (∂ x (a(x)∂ x •)), where a(x) > 0 is a C 1function on S 1 . 2) In Theorems 1.2 and 1.4, we assume for sake of simplicity that f is of class C 2 in all the variables. Actually, we can begin with a nonlinearity f , which is less regular, and immediately replace it by a small perturbation f 0 , which is in

C 2 (S 1 × R × R, R).
As we already mentioned, it is also interesting to consider a non-linearity f , which is independent of x. Even if the choice of such non-linearity is more constrained, this case is not more difficult than the general case due to the particular properties coming from the S 1 -equivariance of (1.2). In Section 5, we prove the following genericity result. Theorem 1.4. Let G i be the subspace of G consisting of functions independent of x. There exists a generic subset O i of G i such that, for all f ∈ O i , (1.2) has no frozen waves and any homogeneous equilibrium or rotating wave of (1.2) is hyperbolic. Remark 1.5. In [START_REF] Fiedler | Heteroclinic orbits between rotating waves of semilinear parabolic equations on the circle[END_REF], the generic hyperbolicity of homogeneous equilibria and rotating waves is asserted, based on a personal communication of P. Brunovský.

There are two main ingredients in the proof of Theorems 1.2 and 1.4. The first one, as expected in genericity properties, is the Sard-Smale Theorem that we recall in the appendix. The second main ingredient is the Sturm property (also called zero number or lap number property). This property originated in the paper of Sturm [START_REF] Sturm | Sur une classe d'équations à différences partielles[END_REF] (see also [START_REF] Matano | Nonincrease of the lap-number of a solution for a one-dimensional semilinear parabolic equation[END_REF] and [START_REF] Angenent | The zero set of a solution of a parabolic equation[END_REF] for more recent results, mainly in the case where f is not analytic). For any ϕ ∈ C 1 (S 1 ), we define the zero number z(ϕ) as the (even) number of strict sign changes of ϕ. Let I be an open subinterval of R and let v(x, t) be a solution of the linear parabolic equation

v t = v xx + b(x, t)v + d(x, t)v x , (1.4)
where b, b x , b t and d are bounded functions on any compact subset of S 1 ×I. Then z(v(•, t)) is finite, for any t > 0, and nonincreasing with t. Moreover, the zero number z(v(•, t)) drops strictly at t = t 0 , if and only if there exists

x 0 ∈ S 1 such that v(x 0 , t 0 ) = 0 , ∂ x v(x 0 , t 0 ) = 0 . (1.5)
In Section 2.3, we will see that these remarkable properties of the zero number imply also special spectral properties for the linearized equation associated with (1.1). In the proof of Theorem 1.2, it will also play an important role. Finally, we point out that the zero number property has been widely used in all the above mentioned papers dealing with the description of the dynamics of a scalar one-dimensional equation.

The paper is organized as follows. In Section 2, we give the main spectral properties of the linearized equations around the equilibria and the periodic solutions of (1.1). Section 3 contains the proof of the genericity of the hyperbolicity of the equilibria of (1.1), while Section 4 is devoted to the genericity of the hyperbolicity of the periodic orbits of (1.1). In Section 5, we consider the special case of equation (1.2) and prove Theorem 1.4. Finally, in the appendix, we recall the Sard-Smale theorem, that we apply here.

Acknowledgements: The authors wish to thank P. Brunovský, R. Czaja and C. Rocha for fruitful discussions with them.

Spectrum of the linearized operators

The notions of non-degeneracy and hyperbolicity of equilibria and periodic orbits of an evolutionary equation are related to the spectral properties of the linearized equations around these elements. In this section, we will recall these notions and describe several properties of the linearized equations associated with (1.1).

Let p be either an equilibrium point e or a periodic orbit p 0 (x, t) of (1.1). We consider the linearized equation

ϕ t = ϕ xx + D u f (x, p, p x )ϕ + D ux f (x, p, p x )ϕ x , ϕ(x, 0) = ϕ 0 (x) .
(2.1)

Let s ∈ (3/2, 2); we introduce the operator U(t, 0) : H s (S 1 ) -→ H s (S 1 ), defined by U(t, 0)ϕ 0 = ϕ(t) where ϕ(t) is the solution of the linearized equation (2.1). Sometimes, if needed, we will also denote the operator U(t, 0) by U p,f (t, 0).

The case of equilibria

Let e ∈ H s (S 1 ) be an equilibrium point of (1.1), that is a solution of e xx + f (x, e, e x ) = 0. Due to the classical elliptic estimates and the regularity of f , the equilibrium e belongs to H s+2 (S 1 ). In the case where p = e is an equilibrium point, the linearized operator U(t, 0) is an analytic semigroup generated by the linear operator

L e = ∂ 2 xx + f ′ u (x, e, e x ) + f ′ ux (x, e, e x )∂ x : H 2 (S 1 ) → L 2 (S 1 ) , (2.2)
that is, U(t, 0) = e Let . The general definitions of simplicity and hyperbolicity are as follows.

Definition 2.1. 1) We say that an equilibrium point e is simple if 0 belongs to the resolvent set of the operator L e .

2) We say that e is a hyperbolic equilibrium point if the intersection of the spectrum σ(U(t, 0)) of U(t, 0) with the unit circle S 1 in the complex plane is the empty set.

Since L e is a Fredholm operator and also a sectorial operator, simple characterizations of the notions of simplicity and hyperbolicity can be given (for the properties of Fredholm operators, see for example [START_REF] Bonic | Linear functional analysis[END_REF]).

Lemma 2.2. Let e be any equilibrium point of (1.1).

1) The operator L e : H 2 (S 1 ) -→ L 2 (S 1 ) is a Fredholm operator of index 0. As a consequence, we have the following obvious equivalences:

e is simple ⇔ Ker L e = {0} ⇔ L e is surjective 2) U(t, 0) : H s (S 1 ) -→ H s (S 1
) is compact and so e is hyperbolic ⇔ no eigenvalue of L e belongs to the imaginary axis.

3) The operator L e is a sectorial operator with compact resolvent. Moreover, the sector is locally uniform in the sense that, for any f ∈ G and any equilibrium point e of (1.1), there exist positive constants C and C ′ uniform in a neighborhood of (e, f ) in

H s (S 1 ) × G such that, for any eigenvalue λ of L e , |Im(λ)| ≤ C -C ′ Re(λ) . (2.3) Proof. 1) Since e ∈ H 2 (S 1 ), ϕ -→ ϕ + f ′ u (x, e, e x )ϕ + f ′ ux (x, e, e x )ϕ x is bounded from H 2 (S 1 ) into H 1 (S 1 ). Thus, L e is a compact perturbation of ∂ 2 xx -Id : H 2 (S 1 ) → L 2 (S 1 ). Since ∂ 2
xx -Id is bijective, it is a Fredholm operator of index 0, which implies that L e is also a Fredholm operator of index 0.

2) Since L e : H 2 (S 1 ) → L 2 (S 1 ) is a real operator with compact resolvent, its spectrum consists in a sequence of eigenvalues of finite multiplicity and its spectrum is symmetric with respect to the real axis. Due to the smoothing properties of the parabolic flow, e Le is a compact operator, thus its spectrum consists in {0} and a sequence of eigenvalues with finite multiplicity converging to 0. Hence, due to the spectral mapping theorem (see theorems 2.2.3 and 2.2.4 of [START_REF] Pazy | Semigroups of Linear Operators and Applications to Partial Differential Equations[END_REF] for example),

exp(tσ(L e )) ⊂ σ(e Let ) ⊂ exp(tσ(L e )) ∪ {0} , ∀ t ≥ 0 , (2.4)
which clearly implies the equivalence.

3) Moreover, L e is the perturbation of the self-adjoint operator

∂ 2 xx + f ′ u (
x, e, e x ) by the term f ux (x, e, e x )∂ x . Therefore, it is a sectorial operator by Theorem 3.2.1 of [START_REF] Pazy | Semigroups of Linear Operators and Applications to Partial Differential Equations[END_REF] or by Theorem 1.3.2 of [START_REF] Henry | Geometric theory of semilinear parabolic equations[END_REF]. The fact that the sector is locally uniform in (e, f ) and the estimate (2.3) are straightforward consequences of the proof of Theorem 1.3.2 of [START_REF] Henry | Geometric theory of semilinear parabolic equations[END_REF]. In Section 2.3 below, we will prove special spectral properties of general scalar onedimensional linear parabolic equations. As a direct consequence of the spectral theorem and of Theorem 2.6 and Proposition 2.7 below, we obtain the following interesting spectral property, that we will apply in the proof of the genericity theorems.

Proposition 2.3. Let e be any equilibrium point of (1.1). Then, the dimension of the generalized eigenspace corresponding to the eigenvalues of L e with same real part is at most two. Moreover, if λ is a real eigenvalue of L e , then there exists no other eigenvalue of L e with real part equal to λ.

The case of periodic orbits

In this section, we consider the non-trivial time-periodic solutions of Equation (1.1). Let p = p 0 (x, t) be a periodic solution of (1.1) of period T 0 > 0. We recall that U(t, 0) ≡ U f (t, 0) denotes the linear operator associated with (2.1) and that, since p 0 (t) is of period T 0 , U(T 0 , 0) is called the period map. Notice that, since p 0 (t) is a periodic solution with period T 0 of the autonomous equation (1.1), µ = 1 is automatically an eigenvalue of U(T 0 , 0) with eigenfunction ∂ t p 0 (0). Definition 2.4. Let p 0 (t) be a periodic solution of (1.1), with period T 0 > 0. 1) We say that p 0 (t) is a simple or non-degenerate periodic orbit if the eigenvalue µ = 1 is simple and isolated from the rest of the spectrum. Then, T 0 is called a simple period.

2) We say that p 0 (t) is hyperbolic if the eigenvalue µ = 1 is simple and if the intersection of the spectrum of U(T 0 , 0) with the unit circle reduces to the eigenvalue 1.

Remark that, since the equation (2.1) is smoothing in finite time, U(T 0 , 0) is a compact map from H s (S 1 ) into itself. Therefore, the spectrum of U(T 0 , 0) consists of 0 and a sequence of eigenvalues µ k converging to 0. Thus, p 0 (t) is a hyperbolic periodic orbit if µ = 1 is the only eigenvalue of U(T 0 , 0) on the unit circle and is simple. Several properties of the spectrum of U(T 0 , 0) are described in Section 2.3 below. In particular, as a direct consequence of Theorem 2.6, Proposition 2.7 and the fact that µ = 1 is an eigenvalue of U(T 0 , 0), we obtain the following result.

Proposition 2.5. Let p 0 (t) be a periodic orbit of (1.1) of period T 0 . Then, µ = 1 is an eigenvalue of the period map U(T 0 , 0) of multiplicity at most 2 and there is no other eigenvalue on the unit circle. As a consequence, we have the equivalence:

p 0 (t) is hyperbolic ⇔ p 0 (t) is simple.
Nota Bene: For more general equations than (1.1), if for example, µ = exp 2iπ/n is an eigenvalue of U(T 0 , 0), the periodic orbit p 0 (t), considered as periodic solution of period nT 0 , will not be simple. So, in general, the definition of simplicity can depend on the chosen period, whereas the definition of the hyperbolicity does not depend on the chosen period. This will not be the case here. Indeed, let p 0 (t) be a periodic solution of (1.1) with minimal period T 0 . Proposition 2.5 implies that the generalized eigenfunctions associated to the eigenvalue µ = 1 of the map U(nT 0 , 0) are exactly the eigenfunctions associated to the eigenvalue µ = 1 of the period map U(T 0 , 0).

Spectrum of a general linear operator

In this section, we consider a more general linear equation. Let T > 0 be any positive time. Let a and b be two functions in C 1 (S 1 × [0, T ], R). We consider the operator U(T, 0) : H s (S 1 ) -→ H s (S 1 ) defined by U(T, 0)w 0 = w(T ) where w(t) is the solution of

∂ t w(x, t) = ∂ 2 xx w(x, t) + a(x, t)w(x, t) + b(x, t)∂ x w(x, t) , ∀(x, t) ∈ S 1 × (0, T ] w(x, 0) = w 0 (x) .
(2.5)

Due to the classical smoothing properties of parabolic equations, U(T, 0) is a compact operator from H s (S 1 ) into itself. Thus, the spectrum consists in {0} and a sequence of nonzero eigenvalues of finite multiplicity converging to 0. Notice that 0 is not an eigenvalue due to the backward uniqueness property of the parabolic equation. We denote by (λ k ) k∈N the eigenvalues of U(T, 0) with the convention that they are repeated according to their multiplicity and ordered by

|λ k+1 | ≤ |λ k |.
Using the properties of the zero number, Angenent ([2]) has shown the following result (a first statement with a and b analytic was proved in [START_REF] Angenent | The dynamics of rotating waves in scalar reaction diffusion equations[END_REF]).

Theorem 2.6. Let (λ k ) k∈N be the spectrum of U(T, 0) as introduced above.

Then, for all j ≥ 0, |λ 2j | > |λ 2j+1 |. In particular, λ 0 is a simple real eigenvalue. Moreover, let E 0 denote the one-dimensional eigenspace corresponding to λ 0 and for j ≥ 1, let E 2j denote the two-dimensional real generalized eigenspace corresponding to {λ 2j-1 , λ 2j }.

Then, for all j ≥ 0, any nonzero real function v ∈ E 2j has exactly 2j zeros and all these zeros are simple.

Assume that λ is a real eigenvalue and that µ is another eigenvalue such that |λ| = |µ|. Since a and b are real functions, µ is also an eigenvalue. Theorem 2.6 shows that there are at most two eigenvalues with same modulus, thus µ is also real. It could be possible that µ = -λ, but the following result prevents this case.

Proposition 2.7. Let j ≥ 1. If λ 2j-1 and λ 2j are two consecutive eigenvalues of U(T, 0), then λ 2j-1 λ 2j > 0. In particular, if λ is a real eigenvalue then -λ is not an eigenvalue and there is no other distinct eigenvalue on the circle {z ∈ C, |z| = |λ|}.

Proof. Due to Theorem 2.6, there are at most two eigenvalues with same modulus (counting multiplicity). Since the spectrum is symmetric with respect to the imaginary axis, if λ 2j-1 or λ 2j is not real, then both must be conjugated and λ 2j-1 λ 2j = |λ 2j | 2 > 0. For the same reason, it is also clear that the last assertion of Proposition 2.7 is a direct consequence of the first one. The only case, which has to be studied, is the case when λ 2j-1 and λ 2j are both real. We argue by contradiction: assume that λ 2j-1 and λ 2j are real eigenvalues of U(T, 0) of opposite signs. We denote by U ε (T, 0) the evolution operator corresponding to

∂ t w(x, t) = ∂ 2 xx w(x, t) + εa(x, t)w(x, t) + εb(x, t)∂ x w(x, t) , ∀(x, t) ∈ S 1 × (0, T ] . (2.6)
We denote by (λ ε k ) k∈N the set of eigenvalues of U ε (T, 0). We set

E = {ε ∈ [0, 1] | λ ε 2j-1 and λ ε 2j are real eigenvalues of U ε (T, 0) of opposite signs} .
By assumption, 1 ∈ E and trivially 0 ∈ E. We will obtain a contradiction by showing that E is open and closed. Openness: let ε 0 ∈ E. Since λ ε 0 2j and λ ε 0 2j-1 are different, they must be simple due to Theorem 2.6. Let ϕ ε 0 2j and ϕ ε 0 2j-1 be two corresponding normalized real eigenfunctions. They have 2j simple zeros. The simplicity of the eigenvalues and the implicit function theorem imply that there exists a neighborhood V of ε 0 and functions µ 1 (ε), µ 2 (ε), ψ 1 (ε) and ψ 2 (ε) defined on V such that the following properties hold. The functions

µ i are of class C 0 (V, R), µ 1 (ε 0 ) = λ ε 0 2j-1 , µ 2 (ε 0 ) = λ ε 0 2j and µ i (ε) is a simple real eigenvalue of U ε (T, 0). The functions ψ i are of class C 0 (V, H s (S 1 )), ψ 1 (ε 0 ) = ϕ ε 0 2j-1 , ψ 2 (ε 0 ) = ϕ ε 0 2j and ψ i (ε)
is the normalized real eigenfunction corresponding to µ i (ε). Since the zeros of all eigenfunctions of U ε (T, 0) are simple and H s (S 1 ) ⊂ C 1 (S 1 ), restricting V if necessary, we can assume that ψ i (ε) has exactly 2j zeros which are all simple. Due to Theorem 2.6, this shows that for all ε ∈ V, the eigenvalues µ i (ε) are the eigenvalues λ ε 2j-1 and λ ε 2j of U ε (T, 0). Moreover, the eigenvalues of U ε (T, 0) cannot be zero due to the backward uniqueness property of (2.6). Thus, up to a restriction of V, the eigenvalues µ i (ε) are of opposite signs and V ⊂ E. Closeness: assume that (ε n ) ⊂ E is a given sequence such that ε n -→ ε. We first consider the sequence of eigenvalues λ εn 2j and the sequence of corresponding real eigenfunctions ϕ εn 2j with ϕ εn 2j L 2 (S 1 ) = 1. Taking the inner product in L 2 of (2.6) with w, integrating in time and applying Gronwall Lemma, we show that there exists a positive constant C 0 independent of ε such that every solution w of (2.6) satisfies

w(T ) L 2 (S 1 ) ≤ C 0 w(0) L 2 (S 1 ) .
Thus, |λ εn 2j | is bounded by C 0 and, up to the extraction of a subsequence, we can assume that λ εn 2j converges to µ. First, µ cannot be zero. Indeed, there exists a closed curve Γ ⊂ C \ {0} surrounding the 2j + 2 first eigenvalues of U ε (T, 0) but not zero. The projector

P 2j+2 = - 1 2iπ Γ (U ε (T, 0) -z) -1 dz
is the spectral projector of U ε (T, 0) onto the space generated by the first 2j + 2 eigenvalues. Thus, for n large enough

P n 2j+2 = - 1 2iπ Γ (U εn (T, 0) -z) -1 dz
is a spectral projector of rank 2j + 2 and thus Γ still surrounds 2j + 2 eigenvalues of U εn (T, 0). Due to the ordering |λ 0 | ≥ |λ 1 | ≥ ..., this shows that λ εn 2j must be away from zero for large n. Next, using the smoothing property of parabolic equations shows that there exists a positive constant constant C 1 independent of ε such that every solution w of (2.6) satisfies w(T ) H 2 (S 1 ) ≤ C 1 w(0) L 2 (S 1 ) .

Therefore,

|λ εn 2j | ϕ εn 2j H 2 (S 1 ) ≤ C 1 ϕ εn 2j L 2 (S 1 ) = C 1 . Since λ εn 2j is bounded away from zero, (ϕ εn 2j ) is bounded in H 2 (S 1
) and we can assume that (ϕ εn 2j ) converges to a function ψ in C 1 (S 1 ). Passing to the limit, we see that µ is a real eigenvalue of U ε (T, 0) with normalized eigenfunction ψ. Due to Theorem 2.6, ψ has simple zeros only and since (ϕ εn 2j ) converges to ψ in C 1 (S 1 ), the number of zeros of ψ must be 2j. Hence, µ must be equal either to λ ε 2j or to λ ε 2j-1 . Arguing in the same way for λ εn 2j-1

we show that, up to the extraction of a subsequence, λ εn 2j and λ εn 2j-1 converge to λ ε 2j or λ ε 2j-1 . Since neither λ ε 2j nor λ ε 2j-1 can be zero and since λ εn 2j λ εn 2j-1 < 0, both λ ε 2j and λ ε 2j-1

are limits of one of the sequences (λ εn 2j ) or (λ εn 2j-1 ) and thus are real and of opposite signs. Therefore, ε belongs to E. All these properties yield a contradiction since [0, 1] is connected. The proposition is proved.

3 Generic hyperbolicity of the equilibrium points 3.1 Generic simplicity Generic simplicity of equilibria has been proved for various parabolic systems, including the Navier-Stokes equations, in different settings (see [START_REF] Quinn | Transversal approximation on Banach manifolds[END_REF], [START_REF] Saut | Generic properties of nonlinear boundary value problems[END_REF], [START_REF] Smoller | Generic properties of steady state solutions[END_REF], [START_REF] Babin | Attractors of evolution equations[END_REF], [START_REF] Brunovský | Generic properties of stationary state solutions of reaction-diffusion equations[END_REF], [START_REF] Brunovský | The Morse-Smale structure of a generic reactiondiffusion equation in higher space dimension[END_REF] for example). Since the proof is rather simple, we include it here for sake of completeneness. We follow the lines of the proof given by [START_REF] Brunovský | The Morse-Smale structure of a generic reactiondiffusion equation in higher space dimension[END_REF] in the case where f does not depend on the derivative u x .

Rg = g |S 1 ×[-(n+2),n+2]×[-(n+2),n+2] .
We notice that R is a continuous, surjective map and that, on

RG = C 2 (S 1 ×[-(n+ 2), n+ 2] × [-(n + 2), n + 2], R),
(f k ) is a sequence of functions in G \ O simp n converging to f in C 2 (S 1 × [-(n + 2), n + 2] × [-(n + 2), n + 2], R), then f belongs to G \ O simp n . Assume that (f k ) is such a sequence of functions in G \ O simp n converging to f . Due to Lemma 2.2, there exist a sequence of equilibria (e k ) with e k C 1 ≤ n and a sequence of functions (ϕ k ) ⊂ H 2 (S 1 ) with ϕ k L 2 = 1 and L e k ϕ k = 0. Since |∂ x ϕ k | 2 = D u f k (x, e k , ∂ x e k )|ϕ k | 2 + D ux f k (x, e k , ∂ x e k )∂ x ϕ k ϕ k , the sequence (ϕ k ) is bounded in H 1 (S 1 ). Moreover, ∂ 2 xx e k = f k (x, e k , ∂ x e k
) and thus the sequence (e k ) is bounded in H s+2 (S 1 ). Up to the extraction of a subsequence, we can assume that (e k ) converges in H 2 (S 1 ) to e and (ϕ k ) converges in L 2 (S 1 ) to ϕ. Passing to the limit, we obtain L e ϕ = 0 and e C 1 ≤ n. By elliptic estimates, ϕ ∈ H 2 (S 1 ), thus f ∈ O simp n , and so O simp n is open. O simp n is dense: let f ∈ G be given. We follow the now classical method (see [START_REF] Brunovský | The Morse-Smale structure of a generic reactiondiffusion equation in higher space dimension[END_REF] for example). We introduce a function χ

∈ C 2 (R 2 , R) satisfying χ ≡ 1 in [-n -1, n + 1] 2 and χ ≡ 0 in R \ [-n-2, n+2] 2 .
For any open neighborhood V of f in G, there exists an open neighborhood U of 0 in C 2 (S 1 ) such that, for all a ∈ U, the function (x, u, v) → f (x, u, v) + a(x)χ(u, v) belongs to V. So, it is sufficient to prove that there is a dense set of functions a ∈ C 2 (S 1 , R) such that f + aχ ∈ O simp n . To obtain this density, we apply Sard-Smale Theorem (Theorem A.1 in the appendix), to the functional Φ : (e, a)

∈ {e ∈ H 2 (S 1 ), e C 1 < n + 1} × C 2 (S 1 , R) → Φ(e, a) ∈ L 2 (S 1
) defined by Φ(e, a) = e xx + f (x, e, e x ) + a(x)χ(e, e x ) and to the point z = 0. Assumption iii) of Theorem A.1 is satisfied. To simplify the notation, let us prove i) and ii) with a = 0, which does not lead to any loss of generality. First notice that (e, 0) ∈ Φ -1 (0) means that e is an equilibrium point of (1.1). Assumption i) of Theorem A.1 is satisfied since D e Φ(e, 0) = L e is a Fredholm operator of index 0 due to Lemma 2.2. To prove ii), we must find for each h ∈ L 2 (S 1 ) a pair (ϕ, b) such that D e,a Φ(e, 0).

(ϕ, b) = L e ϕ + b(x)χ(e, e x ) = L e ϕ + b(x) = h. Since L e is Fredholm, h -b ∈ Im(L e ) if and only if, for all ψ ∈ Ker(L * e ), (h -b)ψ = 0. As Ker(L * e
) is finite-dimensional, we can introduce a finite orthonormal basis (ψ i ) i=1...p of Ker(L * e ). We are reduced to find b such that (hb)ψ i = 0 for all i = 1, . . . , p that is, so that 0 belongs to the image of the map: b ∈ C 2 (S 1 ) -→ ( (hb)ψ i ) i=1...p . This image is closed since it is an affine subspace of R p and by density of C 2 in L 2 , we can find b as close to h as wanted. Therefore, we can find b such that (hb)ψ i = 0 for all i = 1, . . . , p and thus D e,a Φ is surjective. Actually, remarking that the vectors ψ i belong to H 3 (S 1 ), we can simply choose b = p 0 (h, ψ i )ψ i . The conclusion of Theorem A.1 shows that for a generic a ∈ C 2 (S 1 ), any e satisfying e C 1 ≤ n and e xx + f (x, e, e x ) + a(x)χ(e, e x ) = 0 is such that D e Φ = L e is surjective which implies by Lemma 2.2 that e is a simple equilibrium point. Thus, we can choose a function a as small as wanted such that f + aχ ∈ O simp n , which shows that O simp n is dense.

Generic hyperbolicity

In Proposition 3.1, we have proved the generic simplicity of the equilibrium points of (1.1). Using this result, it is not difficult to show the generic hyperbolicity.

O h n is open: As in the proof of Proposition 3.1, it is sufficient to prove that if (f k ) is a se- quence of functions in G\O h n converging to f in C 2 (S 1 ×[-(n+2), n+2]×[-(n+2), n+2], R), then f belongs to G \ O h n . So let (f k ) be such a sequence of functions in G \ O h n converging to f . Then there exist sequences (e k ) ⊂ H s+2 (S 1 ), (λ k ) ⊂ iR and (ϕ k ) ⊂ H 2 (S 1 ) such that ∂ 2 xx e k + f k (x, e k , ∂ x e k ) = 0, e k C 1 ≤ n, ϕ k L 2 = 1 and L e k ϕ k = λ k ϕ k .
As in the proof of Proposition 3.1, we can assume that (e k ) converges in H 2 (S 1 ) to a function e. Then, the proof of openness will be exactly the same as the corresponding one in Proposition 3.1 as soon as we show that there exists a subsequence (λ kn ) ⊂ iR, which is convergent. This is a consequence of Estimate (2.

3). O h

n is dense: let f 0 ∈ G. We are going to show that we can construct successive perturbations of f 0 , as small as needed, to obtain a function f ∈ O h n as closed to f 0 as is wanted. First, due to Proposition 3.1, we can find f 1 close to f 0 such that all equilibrium points of f 1 are simple. The set {e | ∂ 2 xx e + f 1 (x, e, e x ) = 0, e C 1 ≤ n + 1} is bounded in H s+2 (S 1 ) and hence compact in H 2 (S 1 ). Since all equilibrium points of f 1 are simple and thus isolated, there is a finite number of equilibria e 1 , . . . , e p of f 1 which satisfy e j C 1 ≤ n + 1. We next explain how each equilibrium e i can be made hyperbolic by successive perturbations of f 1 . Let e be an equilibrium point of (1.1) with e C 1 ≤ n and let us denote (λ k ) k∈N the sequence of eigenvalues of the corresponding linearized operator L e . Let χ ∈ C 2 (R, R) be a smooth cut-off function such that, for example, χ(y) = y for |y| ≤ n + 1 and χ(y) = 0 for |y| ≥ n + 2. Then, χ(e(x)) = e(x) for any x ∈ S 1 . If we perturb f 1 by setting for small α ∈ R, f α (x, v, w) = f 1 (x, v, w) + α(χ(v) -e(x)), then e is still an equilibrium point of (1.1) with f replaced by f α and the spectrum of L e becomes (λ k +α) k∈N . Since the eigenvalues of L e are isolated, this means that one can perturb f 1 such that L e has no longer eigenvalues on the imaginary axis, that is, such that e becomes hyperbolic. On the other hand, by the implicit functions theorem, if e is a simple (resp. a hyperbolic) equilibrium of f , there exist neighborhoods V ⊂ C 1 (S 1 ) of e and U ⊂ G of f such that for all g ∈ U, there exists a unique equilibrium point e(g) ∈ V and this equilibrium is simple (resp. hyperbolic). Thus, we can make successively each equilibrium hyperbolic without changing the status of the other equilibria e 1 , . . . , e p .

Generic hyperbolicity of the periodic orbits

The aim of this section is the proof of the genericity theorem 1.2, that is, we want to show that there exists a subset O of G such that, for all f ∈ O, all the equilibrium points and all the periodic solutions of (1.1) are hyperbolic.

To show Theorem 1.2, we use the induction argument of Peixoto [START_REF] Peixoto | On an approximation theorem of Kupka and Smale[END_REF] in the case of vector fields on compact manifolds or of Mallet-Paret [START_REF] Mallet-Paret | Generic periodic solutions of functional differential equations[END_REF] in the case of functional differential equations. Thus, for any n ≥ 1 and any A > 0, we introduce the set

O(A, n) ={f ∈ O h
n | all nonconstant periodic orbits p(t) of (1.1) with period T ∈ (0, A] such that sup t∈R p(t) C 1 (S 1 ) ≤ n are non-degenerate} .

Due to Proposition 2.5, we have the following equality:

O(A, n) ={f ∈ O h
n | all nonconstant periodic orbits p(t) of (1.1) with period T ∈ (0, A] such that sup t∈R p(t) C 1 (S 1 ) ≤ n are hyperbolic}.

As in [START_REF] Peixoto | On an approximation theorem of Kupka and Smale[END_REF] and in [START_REF] Mallet-Paret | Generic periodic solutions of functional differential equations[END_REF], we show that

O(n, n) is open and dense in G. Since G is a Baire space, it follows that O = ∩ ∞ n=1 O(n, n
) is a generic subset and hence a dense subset of G, which proves Theorem 1.2.

Let n ∈ N be fixed for the remaining part of the section. We first begin with auxiliary results, which will be widely used in this section. In particular, we prove that, for any A > 0,O(A,n) is open. To simplify our statements below, we denote by S f (t) the local nonlinear semigroup defined by the equation (1.1) with nonlinearity f . n and let δ be as in (a). For any A > 0, there exist a positive constant r and a neighborhood N 2 ⊂ O h n+δ of f such that the following property holds. Let E f,n+δ be the set of the equilibrium points e f of S f (t) satisfying e f C 1 (S 1 ) ≤ n + δ and let BE(f, n + δ, r) = ∪ e f ∈E f,n+δ B H s (S 1 ) (e f , r). For any g ∈ N 2 , E g,n+δ ⊂ BE(f, n + δ, r) and the set of all nonconstant periodic orbits p(t) of S g (t) of period less than A and satisfying sup t∈R p(t) C 1 (S 1 ) ≤ n + δ does not intersect BE(f, n + δ, r).

Proof. The proof of property (a) is similar to the proof of the openness of O simp n in Proposition 3.1.

To prove property (b), we follow the lines of the proof of Theorem 2.1 of [START_REF] Mallet-Paret | Generic periodic solutions of functional differential equations[END_REF]. By the remarks made at the beginning of the proof of Proposition 3.

1, it is sufficient to prove that, if f m is a sequence of functions in G \ O(A, µ) converging to f in C 2 (S 1 × [-(µ + 2), µ + 2] × [-(µ+2), µ+2], R), then f belongs to G\O(A, µ). So assume that f m is such a sequence of functions in G \ O(A, µ) converging to f in C 2 (S 1 × [-(µ + 2), µ + 2] × [-(µ + 2), µ + 2], R).
Then, for any m, there exists a non-simple periodic solution p m (t) of

u t (x, t) = u xx (x, t) + f m (x, u, u x ) , (x, t) ∈ S 1 × R * + , (4.1)
with non-simple period T m ∈ (0, A). Moreover, p m (t) satisfies the following bound

sup t p m (t) C 1 (S 1 ) ≤ µ . (4.2)
Due to the smoothness hypotheses made on f and to the bound (4.2), we can show by a recursion argument that the function p m (t) belongs to C 1 ([0, 2A], H s (S 1 ))∩C 0 ([0, 2A], H 2 (S 1 )) and that there exists a positive constant C 0 such that , for any m ∈ N,

p m (t) C 1 ([0,2A],H s (S 1 ))∩C 0 ([0,2A],H 2 (S 1 )) ≤ C 0 . (4.3)
Thus, the family of mappings p m (t)

∈ C 1 ([0, 2A], H s (S 1 )), m ∈ N is equicontinuous from [0, A] into H s (S 1 )
. By the Ascoli theorem, there exists a subsequence (p m j (t)) which converges to a function p(t) in C 0 ([0, 2A], H s (S 1 )) and p(t) belongs to C 0 ([0, 2A], H s (S 1 )). Furthermore,

f m j (x, p m j (t), ∂ x p m j (t)) converges to f (x, p(t), ∂ x p(t)) in C 0 ([0, 2A], L 2 (S 1 )).
Taking now the limits in the variation of constants formula

p m j (t) = e Bt p m j (0) + t 0 e B(t-s) (p m j (s) + f m j (x, p m j (s), ∂ x p m j (s)))ds ,
where B is the selfadjoint operator B = ∂ xx -I, we conclude that p(t) is a mild solution of (1.1) on the time interval [0, 2A] that is, of the equation

p(t) = e Bt p(0) + t 0 e B(t-s) (p(s) + f (x, p(s), ∂ x p(s)))ds . (4.4)
Since p m (t) is a periodic solution of period T m ≤ A, we also conclude that p(t) is a periodic solution of (1.1) of period T * = lim m→+∞ T m and the integral equality (4.4) holds on R + . Furthermore p(t) is a classical solution of (4.4). We next consider the linearized equations

ϕ t (x, t) = ϕ xx (x, t) + D u f m (x, p m , ∂ x p m )ϕ + D ux f m (x, p m , ∂ x p m )ϕ x , ϕ(x, 0) = ϕ 0 (x) . (4.5)
as well as the associated linear operators U m (t, 0) defined by U m (t, 0)ϕ 0 = ϕ m (t) where ϕ m (t) is the solution of (4.5). We recall that U m (T m , 0) :

H s (S 1 ) → H s (S 1
) is a compact map. By assumption, the element 1, which belongs to the spectrum σ(U m (T m , 0)) of U m (T m , 0), is of multiplicity greater than one. We also consider the operator U(t, 0) associated to the limiting linearized equation

ϕ t (x, t) = ϕ xx (x, t) + D u f (x, p, ∂ x p)ϕ + D ux f (x, p, ∂ x p)ϕ x , ϕ(x, 0) = ϕ 0 (x) .
Since p m j (t) converges to a function p(t) in C 0 ([0, 2A], H s (S 1 )) and that f m converges to

f in C 2 (S 1 × [-(µ + 2), µ + 2] × [-(µ + 2), µ + 2]
, R), we easily prove that the operator U m j (t, 0) converges to U(t, 0) in L(H s (S 1 ), H s (S 1 )), uniformly in t ∈ [0, 2A]. Assume that T * = 0. Then, U m j (T m j , 0) converges to U(T * , 0) in L(H s (S 1 ), H s (S 1 )). Now three cases may arise: 1) the periodic orbit p(t) is nonconstant and T * > 0. The element 1 ∈ σ(U(T m , 0)) has multiplicity greater than one, so 1 ∈ σ(U(T * , 0)) also has multiplicity greater than one. Thus p(t) is a nonsimple periodic solution with the nonsimple period T * . And f / ∈ O(A, µ).

2) The periodic orbit p(t) is a constant a and T * > 0. The element 1 belongs to the spectrum σ(U(T m , 0)) of U(T m , 0). Thus, 1 also belongs to the spectrum σ(U(T * , 0)) of U(T * , 0). This implies that a is not hyperbolic. Thus, f / ∈ O h µ and f / ∈ O(A, µ).

3) The periodic orbit p(t) is a constant a and T * = 0. For any T 0 ∈ (0, 2A], we can find a sequence of positive integers N m such that N m T m converges to T 0 . Then, U m j (N m j T m j , 0) converges to U(T 0 , 0) in L(H s (S 1 ), H s (S 1 )). Thus, 1 belongs to the spectrum σ(U(T 0 , 0)) of U(T 0 , 0). Since, as explained in Section 2.2, U(T 0 , 0) = e LaT 0 and that L a is a sectorial operator, the inclusions (2.4) hold, with e replaced by a and with t replaced by any T 0 ∈ (0, 2A]. It follows that 0 belongs to the spectrum of L a , which means that a is not a simple equilibrium point and that f does not belong to the set O simp µ and thus does not belong to O(A, µ).

To prove the assertions (c) and (d), we argue as in the above cases 2) and 3). Proposition 4.1 is proved.

Before entering into the proof of the density of the set O(n, n), A ≤ n, we want to emphasize that the two main ingredients of this proof are the Sard-Smale theorem and the properties of the zero number. The properties of the zero number are recalled in the introduction (for more details, see [START_REF] Sturm | Sur une classe d'équations à différences partielles[END_REF][START_REF] Angenent | The zero set of a solution of a parabolic equation[END_REF][START_REF] Matano | Nonincrease of the lap-number of a solution for a one-dimensional semilinear parabolic equation[END_REF] for example). These properties are used here through Proposition 2.5 and the following primordial lemma. Lemma 4.2. Let p 0 (t) be a periodic solution of (1.1) of minimal period T 0 > 0. The map

(x, t) ∈ S 1 × [0, T 0 ) → (x, p 0 (x, t), ∂ x p 0 (x, t))
is one to one.

Proof. Assume that this map is not injective. Then there exist x 0 , t 0 ∈ [0, T 0 ) and

t 1 ∈ [0, T 0 ), t 0 = t 1 such that p 0 (x 0 , t 0 ) = p 0 (x 0 , t 1 ) , ∂ x p 0 (x 0 , t 0 ) = ∂ x p 0 (x 0 , t 1 ) . The function v(x, t) = p 0 (x, t + t 1 -t 0 ) -p 0 (x, t) is a solution of the equation v t (x, t) = v xx (x, t) + b(x, t)v(x, t) + d(x, t)v x (x, t) , where b(x, t) = 1 0 D u f (x, p 0 (t) + s(p 0 (t + t 1 -t 0 ) -p 0 (t)), ∂ x p 0 (t + t 1 -t 0 ))ds and d(x, t) = 1 0 D ux f (x, p 0 (t), ∂ x (p 0 (t) + s(p 0 (t + t 1 -t 0 ) -p 0 (t))
))ds. Moreover, the function v(x, t) satisfies v(x 0 , t 0 ) = 0 and ∂ x v(x 0 , t 0 ) = 0 and does not vanish everywhere since |t 1 -t 0 | < T 0 . Thus, the zero number z(v(t)) drops strictly at t = t 0 . Since v(t) is a periodic function of period T 0 , this leads to a contradiction with the fact that z(v(t + T 0 )) = z(v(t)). The lemma is proved.

To prove that O(n, n) is dense in G, we argue as follows. Let f 0 ∈ O h n . Due to Proposition 4.1, there exists a constant δ ∈ (0, 1) such that f 0 ∈ O h n+δ . Let δ ∈ (0, 1), ε > 0 and N 1 be as in Proposition 4.1 (a) and (c). And for A = n + 2, let r > 0, BE(f 0 , n + δ, r) and N 2 be as in Proposition 4.1 (d). We next choose a neighborhood

N 0 = N 1 ∩ N 2 of f 0 . Since O h
n+δ is open, we can also assume that N 0 ⊂ O h n+δ . Let η be a small positive constant such that η +∞ j=1 j -4 ≤ δ/2. We set

P(k) = O (3/2) k ε , n + δ -η k j=1 j -4 .
Obviously, one can choose ε as small as needed so that there exists k 0 ∈ N such that n ≤ (3/2) k 0 ε < n + 2. In Proposition 4.3 below, we show that for all k ∈ N, 0 < k ≤ k 0 , there exists an open neighbourhood

N k , N k ⊂ N k-1 , such that P(k) ∩ N k is dense in P(k -1) ∩ N k . Since P(0) = O(ε, n + δ), Property (c) of Proposition 4.1 implies that P(0) ∩ N 0 = O h n+δ ∩ N 0 = N 0 . These two properties show by recursion that P(k) ∩ N k is dense in N k for any k. Hence, O(n, n) ∩ N k 0 is dense in N k 0 . As f 0 ∈ O h
n is arbitrary and as O h n is dense in G, it follows that O(n, n) is dense in G. Proposition 4.3. For any k ∈ N, 0 < k ≤ k 0 , there exists a neighbourhood N k ⊂ N k-1 of f 0 such that the set P(k) ∩ N k is dense in P(k -1) ∩ N k .

Proof. We apply Theorem A.1 from the appendix with the following Banach spaces and functional Φ. Let 0 < δ * ≤ 1/4, we set:

U = (T, u 0 ) ∈ (ε, ((3/2) k + δ * )ε) × H s (S 1 ) | u 0 / ∈ BE(f 0 , n + δ, r),
and sup

t∈[0,((3/2) k +δ * )ε] S f 0 (t)u 0 C 1 (S 1 ) < n + δ -η k-1 j=1 j -4 - η 2 k -4 , Z =H s (S 1
).

We would like to choose P(k -1) ∩ N k-1 as set V . However, the space G is not even metrizable. To overcome this problem, one has to work with functions defined on compact sets. We notice that we can choose a neighbourhood

N k ⊂ N k-1 of f 0 such that, if sup t∈[0,((3/2) k +δ * )ε] S f 0 (t)u 0 C 1 (S 1 ) < n + δ -η k-1 j=1 j -4 - η 2 k -4 , then, for any g ∈ N k , sup t∈[0,((3/2) k +δ * )ε] S g (t)u 0 C 1 (S 1 ) < n + δ -η k-1 j=1 j -4 - η 4 k -4 . Let R : g ∈ G → Rg ∈ C 2 (S 1 × [-(n + 2), n + 2] × [-(n + 2), n + 2]
) be the restriction operator defined by

Rg = g |S 1 ×[-(n+2),n+2]×[-(n+2),n+2] .
We set V = R(P(k -1) ∩ N k ) endowed with the topology of

C 2 (S 1 × [-(n + 2), n + 2] × [-(n + 2), n + 2], R)
, which is a separable Banach space. The map R is a continuous, open and surjective map. Therefore the density of R(P(k) ∩ N k ) in V is equivalent to the density of P(k) ∩ N k in P(k -1) ∩ N k . We set z = 0 and we consider the functional Φ :

U × V → Z defined by Φ : (T, u 0 , f ) ∈ U × V → Φ(T, u 0 , f ) = S f (T )u 0 -u 0 .
As it will become clear below, Φ is a

C 2 -map from U × V into Z.
Let us make some remarks on the choice of this functional. First, for any (T, u 0 ) ∈ U, the trajectory S g (t)u 0 only depends on the value of Rg. The use of the restriction operator R does not affect any trajectory considered here.

Next, we remark that Φ -1 (0) = {(T, u 0 , f ) ∈ U × V | S f (t)u 0 is a periodic orbit of (1.1) of period T }. For any (T, p(0), f ) ∈ Φ -1 (0), either T is a simple period of the periodic orbit p(t) = S f (t)p(0), or T is not a simple period. Since f belongs to R(P(k -1) ∩ N k ), any periodic orbit p(t) of (1.1) with period T ∈ (0, (3/2) k-1 ε] and such that sup t p(t) C 1 (S 1 ) ≤ n + δη k-1 j=1 j -4 is hyperbolic. Therefore, as noticed in the remark following Proposition 2.5, if T is not a simple period of p(t), then T must belong to ((3/2) k-1 ε, ((3/2) k + δ * )ε] and must be the minimal period of p(t).

Working with sets involving a sequence of bounds of the type n + δη k-1 j=1 j -4 -η 2 k -4 looks complicated and technical. Actually, in the definition of sets as O h µ or O(A, µ), we need large inequalities (i.e. the symbols ≤), in order to obtain open sets, whereas the definition of the open set U requires strict inequalities (i. e. symbols <). Thus, working at the same time with large and strict inequalities, requires to introduce some intermediate bounds, which look complicated and artificial.

We now check that the hypotheses of Theorem A.1 are satisfied. Hypothesis i) of Theorem A.1 holds. Indeed, for any (T, p(0), f ) ∈ Φ -1 (0), we have

D t,u Φ(T, p(0), f )(τ, v) = p t (T )τ + (D u (S f (T )p(0)) -I)v ≡ p t (T )τ + (U f,p (T, 0) -I)v ,
where the linearized operator U f,p has been introduced in (2.1). Since U f,p : H s (S 1 ) → H s (S 1 ) is a compact operator, the operator U f,p (T, 0) -I is a Fredholm operator of index 0. We recall that dim (Ker (U f,p (T, 0) -I)) ≥ 1. Now two cases can occur. Either p t (T ) belongs to Im(U f,p (T, 0) -I) and thus dim (Ker D t,u Φ(T, p(0), f )) = dim (Ker (U f,p (T, 0) -I)) + 1 and codim (Im D t,u Φ(T, p(0), f )) = codim (Im(U f,p (T, 0) -I)).

Or p t (T ) does not belong to Im(U f,p (T, 0) -I) and thus dim (Ker D t,u Φ(T, p(0), f )) = dim (Ker (U f,p (T, 0) -I))

and codim (Im D t,u Φ(T, p(0), f )) = codim (Im(U f,p (T, 0) -I)) -1.

In both cases, we conclude that D t,u Φ(T, p(0), f ) is a Fredholm operator of index 1. We notice that, if D t,u Φ(T, p(0), f ) is a surjective map from R × H s (S 1 ) into itself, then the dimension of Ker D t,u Φ(T, p(0), f )) is equal to 1. We also remark that, if T is a simple period of p(t), then D t,u Φ(T, p(0), f ) is a surjective map. In particular, for any (T, p(0), f ) ∈ Φ -1 (0) such that the minimal period of S f (t)p(0) is less than (or equal to) (3/2) k-1 ε, we know that D t,u Φ(T, p(0), f ) is a surjective map, since f belongs to P(k -1).

We next show that Hypothesis ii) of Theorem A.1 is also satisfied. By the above considerations, we are reduced to proving that D t,u,f Φ(T, p(0), f ) is a surjective map, only in the case where T ∈ [(3/2) k-1 ε, ((3/2) k + δ * )ε] is the minimal period of p(t) = S f (t)p(0). An easy computation shows that

D t,u,f Φ(T, p(0), f )(τ, v, g) = p t (T )τ + (U f,p (T, 0) -I)v + Σ f,p (T )g ,
where Σ f,p (t)g = w(t) is the solution of the following affine equation

w t (x, t) = w xx (x, t) + D u f (x, p, p x )w + D ux f (x, p, p x )w x + g(x, p, p x ) , w(x, 0) = 0 . (4.6)
We remark that

w(t) = t 0 U f,p (t, s)g(•, p(s), p x (s))ds . (4.7)
The map D t,u,f Φ(T, p(0), f ) is surjective if and only if, for any h in H s (S 1 ), there exists (τ, v, g) ∈ R × H s (S 1 ) × RG, such that,

p t (T )τ + (U f,p (T, 0) -I)v + Σ f,p (T )g = h .
Due to the Fredholm alternative, h -Σ f,p (T )g belongs to the image of U f,p (T, 0) -I if and only if

S 1 (h -Σ f,p (T )g)ϕ * (x)dx = 0 , (4.8)
for any solution ϕ * of the adjoint equation

(U f,p (T, 0)) * ϕ * = ϕ * . (4.9)
Let ϕ * i , be a (at most two-dimensional) basis of Ker (U f,p (T, 0) -Id) * . We must find g such that S 1 (Σ f,p (T )g)ϕ * i (x)dx = S 1 h(x)ϕ * i (x)dx, for any i. The surjectivity of the map g → ( S 1 (Σ f,p (T )g)ϕ * i (x)dx) i is equivalent to the non-existence of (c i ) i such that i c i S 1 (Σ f,p (T )g)ϕ * i (x)dx = 0, for every g ∈ RG. Thus, we are reduced to proving that there is no solution ϕ * = 0 of the adjoint equation (U f,p (T, 0)) * ϕ * = ϕ * such that S 1 (Σ f,p (T )g)ϕ * (x)dx = 0, for every g ∈ RG. In other terms, we are reduced to prove that, for any solution ϕ * = 0 of the adjoint equation (U f,p (T, 0)) * ϕ * = ϕ * , there exists g ∈ RG such that

S 1 (Σ f,p (T )g)ϕ * (x)dx = 0 . (4.10)
Using the property (4.7), we see that the condition (4.10) is equivalent to the fact that, for any ϕ * , there exists g ∈ RG such that Since ϕ * = 0, there exist x 0 ∈ S 1 and t 0 ∈ [0, T ) such that [(U f,p (T, t 0 )) * ϕ * ](x 0 ) = 0. It is easy to construct a regular bump function g(x, u, u x ) which vanishes outside a small neighborhood of (x 0 , p(x 0 , t 0 ), p x (x 0 , t 0 )) and is positive in this neighborhood. Due to the injectivity property of Lemma 4.2, for x 0 fixed, there exists no other time t 1 ∈ [0, T ) such that p(x 0 , t 1 ) = p(x 0 , t 0 ) and p x (x 0 , t 1 ) = p x (x 0 , t 0 ). Therefore, the function (x, s) -→ g(x, p(x, s), p x (x, s)) is a regular bump function concentrated around (x 0 , t 0 ). For such a choice of g, the condition (4.11) is thus satisfied.

Since all the hypotheses of Theorem A.1 hold, there exists a generic subset V 1 of V such that, for any f ∈ V 1 , the map D t,u Φ(T, p(0), f ) is a surjective map. If p t (T ) belongs to Im(U f,p (T, 0) -I), then U f,p (T, 0) -I is surjective, which is not possible since it is a Fredholm operator of index 0 and that its kernel contains p t (0). Thus, p t (T ) does not belong to Im(U f,p (T, 0) -I) and 1 is an eigenvalue of algebraic multiplicity 1. Then, dim (Ker (U f,p (T, 0) -I)) = codim (Im (U f,p (T, 0) -I)) = 1 and thus 1 is an eigenvalue of geometric multiplicity 1. The proposition is then proved.

Generic hyperbolicity for nonlinearities independent of x

The purpose of this section is the proof of Theorem 1.4. We denote by G i the subspace of G consisting of functions independent of x. We use the terminology of Proposition 1.1.

Notice that if u is a frozen wave, then every spatial translation u(•x 0 ) of u is also a frozen wave. This means that a frozen wave always belongs to a circle of equilibria and is never a hyperbolic equilibrium of (1.2). However, it is more natural to consider the frozen waves as particular cases of rotating waves with speed c = 0. For the remaining part of this section, we group the waves with speed c ∈ R into a single category and simply call them "waves" if there is no need to distinguish between rotating and frozen waves. To simplify the notations, we say that a frozen wave u is hyperbolic if the corresponding circle of equilibria is normally hyperbolic, that is, if 0 is a simple eigenvalue of the linearized operator with the eigenfunction u x and is the only eigenvalue with real part equal to 0.

If u(x, t) = v(xct) is a wave solution of (1.2) of speed c ∈ R, then v is an equilibrium of the equation w t = w xx + f (w, w x ) + cw x .

(5.1)

For this reason, the first step of the proof of Theorem 1.4 consists in eliminating the time dependence in the problem. Let L : H 2 (S 1 ) -→ L 2 (S 1 ) to be the linearized operator defined by Lϕ = ϕ xx + f ′ u (v, v x )ϕ + f ′ ux (v, v x )ϕ x + cϕ x .

Lemma 5.1. A wave u(x, t) = v(xct) of (1.2) is hyperbolic if and only if 0 is a simple eigenvalue of L. Moreover, if v is spatially 1 n -periodic, i.e. t → u(t) is 1 nc periodic, then any solution ψ of Lψ = 0 or of L * ψ = 0 is also spatially periodic of period 1 n . Proof. If u is a frozen wave, then the first assertion of Lemma 5.1 is a direct consequence of Proposition 2.3. Let u(x, t) = v(xct) be a rotating wave of period T = 1/c. We consider the operator U(T, 0) : H s (S 1 ) -→ H s (S 1 ) defined by U(T, 0)ϕ 0 = ϕ(T ) where ϕ(t) is the solution of

ϕ t = ϕ xx + f ′ u (u, u x )ϕ + f ′ ux (u, u x )ϕ x , ϕ(x, 0) = ϕ 0 (x) .
(5.2)

We set ϕ(x, t) = ψ(xct, t), so that ψ satisfies ψ t = Lψ. Let V (T, 0) = e T L . Since cT = 1, there is a perfect correspondence between the spectrum of U(T, 0) and the spectrum of V (T, 0). In particular, Proposition 2.5 shows that the rotating wave u is hyperbolic if and only if 1 is a simple eigenvalue of V (T, 0). Notice that v x = 0 belongs to Ker L. Thus, by Proposition 2.3, zero is the only eigenvalue of zero real part for L. The spectral theorem recalled in (2.4) implies that u is hyperbolic if and only if 0 is a simple eigenvalue of L.

hyperbolic waves. Indeed, by arguments similar to the ones used in the proof of Property (d) of Proposition 4.1, one can show that there is a finite number of periodic orbits p of period less that n and satisfying sup t p(t) C 1 ≤ n. Thus, we can choose ε > 0 as small as wanted to unfreeze the frozen waves without freezing any rotating wave. We emphasize that, for a general system, without the constraint on the period, the number of hyperbolic periodic orbits could be infinite, even in bounded sets, since hyperbolic periodic orbits might pile up on a homoclinic orbit of a hyperbolic equilibrium point. In the case of Equation (1.2), one should be able to remove the constraint on the period, since there do not exist homoclinic orbits (see [START_REF] Fiedler | Heteroclinic orbits between rotating waves of semilinear parabolic equations on the circle[END_REF]).

A Appendix : Sard-Smale theorem

Let M and M ′ be two differentiable Banach manifolds and let f : M -→ M ′ be a differentiable map. We say that y ∈ M ′ is a regular value of f if, for any x ∈ M such that f (x) = y, the differential Df (x) : T x M -→ T y M ′ is surjective. The points of M ′ which are not regular are said to be critical. The classical theorem of Sard says that, if U is an open set of R p and if f : U -→ R q is of class C s with s > max(pq, 0), then, the set of critical values of f in R q is of Lebesgue measure zero. Using Fredholm operators and a Lyapunov-Schmidt method, Smale has generalized the Sard Theorem to infinite-dimensional spaces (for Fredholm operators, we refer to [START_REF] Bonic | Linear functional analysis[END_REF] for example). The Sard-Smale Theorem stated below is an application of the Smale Theorem.

Theorem A.1. Let X, Y, Z be three smooth Banach manifolds. Let U X, V ⊂ Y be two open sets, Φ : U × V -→ Z be a map of class C k (k ≥ 1) and z be a point of Z.

We assume that: i) ∀(x, y) ∈ Φ -1 (z), D x Φ(x, y) is a Fredholm operator of index strictly less than k, ii) ∀(x, y) ∈ Φ -1 (z), DΦ(x, y) is surjective, iii) X and Y are separable.

Then Θ = {y ∈ V | z is a regular value of Φ(., y)} is a generic subset of V .

The proof of Theorem A.1 can be found in [START_REF] Saut | Generic properties of nonlinear boundary value problems[END_REF] or [START_REF] Quinn | Transversal approximation on Banach manifolds[END_REF] (for stronger versions, see also [START_REF] Henry | Perturbation of the Boundary for Boundary Value Problems of Partial Differential Operators, with editorial assistance from Jack Hale and Antonio Luiz Pereira[END_REF]). We also refer to [START_REF] Joly | Adaptation of the generic PDE's results to the notion of prevalence[END_REF] where one can find a short review on PDE generic results, as well as adaptations of the transversality theorems to the notion of prevalence, which is a notion of "almost always" different from the genericity.

Proposition 3 . 1 .

 31 For any n ≥ 1, the set O simp n = {f ∈ G | any equilibrium point e of (1.1) with e C 1 (S 1 ) ≤ n is simple} is a dense open subset of G. As a consequence, the set O simp = {f ∈ G | any equilibrium point e of (1.1) is simple} is a generic subset of G. Proof. If O simp n is a dense open set, then, since any equilibrium belongs to C 1 (S 1 ), O simp = ∩ n O simp n and thus O simp is a generic subset of G. Let n be any positive integer. O simp n is open: We denote by R : g ∈ G → Rg ∈ C 2 (S 1 ×[-(n+2), n+2]×[-(n+2), n+2], R) the restriction operator defined by

  the Whitney topology and the classical C 2 -topology coincide. Since O simp n only depends on the values of f in S 1 × [-n, n] × [-n, n], it suffices to show that RO simp n is open in RG for the classical C 2 -topology. It thus suffices to prove, that if

Proposition 3 . 2 .

 32 For any n ≥ 1, the set O h n = {f ∈ G | any equilibrium point e of (1.1) with e C 1 (S 1 ) ≤ n is hyperbolic} is a dense open subset of G. As a consequence, the set O h = {f ∈ G | any equilibrium point e of (1.1) is hyperbolic} is a generic subset of G. Proof. As in the proof of Proposition 3.1, it is sufficient to show that O h n is a dense open set.

Proposition 4 . 1 .

 41 The following properties hold.(a) Let f ∈ O simp n (resp. f ∈ O h n ). There exists δ > 0 such that f ∈ O simp n+δ (resp. f ∈ O h n+δ ). (b) For any µ > 0, the set O(A, µ) is open. (c) Let f ∈ O simpn and let δ be as in (a). There exist ε > 0 and a neighborhood N 1 ⊂ O simp n+δ of f such that, for any g ∈ N 1 , any nonconstant periodic solution p(t) of S g (t) with sup t∈R p(t) C 1 (S 1 ) ≤ n + δ has a smallest period strictly larger than ε. (d) Let f ∈ O h

S 1 T 0 U 1 T 0 g

 1010 f,p (T, s)(g(x,p(x, s), p x (x, s)))ϕ * (x)dsdx = S (x, p(x, s), p x (x, s))[(U f,p (T, s)) * ϕ * ](x)dsdx = 0 .(4.11)

Assume now that v is 1 n -periodic. Let L be the restriction of L to H s 1/n-per (S 1 ) = H s (R/(1/n)Z) and let ṽx the restriction of v x to R/(1/n)Z. We have Lṽ x = 0, which implies that 0 is also an eigenvalue of L * . By Proposition 2.3, the only eigenvalue of L or L * with zero real part is zero. Using the remark following Proposition 2.5, we prove that every solution of Lψ = 0 (resp. L * ψ = 0) is necessarily 1 n -periodic and solution of L ψ = 0 (resp. L * ψ = 0).

We have to consider the case of homogeneous equilibria separately. Lemma 5.2. There exists a generic dense subset O hom of G i such that every homogeneous equilibrium point of (1.2) is hyperbolic.

Proof. The lemma is a direct consequence of the following computation. If u ∈ R is a homogeneous equilibrium, then there exist a function ϕ ∈ H 2 (S 1 ) and µ ∈ R such that

The main step of the proof of Theorem 1.4 consists in applying Sard-Smale Theorem to deal with the waves. Lemma 5.3. There exists a generic subset O wav of G i such that every wave of (1.2) is hyperbolic.

Proof. The proof is very similar to the one of Proposition 4.3. The main tool is Theorem A.1 of the appendix. We recall that G i is not a metrizable space. To overcome this difficulty, we write

do not matter for the genericity of the set O wav n . We apply Theorem A.1 of the appendix with the following spaces and functional. We

). We set z = 0 and

First notice that Hypothesis iii) of Theorem A.1 is satisfied and that a point (v, c, f ) belongs to Φ -1 (0) if and only if u(x, t) = v(xct) is a wave of speed c for (1.2). We set

We recall that, as proved in Lemma 2. Hypothesis ii) of Theorem A.1 is also satisfied. Indeed, let h ∈ L 2 (S 1 ). We have to find v and g such that DΦ(v, c, f ).(ϕ, 0, g) = Lϕ + g(v, v x ) = h. Due to the Fredholm alternative, hg(v, v x ) belongs to Im(L) if and only if S 1 (hg(v, v x ))ψ = 0 for all ψ solution of L * ψ = 0. Let (ψ i ) be a (at most two-dimensional) basis of Ker(L * ), we must find g such that g(v, v x )ψ i = hψ i for all i. The surjectivity of the map g → g(v, v x )ψ i i is equivalent to the non-existence of (c i ) = 0 such that c i g(v, v x )ψ i = 0 for all g. Thus, setting ψ = c i ψ i , we are reduced to prove that there is no ψ = 0 such that L * ψ = 0 and S 1 g(v, v x )ψ = 0 for all g ∈ RG i . Let ψ satisfying L * ψ = 0 and S 1 g(v, v x )ψ = 0 for all g ∈ RG i . Let m = 0 be the integer such that 1/m is the minimal period of the function v. By Lemma 5.1, ψ is also 1/m-periodic and S 1 g(v, v x )ψ = 0 is equivalent to 1/m 0 g(v, v x )ψ = 0. Since v is a periodic solution of minimal period 1/m of a second order ordinary differential equation, the map x ∈ [0, 1/m) → (v(x), v x (x)) ∈ R 2 is injective and, hence 1/m 0 g(v, v x )ψ = 0 for all g implies that ψ ≡ 0. This shows the surjectivity of DΦ(v, c, f ). All the assumptions of Theorem A.1 being satisfied, there exists a generic subset RO wav n of RG i such that for any f ∈ RO wav n and for any wave u(x, t) = v(xct) of (1.2) in U, the map D v,c Φ : (ϕ, d) → Lϕ + dv x is surjective. If v x belongs to Im(L), this surjectivity implies that L is surjective, which is not possible since L is a Fredholm operator of index 0 and since Ker(L) is not {0} because it contains v x = 0. Thus, v x does not belongs to Im(L), which means that 0 is an algebraically simple eigenvalue for L. Moreover, dim(KerL)=codim(Im(L))=1 which means that 0 is a geometrically simple eigenvalue of L. The conclusion is then given by Lemma 5.1.

Proof of Theorem 1.4: Applying Lemmas 5.2 and 5.3, we obtain a generic subset of G i such that all homogeneous equilibria and all waves of (1.2) are hyperbolic. To obtain Theorem 1.4, it only remains to remove the frozen waves. Indeed, we recall that a frozen wave is never hyperbolic as a non-homogeneous equilibrium point of (1.2) (and not as a wave as it was considered in the above lemmas). As already noticed in [START_REF] Fiedler | Heteroclinic orbits between rotating waves of semilinear parabolic equations on the circle[END_REF], if we replace f (u, u x ) by f (u, u x ) + εu x , we can "unfreeze" every frozen wave. To be sure that we are not "freezing" some rotating wave, we remark that there is at most a countable number of


Modal Logics with Counting

Carlos Areces, Guillaume Hoffmann, and Alexandre Denis INRIA Nancy Grand Est, France {firstname.lastname}@loria.fr Abstract. We present a modal language that includes explicit operators to count the number of elements that a model might include in the extension of a formula, and we discuss how this logic has been previously investigated under different guises. We show that the language is related to graded modalities and to hybrid logics. We illustrate a possible application of the language to the treatment of plural objects and queries in natural language. We investigate the expressive power of this logic via bisimulations, discuss the complexity of its satisfiability problem, define a new reasoning task that retrieves the cardinality bound of the extension of a given input formula, and provide an algorithm to solve it.

Counting, Modally

Suppose there are at least two apples (say, on the table, but we don't care at the moment where the apples are). First-order logic (FOL) with equality has no problem expressing this fact1 : ∃x.∃y.(x = y ∧ Apple(x) ∧ Apple(y)).

We can actually dispense with equality, if we introduce counting quantifiers [START_REF] Mostowski | On a generalization of quantifiers[END_REF] ∃ ≥2 x.Apple(x).

But suppose that we want to dispense with quantifiers instead, and count in terms of a propositional (or a modal) language. The following representation seems quite natural (arguably, even more natural than the first-order counterparts with or without counting quantifiers)

Apple ≥ 2.
In this paper we will investigate propositional and modal languages extended with such counting operators. Let us be bold and introduce, already, the formal syntax and semantics of the basic modal logic with counting MLC, the main language we want to explore: Definition 1 (Syntax). Let Prop = {p 1 , p 2 , . . . } (the propositional symbols) and Rel = {r 1 , r 2 , . . . } (the relational symbols) be disjoint, countable infinite sets. The set Forms of formulas of MLC over signature Prop, Rel is defined as:

Forms ::= ⊥ | p | ¬ϕ | (ϕ 1 ∧ ϕ 2 ) | r ϕ | (ϕ ≥ n) | (ϕ ≤ n),
for p ∈ Prop, r ∈ Rel, ϕ, ϕ 1 , ϕ 2 ∈ Forms and n a natural number. Other Boolean and modal operators are defined as usual, and we define (ϕ = n) as

(ϕ ≥ n)∧(ϕ ≤ n), (ϕ > n) as (ϕ ≥ (n+1)) and (ϕ < n) as (ϕ ≤ (n-1)) if n > 0 or ⊥ otherwise.
We will call PLC the "propositional fragment," i.e., the fragment obtained by dropping r ϕ. Let us now introduce the semantics.

Definition 2 (Semantics). Given a signature S = Prop, Rel , a model for S is a tuple W, (R r ) r∈Rel , V , satisfying the following conditions: (i) W = ∅ (elements in W are called states); (ii) each R r is a binary relation on W (usually called accessibility relations); (iii) V : Prop → 2 W is a labeling function.

Given the model M = W, (R r ) r∈Rel , V and w ∈ W , the semantics for the different operators is defined as follows:

M, w |= p ⇐⇒ w ∈ V (p), p ∈ Prop M, w |= ¬ϕ ⇐⇒ M, w |= ϕ M, w |= ϕ ∧ ψ ⇐⇒ M, w |= ϕ and M, w |= ψ M, w |= r ϕ ⇐⇒ there is w ′ such that R r (w, w ′ ) and M, w ′ |= ϕ M, w |= (ϕ ≥ n) ⇐⇒ |{w | M, w |= ϕ}| ≥ n M, w |= (ϕ ≤ n) ⇐⇒ |{w | M, w |= ϕ}| ≤ n.
We will say that a formula ϕ is satisfiable, if there is a model M and a state w in its domain such that M, w |= ϕ. For a set of formulas Γ ∪ {ϕ} we say that Γ |= ϕ if and only if for any model M and any w in its domain M, w |= Γ implies M, w |= ϕ (this relation is sometimes called local entailment). The extension ||ϕ|| M of a formula ϕ in a model M is the set {w | M, w |= ϕ}, and the theory of w in M, notation Th M (w), is the set {ϕ | M, w |= ϕ}. When the model M is clear from context we will drop the super-indexes. We will write

M, w ≡ MLC M ′ , w ′ if Th M (w) = Th M ′ (w ′ ).
It should be clear from Definitions 1 and 2 that MLC is indeed the basic modal logic ML [START_REF] Blackburn | Modal Logic[END_REF] extended with the counting operators. We will be mainly discussing extensions of ML for simplicity. We could have naturally added the counting operators to any modal logic, e.g., temporal logic with counting.

The MLC language and, in particular, its sublanguage PLC have been investigated under different guises. PLC is introduced as the logic S5 n by Fine in [START_REF] Fine | In so many possible worlds[END_REF] where the, by now well studied, notion of graded modalities was introduced. The semantic definition of the graded modality r n ϕ is given by the condition

M, w |= r n ϕ ⇐⇒ |{w ′ | R r (w, w ′ ) and M, w ′ |= ϕ}| ≥ n.
S5 n is the logic obtained when the r n operator is restricted to models where R r is interpreted as an equivalence relation. Now, if R r is the universal relation, then r n ϕ is trivially equivalent to (ϕ ≥ n). But a well known result (see, e.g. [START_REF] Blackburn | Modal Logic[END_REF]) establishes that the modal logic of the universal relation coincides with the modal logic obtained when we only require the accessibility relation to be an equivalence relation. The main contribution of [START_REF] Fine | In so many possible worlds[END_REF] is to provide sound and complete axiomatizations for these languages. The original results of Fine were extended by van der Hoek and de Rijke in [START_REF] Van Der Hoek | Generalized quantifiers and modal logic[END_REF][START_REF] Van Der Hoek | Counting objects[END_REF]. In addition to providing further axiomatizations, investigating normal forms, and establishing the complexity of the satisfiability problem for different logics with graded modalities, the authors propose these languages as a modal framework where some ideas from the Theory of Generalized Quantifiers [START_REF] Westerståhl | Quantifiers in formal and natural languages[END_REF] could be investigated by means of modal tools.

The relation between MLC and graded modalities was also discovered in the field of description logics. In this area, graded modalities are called cardinality restrictions and Baader et al. investigate in [START_REF] Baader | Cardinality restrictions on concepts[END_REF] concept cardinality restrictions which coincide exactly with the counting operators we defined. Interestingly, they decide to add concept cardinality restrictions not as operators of the concept language, but as a more expressive kind of terminological axioms, and they remark that they can express classical terminological axioms of the form ϕ ⊑ ψ. ϕ ⊑ ψ is satisfied in the model if the interpretation of ϕ is a subset of the interpretation of ψ, and indeed this is the case exactly when ((ϕ ∧ ¬ψ) ≤ 0). The main contribution of [START_REF] Baader | Cardinality restrictions on concepts[END_REF] is the definition of sound, complete and terminating tableaux calculus for these languages. A detailed complexity analysis of their satisfiability problem and optimal tableau calculi are given in [START_REF] Tobies | Complexity results and practical algorithms for logics in Knowledge Representation[END_REF].

Another way of explaining why counting operators can express terminological axioms is realizing that they can express the universal modality Aϕ [START_REF] Goranko | Using the universal modality: Gains and questions[END_REF]:

M, w |= Aϕ ⇐⇒ for all w ′ , M, w ′ |= ϕ.
Aϕ is equivalent to ((¬ϕ) ≤ 0), and ϕ ⊑ ψ is equivalent to A(ϕ → ψ). Actually, counting modalities can also express nominals (i.e., special propositional symbol whose interpretations are restricted to singleton subsets of the domain) by just stating (p = 1) for p a propositional symbol, and hence they can be considered also as hybrid logics [START_REF] Areces | Hybrid logics[END_REF].

In this article, we provide new results about the MLC language. Our first contribution is conceptual, rather than technical, and it can be simple put as follows. The counting operators (ϕ ≥ n) and (ϕ ≤ n) are interesting on their own, independently of their relation with graded modalities. They are global operators (with a behavior similar to the universal modality or satisfiability operators), and they can be naturally combined with local operators (as is commonly done in hybrid languages). They are also modular, and they can naturally be added to any modal language. In a slogan: counting operators are the modal counterpart of first-order counting quantifiers.

In Section 2 we show how MLC can be used as representation language in a natural language application modeling queries including plurals. In Section 3 we will investigate the expressive power of MLC using a suitable notion of bisimulation. In Section 4 we first discuss the complexity of the satisfiability problem, drawing from previously known results, we then introduce a new reasoning task and devise an algorithm to solve it.

We discuss here a possible representation of plurals and references in MLC, intended to be used in natural language processing tasks such as reference resolution or generation as is done in, e.g., [START_REF] Varges | Generating referring expressions containing quantifiers[END_REF]. The idea is to represent the information introduced in a discourse as a set of MLC formulas Γ , and to be able to express and answer queries of the form "how many of a certain kind of objects are there?" in this context. This representation does not aim to solve all the issues concerning the use of plurals in natural language (e.g., the distributive versus collective readings of certain adjectives when applied to sets of objects), which are known to be difficult to model [START_REF] Asher | Ambiguity and anaphora with plurals in discourse[END_REF]. For further details see, for example, [START_REF] Franconi | A treatment of plurals and plural quantifications based on a theory of collections[END_REF].

As we saw in the previous section, MLC enables us to assert the cardinality of a proposition in the model. For example, Γ = {(Apple∧Red) = 2} represents the sentence "there are two red apples", and the query "how many (Apple ∧ Red)?" should return "2". But suppose that we want to refer to "two red apples" (i.e., we don't know how many red apples are there in total, but we want to refer to two of them). For the representation of this kind of reference we need to be able to name the referred group of object by, for example, introducing a new propositional symbol a 1 and adding to Γ the formula2 : "two red apples":

(a 1 = 2) ∧ (a 1 ⊑ (Apple ∧ Red))
In this case, a query "how many (Apple ∧ Red)?" cannot be answered (i.e., is undefined) since the total number of apples in the model is not known. But the query "how many a 1 ?" should return "2."

If now we add that there are also two green apples and want to refer to that group, we need to introduce another propositional symbol a 2 and add to Γ : "two green apples": (a 2 = 2) ∧ (a 2 ⊑ (Apple ∧ Green))

Now, the number of apples that are in the group formed by a 1 and a 2 (i.e., a 1 ∨ a 2 ) is also undefined because nothing prevents those two sets from overlapping. If we explicitly say that the group are disjoint (a 1 ⊑ ¬a 2 ) or that the colors are mutually exclusive (Green ⊑ ¬Red) for that we should be able to answer "4".

Suppose that now we learn that "three of the apples are rotten." This reference creates a new group containing all the apples mentioned up to now:

(a 3 ⊑ (a 1 ∨ a 2 )) ∧ ((a 1 ∨ a 2 ) ⊑ a 3 )
And then assert that three of them are rotten by adding to Γ (a 3 ∧Rotten) = 3). If we further discover that all the red apples are rotten (a 1 ⊑ Rotten), querying for "how many green apples are rotten," i.e., "how many (a 2 ∧Rotten)" will returns "1".

In Section 4 we introduce the inference task of counting that corresponds to the finite cardinality queries we just discussed. But first, in the next section, we investigate in detail the expressive power of MLC.

To get more familiar with the language, let us start with some examples of what can be expressed in MLC. We can, for example, fix the size of the model to any finite cardinality by setting (⊤ = n)

for n a natural number. The formula also shows that, if numbers are coded in binary, then neither MLC nor PLC has the polysize model property.

Proposition 1. If numbers are coded in binary, then there are formulas in PLC (and hence also in MLC) whose only models are exponentially larger.

Notice that counting operators can be nested. For example ((p ≥ 1) ≥ 1) is a well formed formula, which it is actually equivalent to (p ≥ 1). But, as it is discussed in [START_REF] Van Der Hoek | Generalized quantifiers and modal logic[END_REF], every formula in MLC is equivalent to a formula where each counting operator appears under the scope of neither modal nor counting operators. The proof uses the fact that for any counting subformula σ appearing in a formula ϕ we have that the following is valid

ϕ[σ] ↔ (σ → ϕ[σ/⊤]) ∧ (¬σ → ϕ[σ/⊥])
Other operators with a global semantics, like the universal modality A or satisfiability operators i:, have the same property. Notice though, that the formula we obtain after extracting all counting operators can be exponentially larger. If we only require equi-satisfiability (and not equivalence), we can use the method of [START_REF] Areces | Coinductive models and normal forms for modal logics[END_REF] to obtain a formula which is only polynomially larger. We will return to this issue in Section 4.

As we mentioned in the introduction, the hybrid logic H(A) (the basic modal logic extended with nominals and the universal modality [START_REF] Areces | Hybrid logics[END_REF]) is a sublogic of MLC, as the language can express nominals and the universal modality. It can even express the difference modality Dϕ [START_REF] De Rijke | The modal logic of inequality[END_REF] with semantics M, w |= Dϕ ⇐⇒ there is w ′ = w and M, w ′ |= ϕ as Dϕ is equivalent to (ϕ → (ϕ ≥ 2)) ∧ (¬ϕ → (ϕ ≥ 1)). On the other hand, the expressive power of counting and graded modalities is incomparable. We will establish this in Theorem 3 using a suitable notion of bisimulation for MLC that we now introduce Definition 3 (Bisimulation). A bisimulation between two models M = W, (R r ) r∈Rel , V and M ′ = W ′ , (R ′ r ) r∈Rel , V ′ is a non-empty binary relation E between their domains (that is, E ⊆ W ×W ′ ) such that whenever wEw ′ we have:

Atomic harmony: w and w ′ satisfy the same propositional symbols. Zig: if R r wv then there exists a point v ′ ∈ W ′ such that vEv ′ and R ′ r w ′ v ′ . Zag: if R ′ r w ′ v ′ then there exists a point v ∈ W such that vEv ′ and R r wv. Bijectivity: E contains a bijection between W and W ′ .

For two models M and M ′ and two elements w and w ′ in their respective domains, we write M, w M ′ , w ′ if there exists a bisimulation between M, w and M ′ , w ′ linking w and w ′ . Theorem 1. If M, w M ′ , w ′ then M, w and M ′ , w ′ satisfy the same formulas of MLC.

Proof. Assume there is a bisimulation E between M and M ′ . Because of Atomic harmony, Zig and Zag, we know that E preserves all formulas of the basic modal language [START_REF] Blackburn | Modal Logic[END_REF]. We only need to consider the counting operators.

Suppose then that ϕ = (ψ ≥ n) and let f be one bijection that by definition is contained in the bisimulation linking M and M ′ . Assume that M, w |=

(ψ ≥ n). By inductive hypothesis f (||ψ|| M ) ⊆ ||ψ M ′ || and because f is a injec- tive |f (||ψ|| M )| ≥ n, hence M ′ , w ′ |= (ψ ≥ n). For the other direction, assume M ′ , w ′ |= (ψ ≥ n).
Because f is a bijection we can consider f -1 (||ψ|| M ′ ) which has size greater than n , and by inductive hypothesis we know that it is a subset of ||ψ|| M . Hence M, w |= (ψ ≥ n). The case for ϕ = (ψ ≤ n) is similar.

As usual, the converse is not necessarily true but it holds on finite models.

Theorem 2. Let M = W, R, V and M ′ = W ′ , R ′ , V ′ be two finite models and (w, w ′ ) ∈ W × W ′ , M, w M ′ , w ′ if and only if M, w ≡ MLC M ′ , w ′ .
Proof. The implication from left to right is given by Theorem 1. For the other implication, we have to prove that ≡ MLC is a bisimulation between M and M ′ that links w and w ′ . Atomic harmony, Zig and Zag are proved in the standard way (see [START_REF] Blackburn | Modal Logic[END_REF]). To prove that ≡ MLC contains a bijection reason as follows.

Consider every pair of subsets (C,

C ′ ), C ⊆ W , C ′ ⊆ W ′ such that for all (a, b) ∈ C × C ′ , M, a ≡ MLC M ′ , b.
There is at least one such pair by hypothesis. Enumerate these pairs as (C 1 , C ′ 1 ), . . . , (C n , C ′ n ) (as the model is finite there is only a finite number of them), and let Σ 1 , . . . , Σ n be such that Σ i = Th(a) for some a ∈ C i ∪C ′ i (by construction all elements in C i ∪C ′ i satisfy the same formulas of MLC). Now choose for each i, ϕ i ∈ Σ i such that for all j = i, ϕ i ∈ Σ j . Notice that

|C i | = |||ϕ i || M | and that |C ′ i | = |||ϕ i || M ′ |, we want to prove that |C i | = |C ′ i |. But by hypothesis M, w ≡ MLC M ′ , w ′ , and then M, w |= ϕ i = n if and only if M ′ , w ′ |= ϕ i = n.
As C i and C ′ i have the same cardinality we can define an injective function f :

C i → C ′ i , such that for a ∈ C i , f (a) ∈ C ′ i .
It only rests to prove that f is total and surjective.

Suppose there is a ∈ W such that a ∈ C i , then there is no element a ′ in W ′ such that M, a ≡ MLC M ′ , a ′ . For each a ′ i ∈ W ′ , let ϕ i be a formula such that ϕ i ∈ Th(a) but ϕ i ∈ Th(a ′ ). But then M, w |= ( ϕ i ≥ 1) while M, w ′ |= ( ϕ i ≥ 1) contradicting hypothesis. In a similar way we can prove that f is surjective.

Notice that MLC-bisimulations are not isomorphisms. The following two models, for example, are MLC-bisimilar but not isomorphic.

M M ′

M and M ′ can be differentiated by the first order sentences ∃x.∀y.(¬R(x, y)∧ ¬R(y, x)). But there is no MLC formula which is globally true in one model but false in the other. On the other hand, [START_REF] Westerståhl | Quantifiers in formal and natural languages[END_REF] proves that every sentence of first-order logic with equality and only monadic propositional symbols is equivalent to the translation of a formula in PLC.

We now return to the comparison of MLC and graded modalities.

Theorem 3. The expressive power of counting modalities and graded modalities is incomparable (when interpreted on the set of all possible models).

Proof. Consider the following two models M and M ′ . It is not difficult to verify that the dotted arrows defines a MLC-bisimulation.

w M w ′ M ′ M, w |= r 2 ⊤ while M ′ , w ′ |= r 2 ⊤
while no formula of MLC can differentiate w and w ′3 . For the other direction, just consider a model with one state and another model with two states. Clearly, the models cannot be distinguished using graded modalities (as they can only count the number of successors) but the counting forma formula (⊤ ≤ 1) differentiates them.

Inference in MLC

The complexity of the satisfiability problem for MLC and PLC have been studied in the literature. As we mention in Section 3, when dealing with complexity we should take care of whether numbers are coded in unary or binary. Let us call L u and L b the unary and binary coding, respectively, for either MLC or PLC. Then, the previously established results are as follows.

Theorem 4. 1. PLC u -SAT is NP-complete [START_REF] Van Der Hoek | Counting objects[END_REF]. 2. MLC u -SAT is ExpTime-complete [START_REF] Areces | The computational complexity of hybrid temporal logics[END_REF][START_REF] Tobies | Complexity results and practical algorithms for logics in Knowledge Representation[END_REF]. 3. PLC b -SAT is NP-hard and in PSpace [START_REF] Van Der Hoek | Generalized quantifiers and modal logic[END_REF]. 4. MLC b -SAT is ExpTime-hard and in 2-NExpTime [START_REF] Tobies | Complexity results and practical algorithms for logics in Knowledge Representation[END_REF].

Proof. Hardness in all cases is clear, we only comment on the upper bounds. The proof of 1) is via the polysize model property. The proof of 2) is by a linear satisfiability preserving translation into H(A) as we will show below. The proof of 3) is by a direct algorithm that solves satisfiability. The proof of 4) is by a linear satisfiability preserving translation into C 2 , first order logic with only two variables and counting quantifiers.

The satisfiability problem is not our main focus here, although it is going to be an essential part of the following inference task "exactly how many ϕ states are implied by the theory Γ ?" Formally Definition 4. Let Γ ∪ {ϕ} be a finite set of formulas in MLC, we define the function |ϕ| in Γ as follows 4|ϕ| in

Γ = n if Γ |= (ϕ = n) and Γ consistent undefined otherwise
For instance, given Γ = {(p = 2), (q = 3), (¬(p ↔ ¬q) ≤ 0)}, we have that |p ∨ q| in Γ will be defined as 5.

We will show an algorithm that solves this task using any model building procedure. In particular we will show how model building algorithms for H(A) like those proposed in [START_REF] Bolander | Termination for hybrid tableaus[END_REF][START_REF] Kaminski | Terminating tableaux for graded hybrid logic with global modalities and role hierarchies[END_REF] can be used. We introduce first the notion of negation normal form for MLC. Definition 5. Given ϕ ∈ Forms the negation normal form of ϕ is obtained applying the following rules

¬¬ϕ ❀ ϕ ¬(ϕ 1 ∧ ϕ 2 ) ❀ (¬ϕ 1 ) ∨ (¬ϕ 2 ) ¬(ϕ 1 ∨ ϕ 2 ) ❀ (¬ϕ 1 ) ∧ (¬ϕ 2 ) ¬ r ϕ ❀ [r]¬ϕ ¬[r]ϕ ❀ r ¬ϕ ¬(ϕ ≥ 0) ❀ ⊥ ¬(ϕ ≥ n) ❀ ϕ ≤ (n -1) for n > 0 ¬(ϕ ≤ n) ❀ ϕ ≥ (n + 1)
As we mentioned in Section 3, every formula in MLC is equivalent to a formula where each counting operators has been extracted and it appears under the scope of neither modal nor counting operators. Each MLC formula is equivalent to its extracted, negation normal form. Let MLC en be set of extracted formulas of MLC in negation normal form. We now present a translation from MLC en to H(A) formulas, which follows a very similar procedure to the one presented by Tobies for Description Logics in [START_REF] Tobies | Complexity results and practical algorithms for logics in Knowledge Representation[END_REF]. Tr π works by traversing formulas and adding new nominals so that counting claims are preserved (π is used to ensure that we always introduce new nominals, initially π is set to the empty string; i:ϕ is a satisfiability statement defined in H(A) as A(¬i ∨ ϕ)).

Tr π (p) = p Tr π (¬ϕ) = ¬Tr π (ϕ) Tr π (ϕ ∧ ψ) = Tr π0 (ϕ) ∧ Tr π1 (ψ) Tr π (ϕ ∨ ψ) = Tr π0 (ϕ) ∨ Tr π1 (ψ) Tr π ( r ϕ) = r Tr π (ϕ) Tr π ([r]ϕ) = [r]Tr π (ϕ) Tr π (ϕ ≥ n) = ( 1≤i<j≤n x π i :¬x π j ) ∧ ( 1≤i≤n x π i :ϕ) Tr π (ϕ ≤ n) = A(¬ϕ ∨ 1≤i≤n x π i )
in particular T r π (ϕ ≥ 0) = ⊤ and T r π (ϕ ≤ 0) = A(¬ϕ).

Let us call ϕ Hπ the formula obtained from the MLC formula ϕ by first extracting counting operators, transforming into negation normal form, and applying Tr π ; we write ϕ H when π is the empty prefix.

Suppose now that M is a model satisfying ϕ H returned by the model builder. We will show that counting has not been affected by the translation. Definition 6. We call a model M ′ a naming extension of M if it is a conservative extension of M for an extended language that only adds nominals.

≤ i ≤ n, M, v i |= ϕ. For any π, choose N = 1≤i≤n (x π i , v i ) to obtain M+N, w |= ( 1≤i<j≤n x π i :¬x π j ) ∧ ( 1≤i≤n x π i :ϕ) as needed. Now, assume M, w |= ϕ ≤ n. Let v 1 to v m (m ≤ n) be
all the states of M satisfying ϕ. For any π, introduce n nominals x π 1 to x π n and a mapping N such that for 1 ≤ i ≤ n there exists j, 1 ≤ j ≤ m such that (x π i , v j ) ∈ N (two nominals can be true in the same state). Then M+N, u |= ¬ϕ ∨ 1≤i≤n x i for u an arbitrary state, and M+N, w |= ϕ H .

[⇐] Let ϕ ∈ MLC and π an arbitrary prefix, and M ′ a naming extension of M such that M ′ , w |= ϕ Hπ . If ϕ is a modal formula the implication is trivial.

Assume M ′ , w |= (ϕ ≥ n) Hπ . By definition M ′ , w |= ( 1≤i<j≤n x π i :¬x π j )∧ ( 1≤i≤n x π i :ϕ). Since x π 1 to x π n are all true at different states M, w |= ϕ ≥ n. Assume M ′ , w |= (ϕ ≤ n) H(π) , i.e., M ′ , w |= A(¬ϕ ∨ 1≤i≤n x π i ). Then an arbitrary u of M ′ , M ′ , u |= ¬ϕ ∨ 1≤i<n x π i . Hence, either M ′ , u |= ¬ϕ or M ′ , u |= x π i for a given i ∈ [[1..m]], ie {u} = V (x π i ) for i ∈ [[1..m]]
. So there can not be more than n distinct states satisfying ϕ in M ′ and M, w |= ϕ ≤ n.

⊓ ⊔

Thus we can say that for a given MLC formula ϕ, a model of ϕ H is a model of ϕ. We can now present the algorithm that carries out the reasoning task of counting. Given P a decision procedure for H(A), Γ a finite set of MLC formulas and ϕ a MLC formula: end if 10: end if Intuitively, our counting algorithm uses a model of the theory Γ to have a candidate answer n to the question "how many ϕ are implied by Γ ?". We then test satisfiability of (Γ ∧ ¬(ϕ = n)) H to get the answer. Theorem 6. The algorithm above computes |ϕ| in Γ .

1: if P (Γ H ) returns UNSAT
Our solving of the counting task relies essentially on the satisfiability problem and on the model building task carried out by the previously mentioned decision procedures. Another way of carrying this out would be to go the proof-theoretic way and directly try to derive the cardinality of ϕ given a theory Γ . However, this involves using an axiomatization of MLC which we currently lack, so given the tools we have, the satisfiability-based approach seems more adequate.

A more feasible alternative would be to solve the satisfiability problem in MLC directly. As some tableaux systems for Decription Logics with global counting already exist [START_REF] Baader | Cardinality restrictions on concepts[END_REF], a dedicated calculus for MLC seems easy to obtain. For a pratical implementation, combining tableaux with arithmetic reasoning, as it has been done in [START_REF] Ohlbach | Modal logics, description logics and arithmetic reasoning[END_REF][START_REF] Haarslev | Combining tableaux and algebraic methods for reasoning with qualified number restrictions[END_REF][START_REF] Faddoul | A hybrid tableau algorithm for ALCQ[END_REF], seems a good direction to take. The idea is to separate the counting constraints of the tableau and solve them with a constraint programming or a linear integer programming system. Thus unsatisfiable tableaux can be found efficiently even for large cardinality constraints.

In this paper we investigated various aspects of modal logics containing the counting quantifiers (ϕ ≥ n) and (ϕ ≤ n), motivated by the natural language application of representing and querying plural objects in a discourse.

These quantifiers have been introduced before in different areas (generalized quantifiers, modal logics, and description logics), and some of their previously known properties have been outlined (existence of extracted normal forms, complexity of the satisfiability problem, etc.). In this article we investigate expressive power and inference.

With respect to the former, we introduce the notion of MLC bisimulations, prove that it preserves MLC formulas and that it characterizes MLC-equivalent finite models. A natural next step would be to investigate "van Benthem characterization" results [START_REF] Van Benthem | Modal correspondence theory[END_REF]. I.e., to verify whether any formula of the first-order language with equality (in the appropriate signature) invariant under MLC bisimulations is equivalent to the translation of an MLC formula. We strongly conjecture that this is the case.

With respect to inference, we defined a new task that given a theory Γ and a formula ϕ returns the cardinality of the extension of ϕ in any model of Γ if such cardinality is fixed to be a finite natural number. We show that this task can be solved in terms of a calculus for the hybrid logic H(A) that can return a model for any satisfiable formula (e.g., tableaux based calculi as those defined by [START_REF] Bolander | Termination for hybrid tableaus[END_REF][START_REF] Kaminski | Terminating tableaux for graded hybrid logic with global modalities and role hierarchies[END_REF]). The proposed algorithm involves a translation into H(A) that might return an exponentially larger formula even when numbers are coded in unary. We conjecture that the polynomial satisfiability preserving translation of [START_REF] Areces | Coinductive models and normal forms for modal logics[END_REF] could be used instead (but assuming, again, that numbers are coded in unary). The complexity of the problem when numbers are coded in binary is open. As we mentioned in Section 4, the complexity of satisfiability for MLC and PLC when numbers are coded in unary has been established [START_REF] Van Der Hoek | Counting objects[END_REF][START_REF] Areces | The computational complexity of hybrid temporal logics[END_REF][START_REF] Tobies | Complexity results and practical algorithms for logics in Knowledge Representation[END_REF]. On the other hand, to our knowledge the problem is still open when numbers are given in binary.

Theorem 5 . 2 . 1 ∧ ϕ Hπ1 2 ,

 5212 Let ϕ ∈ MLC, and π an arbitrary prefix. Then M, w |= ϕ if and only if M ′ , w |= ϕ Hπ for M ′ a naming extension of M. Proof. We can disregard the extraction and negation normal form steps of the transformation since they are equivalence preserving. [⇒] The atomic, negation and modal connectors cases are immediate. For any model M let us represent as M+N any naming extension of M where N is the function that assigns nominals to elements of the domain of M. Assume M, w |= ϕ 1 ∧ ϕ 2 , i.e., M, w |= ϕ 1 and M, w |= ϕ 2 . By induction hypothesis M+N 1 , w |= ϕ Hπ0 1 and M+N 2 , w |= ϕ Hπ1 As N 1 and N 2 are defined on different nominals we can obtain N = N 1 ∪ N 2 and we have M+N, w |= ϕ Hπ0 and hence M+N, w |= (ϕ 1 ∧ ϕ 2 ) Hπ . The case for ϕ 1 ∨ ϕ 2 is handled similarly. Assume M, w |= ϕ ≥ n, i.e., there exist n different states v 1 to v n such that for all 1

  then

4 :

 4 let n = |||ϕ|| M | for M a model returned by P 5: if P ((Γ ∧ ¬(ϕ = n)) H ) returns UNSAT then

It is well known that FOL can express any finite counting quantifier.

Remember that ϕ ⊑ ψ as a short hand for A(ϕ → ψ) or, equivalently, (ϕ ∧ ¬ψ) ≤ 0.

The proof goes through using the same models even if we add past operators to the language, as the bisimulation shown also satisfies the standard conditions Zig -1 and Zag -1 which preserve past operators[START_REF] Blackburn | Modal Logic[END_REF].

We recall that the implication |= is to be taken as local, see Definition 2.